phino-0.0.96: resources/morphing.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# Morphing 𝕄 — applied top-to-bottom, first matching clause wins. It is ternary,
# 𝕄(n, e, s): n is the morphed term, e is the fixed global universe and s is
# the mutable state. The universe is threaded unchanged through every recursive
# call and substituted for Φ by the 'root' rule (Φ, rendered Q, is just the
# locator of e); the state is threaded too and the new state returned. Only the
# 'ml' rule changes it, by firing an atom through 𝔼. The first argument is
# always a normal form: a non-NF expression matches no clause. 𝕄 navigates a
# normal form to a formation one operation at a time, resolving Φ against e and
# peeling dispatches and applications through normalization 𝒩. It never fires a
# bare atom: a saturated λ-formation is returned untouched and fired later by 𝔼
# (the 'fire' rule of 𝔻).
#
# Each rule is an inference rule: when 'match' matches the term and 'e-match'
# matches the universe (binding the meta e), the rule yields the conclusion
# 'n-result' (a premise meta or a literal), provided 'when' holds and the
# ordered 'premises' reduce as stated. A premise binds 'n-result' to the result
# of one judgment — 𝕄 ('morph'), 𝒩 ('normalize') or 𝔼 ('evaluate'). 'e-match' is
# the universe-argument matcher of 𝕄(n, e); usually the e meta, but a rule may
# pin it to a literal (e.g. 'mg' fires only on 𝕄(Φ, Φ)). Derived terms are
# named 𝑛, 𝑛1, … in premise order; the bare 𝑛 is skipped only when 'match'
# already binds it.
#
# 'ml' and 'md' are kept mutually exclusive: 'md' fires only
# when its head 𝑛 is not a formation ('not (formation 𝑛)'), so every formation
# head — λ-bearing or not — is left to 'ml' (and 'mf'). The two clauses
# are disjoint and their relative order does not change behavior.

- name: mf
  match: ⟦𝐵⟧
  e-match: 𝑒
  n-result: ⟦𝐵⟧

- name: ml
  label: \lambda
  match: '⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧.𝜏'
  e-match: 𝑒
  n-result: 𝑛2
  premises:
    - n-result: 𝑛
      evaluate:
        - '⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧'
        - 𝑒
    - n-result: 𝑛1
      normalize: '𝑛.𝜏'
    - n-result: 𝑛2
      morph: 𝑛1

- name: md
  match: '𝑛.𝜏'
  e-match: 𝑒
  n-result: 𝑛3
  when:
    not:
      formation: 𝑛
  premises:
    - n-result: 𝑛1
      morph: 𝑛
    - n-result: 𝑛2
      normalize: '𝑛1.𝜏'
    - n-result: 𝑛3
      morph: 𝑛2

- name: ma
  match: '𝑛(𝜏 ↦ 𝑒1)'
  e-match: 𝑒
  n-result: 𝑛3
  premises:
    - n-result: 𝑛1
      morph: 𝑛
    - n-result: 𝑛2
      normalize: '𝑛1(𝜏 ↦ 𝑒1)'
    - n-result: 𝑛3
      morph: 𝑛2

- name: maa
  match: '𝑛(α𝑖 ↦ 𝑒1)'
  e-match: 𝑒
  n-result: 𝑛3
  premises:
    - n-result: 𝑛1
      morph: 𝑛
    - n-result: 𝑛2
      normalize: '𝑛1(α𝑖 ↦ 𝑒1)'
    - n-result: 𝑛3
      morph: 𝑛2

- name: root
  match: Φ
  e-match: 𝑒
  n-result: 𝑛1
  when:
    not:
      eq:
        - 𝑒
        - Φ
  premises:
    - n-result: 𝑛
      normalize: 𝑒
    - n-result: 𝑛1
      morph: 𝑛

- name: dead
  match: ⊥
  e-match: 𝑒
  n-result: ⊥

- name: xi
  match: ξ
  e-match: 𝑒
  n-result: 𝑛
  premises:
    - n-result: 𝑛
      morph: ⊥

- name: mg
  match: Φ
  e-match: Φ
  n-result: 𝑛
  premises:
    - n-result: 𝑛
      morph: ⊥