leaves-a-formation-with-an-attribute-of-its-own-as-it-is.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The λ of a formation stands for its φ alone, so a dispatch on any other
# attribute it binds must find that attribute in the formation. Each side of
# the fork is a copy of 'box', which binds 'tag' beside its λ, and 'tag' is
# no void 'box' declares. The 'evaluate' lines hand both copies back as they
# are, the join fabricates nothing, since the two copies differ only in their
# symbols, and 'y' comes to the joined 'tag' rather than to a dispatch on a
# symbol (#2265).
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'
input: >
  ⟦ box(v) ↦ ⟦ tag ↦ ξ.v, λ ⤍ L_box ⟧,
    x ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎1:λ, left🌵 ↦ Φ.box( 𝜎2:λ ), right🌵 ↦ Φ.box( 𝜎3:λ ) ⟧,
    y ↦ Φ.x.tag ⟧
result: '𝜎4:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝔻(ξ.on🌵):
        𝛿·1·1 := 𝔻(𝜎1:λ)
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.on🌵)
      𝕄(ξ.left🌵):
        𝑛·1·1 := Φ.box( v ↦ 𝜎2:λ )
        𝑛·1·2 := ⟦ v ↦ 𝜎2:λ, tag ↦ v, λ ⤍ L_box ⟧
        morphed 𝑛·1·3 := 𝑛·1·2
      𝑛1·1 := 𝑛·1·2  # 𝕄(ξ.left🌵)
      𝕄(ξ.right🌵):
        𝑛·1·4 := Φ.box( v ↦ 𝜎3:λ )
        𝑛·1·5 := ⟦ v ↦ 𝜎3:λ, tag ↦ v, λ ⤍ L_box ⟧
        morphed 𝑛·1·6 := 𝑛·1·5
      𝑛2·1 := 𝑛·1·5  # 𝕄(ξ.right🌵)
      joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3
      𝑛·1·7 := ⟦ v ↦ 𝜎4:λ, tag ↦ v, λ ⤍ L_box ⟧
    morphed 𝑛·0·1 := 𝜎4:λ