fires-a-formation-written-in-place-with-its-voids-filled.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The left side of the fork is a formation written in place, not an object of
# the world, with its void 'v' filled by an argument. The 'v' it binds after
# the copy is the void it showed before, not an attribute of its own, so the
# 'evaluate' line fires it as it fires a copy of an object of the world, and
# the join joins the two symbols (#2267).
symbolic: |
  - λ: L_fork
    dataize:
      𝛿1: $.on🌵
    morph:
      𝑛1: $.left🌵
      𝑛2: $.right🌵
    evaluate:
      𝑛3: 𝑛1
      𝑛4: 𝑛2
    join:
      'on': 𝛿1
      left: 𝑛3
      right: 𝑛4
      otherwise: L_fork
  - λ: L_box
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
location: 'Q.y'
partial: true
input: >
  ⟦ x ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ⟦ v ↦ ∅, λ ⤍ L_box ⟧( v ↦ 𝜎2:λ ), right🌵 ↦ 𝜎3:λ ⟧,
    y ↦ Φ.x.φ ⟧
result: '𝜎5:λ.φ'
protocol: |
  𝕄(Φ.y):
    𝑛·0·1 := ⟦ v ↦ ∅, λ ⤍ L_box ⟧( v ↦ 𝜎2:λ )
    𝑛·0·2 := ⟦ v ↦ 𝜎2:λ, λ ⤍ L_box ⟧
    remembered 𝑛·0·3 ≡ Φ.x  # ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎1:λ, left🌵 ↦ 𝑛·0·2, right🌵 ↦ 𝜎3:λ ⟧
    𝔼(L_fork):
      𝔻(ξ.on🌵):
        𝛿·1·1 := 𝔻(𝜎1:λ)
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.on🌵)
      𝕄(ξ.left🌵):
        morphed 𝑛·1·1 := 𝑛·0·2
      𝑛1·1 := 𝑛·0·2  # 𝕄(ξ.left🌵)
      𝕄(ξ.right🌵):
        morphed 𝑛·1·2 := 𝜎3:λ
      𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.right🌵)
      𝔼(L_box):  # 𝔼(𝑛1)
        𝑛·2·1 := 𝜎4:λ  # 𝑛
        𝕄(𝑛·2·1):
          morphed 𝑛·2·2 := 𝜎4:λ
        𝑛·2·3 := 𝑛·2·2  # 𝕄(𝑛·2·1)
      𝑛3·1 := 𝑛·2·3  # 𝔼(𝑛1)
      joined 𝜎5 := 𝛿1·1 ? 𝜎4 : 𝜎3
      𝑛·1·3 := 𝜎5:λ
    unanswered 𝜎5  # 𝕄(𝜎5:λ)