joins-the-two-branches-of-a-fork.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# A fork answers neither of its branches: nobody has picked between the two, so
# handing one of them through would say that the branch point is not there at
# all. What it answers with is the join of the two — the shape both of them
# have, with a fresh symbol wherever they carry two different unknowns — and
# what that fresh symbol stands for stands on a line of its own, since a 𝜎 is
# the name of a λ function and nothing is assigned to it. The branches differ
# under φ, that being where the value of a branch is reached and so the only
# place the join looks at all (#1293).
symbolic: |
  - λ: L_fork
    morph:
      𝑛1: $.a
      𝑛2: $.b
    join:
      𝑛3: [𝑛1, 𝑛2]
    𝑛: 𝑛3
location: 'Q.y'
input: '⟦ y ↦ ⟦ a ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, b ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧, λ ⤍ L_fork ⟧.φ ⟧'
result: '𝜎3:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝑛1·1 := 𝜎1:λ:φ  # 𝕄(ξ.a)
      𝑛2·1 := 𝜎2:λ:φ  # 𝕄(ξ.b)
      𝔻(𝜎3:λ) ∈ { 𝔻(𝜎1:λ), 𝔻(𝜎2:λ) }
      𝑛3·1 := 𝜎3:λ:φ  # [𝑛1, 𝑛2]
      𝑛·1·1 := 𝑛3·1  # 𝑛
      𝑛·1·2 := 𝑛3·1  # 𝕄(𝑛·1·1)