phino-0.0.117: resources/contextualization.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# Contextualization 𝒞 — applied top-to-bottom, first matching clause wins. It is
# binary, 𝒞(n, c): n is the term being contextualized and c is the context (the
# expression that every free ξ inside n stands for). 𝒞 walks the term
# structurally, replacing each ξ with the context c, descending through
# dispatches and applications and stopping at formations — which introduce their
# own scope and are returned untouched — and at the global Φ and termination ⊥.
# The context c is supplied by the caller: DOT dispatching 𝜏 on a formation
# passes that formation WITHOUT the dispatched binding (⟦𝐵1, 𝐵2⟧), so a
# self-referential ξ resolves to an object that lacks 𝜏 and collapses to ⊥
# rather than re-deriving the dispatch and diverging.
#
# Each rule is an inference rule: when 'match' matches the term and 'c-match'
# matches the context (binding the meta c), the rule yields the conclusion
# 'c-result' (a premise meta or a literal), provided the ordered 'premises'
# reduce as stated. A premise binds its 'n-result' to one 𝒞 ('contextualize')
# judgment. 'c-match' is the context-argument matcher of 𝒞(n, c); it is always
# the 𝑘0 meta. Derived terms are named 𝑛1, 𝑛2, … in premise order; the term 𝒞 is
# handed is 𝑛0, leaving that numbering to the premises alone. A meta the rule
# never reads back is written bare: it matches whatever stands in its place,
# binds nothing and cannot be referenced.

- name: cg
  match: Φ
  c-match: 𝑘0
  c-result: Φ

- name: cxi
  match: ξ
  c-match: 𝑘0
  c-result: 𝑘0

- name: ct
  match: ⊥
  c-match: 𝑘0
  c-result: ⊥

- name: cf
  match: ⟦𝐵0⟧
  c-match: 𝑘0
  c-result: ⟦𝐵0⟧

- name: cd
  match: '𝑛0.𝜏0'
  c-match: 𝑘0
  c-result: '𝑛1.𝜏0'
  premises:
    - n-result: 𝑛1
      contextualize:
        - 𝑛0
        - 𝑘0

- name: ca
  match: '𝑛0(𝜏0 ↦ 𝑒1)'
  c-match: 𝑘0
  c-result: '𝑛1(𝜏0 ↦ 𝑛2)'
  premises:
    - n-result: 𝑛1
      contextualize:
        - 𝑛0
        - 𝑘0
    - n-result: 𝑛2
      contextualize:
        - 𝑒1
        - 𝑘0

- name: caa
  match: '𝑛0(α𝑖0 ↦ 𝑒1)'
  c-match: 𝑘0
  c-result: '𝑛1(α𝑖0 ↦ 𝑛2)'
  premises:
    - n-result: 𝑛1
      contextualize:
        - 𝑛0
        - 𝑘0
    - n-result: 𝑛2
      contextualize:
        - 𝑒1
        - 𝑘0