phino-0.0.105: resources/dataization.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# Dataization 𝔻 — applied top-to-bottom, first matching clause wins. It is
# ternary, 𝔻(n, e, s): the second argument e is the global universe, the same
# expression that 𝕄 takes as its second argument (𝔻 forwards it to 𝕄), and the
# third argument s is the mutable state, threaded through and returned possibly
# changed. Only the 'fire' rule changes it, by firing an atom through 𝔼. The
# first argument is always a normal form: a non-NF expression matches no clause.
#
# 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
# 'd-result' (a premise bytes meta or a literal), provided 'when' holds and the
# ordered 'premises' reduce as stated. A premise binds its 'n-result'/'d-result'
# to one judgment — 𝔻 ('dataize'), 𝕄 ('morph'), 𝒩 ('normalize'), 𝔼 ('evaluate')
# or 𝒞 ('contextualize'). 'e-match' is the universe-argument matcher of
# 𝔻(n, e); it is always the e meta. The single bytes result is named δ. A
# normal-form-valued result (𝕄 'morph', 𝒩 'normalize', 𝔼 'evaluate') is named
# 𝑛, 𝑛1, … in premise order, skipping the bare 𝑛 only when 'match' already binds
# it; an expression-valued result (𝒞 'contextualize') is not a normal form —
# that is why a 'normalize' premise follows it — so it takes an 𝑒-family name
# (𝑒1, 𝑒2, …, the next index free of 'match', 𝑒 itself being the universe)
# rather than an 𝑛 name reserved for normal forms.
#
# The clauses are disjoint, so their relative order does not change behavior.
# 'norm' matches the bare meta 𝑛, which unifies with any expression, so it is
# guarded to fire only when 𝑛 is neither a formation ('not (formation 𝑛)',
# carving out 'delta', 'box', 'fire' and 'none') nor the termination ⊥
# ('not (𝑛 = ⊥)'). 𝔻 is partial: ⊥ (the terminator T) signals an error and
# lies outside its domain, so it deliberately matches no clause and dataization
# stops there — there is no 'end' rule mapping ⊥ to empty bytes (see #955).
# Without the guard 'norm' would behave correctly only by being declared last;
# with it the clauses no longer rely on their order.

- name: delta
  label: \Delta
  match: ⟦𝐵1, Δ ⤍ δ, 𝐵2⟧
  e-match: 𝑒
  d-result: δ

- name: box
  match: ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧
  e-match: 𝑒
  d-result: δ
  when:
    disjoint:
      - [Δ, λ]
      - [𝐵1, 𝐵2]
  premises:
    - n-result: 𝑒2
      contextualize:
        - 𝑒1
        - ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧
    - n-result: 𝑛1
      normalize: 𝑒2
    - d-result: δ
      dataize: 𝑛1

- name: fire
  match: ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧
  e-match: 𝑒
  d-result: δ
  premises:
    - n-result: 𝑛1
      evaluate:
        - ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧
        - 𝑒
    - d-result: δ
      dataize: 𝑛1

- name: none
  match: ⟦𝐵⟧
  e-match: 𝑒
  d-result: δ
  when:
    disjoint:
      - [Δ, λ, φ]
      - [𝐵]
  premises:
    - d-result: δ
      dataize: ⊥

- name: norm
  match: 𝑛
  e-match: 𝑒
  d-result: δ
  when:
    and:
      - not:
          formation: 𝑛
      - not:
          eq:
            - 𝑛
            - ⊥
  premises:
    - n-result: 𝑛1
      morph: 𝑛
    - d-result: δ
      dataize: 𝑛1