joins-a-bare-symbol-a-cast-brought-into-a-decorator-of-a-fork.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The left side holds 'k' beside a φ that is another fork, and the right side
# is the bare symbol 𝜎3. The φ chain of the left side ends in no symbol, so
# the 'cast' block used to cast nothing, and the join diverged (#2223). Now
# the cast copies the left side down its φ chain to the first φ binding no φ
# of its own, the fork, and puts 𝜎3 in its place. The two sides then differ
# in what their φ holds, so the firing fabricates a formation. The program
# asks that formation for its φ, a copy of 'L_fork' with the inner fork on the
# left and 𝜎3 on the right. That copy fires the inner fork, which answers 𝜎7,
# the join of 𝜎5 and 𝜎6, casts 𝜎3 into the shape of that answer, and answers
# 𝜎8, the join of 𝜎7 and 𝜎3.
symbolic: |
  - λ: L_fork
    dataize:
      𝛿1: $.on🌵
    morph:
      𝑛1: $.left🌵
      𝑛2: $.right🌵
    evaluate:
      𝑛3: 𝑛1
      𝑛4: 𝑛2
    cast:
      𝑛5: 𝑛3
      𝑛6: 𝑛4
    join:
      on: 𝛿1
      left: 𝑛5
      right: 𝑛6
      otherwise: L_fork
location: 'Q.e1'
input: '⟦ e1 ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎1 ⟧, left🌵 ↦ ⟦ k ↦ ⟦⟧, φ ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎5 ⟧ ⟧, right🌵 ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎6 ⟧ ⟧ ⟧ ⟧, right🌵 ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧.φ.φ ⟧'
result: '𝜎8:λ'
protocol: |
  𝕄(Φ.e1):
    𝔼(L_fork):
      𝔻(ξ.on🌵):
        𝛿·1·1 := 𝔻(𝜎1:λ)
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.on🌵)
      𝕄(ξ.left🌵):
        morphed 𝑛·1·1 := ⟦ k ↦ ⟦⟧, φ ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎4:λ, left🌵 ↦ 𝜎5:λ:φ, right🌵 ↦ 𝜎6:λ:φ ⟧ ⟧
      𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.left🌵)
      𝕄(ξ.right🌵):
        morphed 𝑛·1·2 := 𝜎3:λ
      𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.right🌵)
      cast 𝑛6·1 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎3:λ ⟧  # 𝑛2·1 up to 𝑛·1·1
      fabricated 𝑛·1·3 := 𝑛·1·1 and 𝑛6·1  # ⟦ left🌵 ↦ 𝑛·1·1, right🌵 ↦ ⟦ k ↦ ⟦⟧, φ ↦ 𝜎3:λ ⟧, k ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ρ.left🌵.k, right🌵 ↦ ρ.right🌵.k ⟧, φ ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ρ.left🌵.φ, right🌵 ↦ ρ.right🌵.φ ⟧ ⟧
    𝔼(L_fork):
      𝔻(ξ.on🌵):
        𝛿·2·1 := 𝔻(𝜎1:λ)
      𝛿1·2 := 𝛿·2·1  # 𝔻(ξ.on🌵)
      𝕄(ξ.left🌵):
        morphed 𝑛·2·1 := ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎4:λ, left🌵 ↦ 𝜎5:λ:φ, right🌵 ↦ 𝜎6:λ:φ ⟧
      𝑛1·2 := ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎4:λ, left🌵 ↦ 𝜎5:λ:φ, right🌵 ↦ 𝜎6:λ:φ ⟧  # 𝕄(ξ.left🌵)
      𝕄(ξ.right🌵):
        morphed 𝑛·2·2 := 𝑛2·1
      𝑛2·2 := 𝑛2·1  # 𝕄(ξ.right🌵)
      𝔼(L_fork):  # 𝔼(𝑛1)
        𝔻(ξ.on🌵):
          𝛿·3·1 := 𝔻(𝜎4:λ)
        𝛿1·3 := 𝛿·3·1  # 𝔻(ξ.on🌵)
        𝕄(ξ.left🌵):
          morphed 𝑛·3·1 := 𝜎5:λ:φ
        𝑛1·3 := 𝑛·3·1  # 𝕄(ξ.left🌵)
        𝕄(ξ.right🌵):
          morphed 𝑛·3·2 := 𝜎6:λ:φ
        𝑛2·3 := 𝑛·3·2  # 𝕄(ξ.right🌵)
        joined 𝜎7 := 𝛿1·3 ? 𝜎5 : 𝜎6
        𝑛·3·3 := 𝜎7:λ:φ
      𝑛3·2 := 𝑛·3·3  # 𝔼(𝑛1)
      cast 𝑛6·2 := 𝜎3:λ:φ  # 𝑛2·2 up to 𝑛3·2
      joined 𝜎8 := 𝛿1·2 ? 𝜎7 : 𝜎3
      𝑛·2·3 := 𝜎8:λ:φ
    morphed 𝑛·0·1 := 𝜎8:λ