phino-0.0.97: 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 δ; derived
# terms are 𝑛, 𝑛1, … in premise order, skipping the bare 𝑛 only when 'match'
# already binds it.
#
# 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: 𝑛
      contextualize:
        - 𝑒1
        - ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧
    - n-result: 𝑛1
      normalize: 𝑛
    - d-result: δ
      dataize: 𝑛1

- name: fire
  match: ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧
  e-match: 𝑒
  d-result: δ
  premises:
    - n-result: 𝑛
      evaluate:
        - ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧
        - 𝑒
    - n-result: 𝑛1
      normalize: 𝑛
    - 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