phino-0.0.86: 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
# binary, 𝔻(n, e): the second argument e is the global universe, the same
# expression that 𝕄 takes as its second argument; 𝔻 forwards it to 𝕄. 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'), 𝔼 ('lambda')
# 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.

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

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

- name: none
  label: none
  match: ⟦𝐵⟧
  e-match: 𝑒
  d-result: '--'

- name: bott
  label: bott
  match: ⊥
  e-match: 𝑒
  d-result: '--'

- name: norm
  label: norm
  match: 𝑛
  e-match: 𝑒
  d-result: δ
  premises:
    - n-result: 𝑛1
      morph: 𝑛
    - d-result: δ
      dataize: 𝑛1