joins-a-bare-symbol-with-a-branch-holding-one-symbol-when-lenient.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The fork of 'bool.and' from #1817: one branch is a bare symbol, the other a
# call of 'Φ.bool', whose φ is code and not a formation, so its φ chain ends in
# no symbol. The call holds one symbol, '𝜎2', so a lenient join answers a copy
# of the call with '𝜎2' replaced by a fresh '𝜎3', which stands for either
# '𝜎1' or '𝜎2'. The join reads nothing outside the two branches.
symbolic: |
  - λ: L_fork
    morph:
      𝑛1: $.a
      𝑛2: $.b
    join:
      𝑛3: [𝑛1, 𝑛2]
    lenient: true
    𝑛: 𝑛3
location: 'Q.y'
deep: true
input: |
  ⟦
    bool(if) ↦ ⟦ φ ↦ ξ.if( α0 ↦ ⟦ Δ ⤍ FF- ⟧, α1 ↦ ⟦ Δ ⤍ 00- ⟧ ) ⟧,
    y ↦ ⟦
      r ↦ ⟦
        a ↦ ⟦ λ ⤍ 𝜎1 ⟧,
        b ↦ ⟦ φ ↦ Φ.bool( if ↦ ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧ ) ⟧,
        λ ⤍ L_fork
      ⟧
    ⟧
  ⟧
result: 'Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎3:λ ⟧ ):φ:r'
protocol: |
  𝕄(Φ.y):
    𝕄(Φ.y.r):
      𝕄(Φ.y.r.b):
        𝕄(Φ.y.r.b.φ):
          𝑛·0·1 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ ⟧ )
      𝔼(L_fork):
        𝑛1·1 := 𝜎1:λ  # 𝕄(ξ.a)
        𝕄(Φ.a🌵1):
          𝕄(Φ.a🌵1.φ):
            𝑛·1·1 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ ⟧ )
        𝑛2·1 := 𝑛·1·1:φ  # 𝕄(ξ.b)
        𝔻(𝜎3:λ) ∈ { 𝔻(𝜎1:λ), 𝔻(𝜎2:λ) }
        𝑛3·1 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎3:λ ⟧ ):φ  # [𝑛1, 𝑛2]
        𝑛·1·2 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎3:λ ⟧ ):φ  # 𝑛
        𝑛·1·3 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎3:λ ⟧ ):φ  # 𝕄(𝑛·1·2)