phino-0.0.99: 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 'universe' 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.
#
# 'ma'/'maa' and 'mad'/'maad' partition application-headed normal forms on
# the argument's absoluteness (#959). Both pairs pin the argument to a
# normal-form meta, so the split is total over the normal forms 𝕄 actually
# sees: 'ma'/'maa' take a '𝑘' argument — absolute (xi-free) and in normal
# form — and recurse by re-normalizing the application; 'mad'/'maad' take an
# '𝑛' argument (a normal form) that is 'not (absolute 𝑛1)' and yield ⊥ with
# no recursion. A non-absolute argument can never fill a slot, so ⊥ is the
# correct outcome and morphing stays total: exactly one of the four fires,
# and the ⊥ axioms add no regress. Without them, a void slot receiving a
# non-absolute argument — e.g. ⟦ x ↦ ∅ ⟧( x ↦ ξ.foo ) — had no terminating
# derivation: 'copy' cannot fire on a non-absolute argument, so 'ma'
# re-morphed the identical stuck term forever.

- 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: mad
  match: '𝑛(𝜏 ↦ 𝑛1)'
  e-match: 𝑒
  n-result: ⊥
  when:
    not:
      absolute: 𝑛1

- name: maad
  match: '𝑛(α𝑖 ↦ 𝑛1)'
  e-match: 𝑒
  n-result: ⊥
  when:
    not:
      absolute: 𝑛1

- name: universe
  label: \Phi
  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: ⊥