keeps-a-bare-symbol-no-path-casts-for-a-lenient-join.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# An 'upcast' block casts the bare symbol of its pair only when a path reaches
# every symbol of the other term (#1921). The one symbol of the branch 'b' sits
# under the dispatch '.not', which no path walks into, so both lines bind their
# terms as they are and nothing is written for the cast. The 'join' line of the
# lenient entry then pairs the bare symbol with that one symbol, the way a
# lenient join always did (#1817).
symbolic: |
  - λ: L_fork
    morph:
      𝑛1: $.a
      𝑛2: $.b
    upcast:
      𝑛3: 𝑛1
      𝑛4: 𝑛2
    join:
      𝑛5: [𝑛3, 𝑛4]
    lenient: []
    𝑛: 𝑛5
location: 'Q.y'
input: |
  ⟦
    bool(if) ↦ ⟦ φ ↦ ξ.if( α0 ↦ ⟦ Δ ⤍ FF- ⟧, α1 ↦ ⟦ Δ ⤍ 00- ⟧ ) ⟧,
    y ↦ ⟦
      a ↦ ⟦ λ ⤍ 𝜎1 ⟧,
      b ↦ ⟦ φ ↦ Φ.bool( if ↦ ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ ⟦ λ ⤍ 𝜎2 ⟧.not ⟧ ) ⟧,
      λ ⤍ L_fork
    ⟧.φ
  ⟧
result: '⟦ if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎3:λ.not ⟧, φ ↦ if( FF-:Δ, 00-:Δ ) ⟧'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝑛1·1 := 𝜎1:λ  # 𝕄(ξ.a)
      𝑛2·1 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ.not ⟧ ):φ  # 𝕄(ξ.b)
      𝑛3·1 := 𝑛1·1  # 𝑛1
      𝑛4·1 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ.not ⟧ ):φ  # 𝑛2
      𝔻(𝜎3:λ) ∈ { 𝔻(𝜎1:λ), 𝔻(𝜎2:λ) }
      𝑛5·1 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎3:λ.not ⟧ ):φ  # [𝑛3, 𝑛4]
      𝑛·1·1 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎3:λ.not ⟧ ):φ  # 𝑛
      𝑛·1·2 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎3:λ.not ⟧ ):φ  # 𝕄(𝑛·1·1)
    𝑛·0·1 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎3:λ.not ⟧ )