phino-0.0.85: resources/morphing.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# Morphing 𝕄 — applied top-to-bottom, first matching clause wins. The input is
# always a normal form: a non-NF expression matches no clause. 𝕄 navigates a
# normal form down to a formation one operation at a time,
# resolving the universe Φ 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 𝔻).

- name: prim
  description: '𝕄(⟦𝐵⟧) ⟿ ⟦𝐵⟧'
  match: ⟦𝐵⟧
  then: ⟦𝐵⟧

- name: lambda
  label: \lambda
  description: '𝕄(⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧.τ) ⟿ 𝕄(𝒩(𝔼(⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧).τ))'
  match: '⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧.𝜏'
  where:
    - meta: 𝑒
      function: lambda
      args:
        - '⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧'
  then:
    morph:
      normalize: '𝑒.𝜏'

- name: dispatch
  description: '𝕄(n.τ) ⟿ 𝕄(𝒩(𝕄(n).τ))'
  match: '𝑛.𝜏'
  where:
    - meta: 𝑒
      function: morph
      args:
        - 𝑛
  then:
    morph:
      normalize: '𝑒.𝜏'

- name: application
  description: '𝕄(n(τ ↦ e)) ⟿ 𝕄(𝒩(𝕄(n)(τ ↦ e)))'
  match: '𝑛(𝜏 ↦ 𝑒)'
  where:
    - meta: 𝑒1
      function: morph
      args:
        - 𝑛
  then:
    morph:
      normalize: '𝑒1(𝜏 ↦ 𝑒)'

- name: applicationa
  description: '𝕄(n(α_i ↦ e)) ⟿ 𝕄(𝒩(𝕄(n)(α_i ↦ e)))'
  match: '𝑛(α𝑖 ↦ 𝑒)'
  where:
    - meta: 𝑒1
      function: morph
      args:
        - 𝑛
  then:
    morph:
      normalize: '𝑒1(α𝑖 ↦ 𝑒)'

- name: root
  description: '𝕄(Φ) ⟿ 𝕄(𝒩(e)) where e := global(), unless e is Φ'
  match: Φ
  where:
    - meta: 𝑒
      function: global
  when:
    not:
      eq:
        - 𝑒
        - Φ
  then:
    morph:
      normalize: 𝑒

- name: dead
  description: '𝕄(⊥) ⟿ ⊥'
  match: ⊥
  then: ⊥

- name: xi
  description: '𝕄(ξ) ⟿ ⊥'
  match: ξ
  then: ⊥

- name: globe
  description: '𝕄(Φ) ⟿ ⊥ when the universe is Φ itself'
  match: Φ
  then: ⊥