joins-a-branch-reached-from-a-literal.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# A datum is never joined with anything, which is why a branch carrying one
# goes through 'symbolize' first: a value somebody worked out and a value
# nobody did are a difference in kind and not in value, and after that stage
# both branches carry ⟦ λ ⤍ 𝜎 ⟧ where they differ. The symbol the literal
# stood into is a symbol like any other here, so what the fork answers is the
# join of the two and what is known about the literal stays on the line the
# 'symbolize' stage wrote it on. Both stages walk the φ chain and nothing
# else, that being where the value of a branch is reached (#1293).
symbolic: |
  - λ: L_fork
    morph:
      𝑛1: $.a
      𝑛2: $.b
    symbolize:
      𝑛3: 𝑛1
      𝑛4: 𝑛2
    join:
      𝑛5: [𝑛3, 𝑛4]
    𝑛: 𝑛5
location: 'Q.y'
input: '⟦ y ↦ ⟦ a ↦ ⟦ φ ↦ ⟦ Δ ⤍ 01- ⟧ ⟧, b ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎7 ⟧ ⟧, λ ⤍ L_fork ⟧.φ ⟧'
result: '𝜎9:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝑛1·1 := 01-:Δ:φ  # 𝕄(ξ.a)
      𝑛2·1 := 𝜎7:λ:φ  # 𝕄(ξ.b)
      𝔻(𝜎8:λ) == 01-
      𝑛3·1 := 𝜎8:λ:φ  # 𝑛1
      𝑛4·1 := 𝑛2·1  # 𝑛2
      𝔻(𝜎9:λ) ∈ { 𝔻(𝜎8:λ), 𝔻(𝜎7:λ) }
      𝑛5·1 := 𝜎9:λ:φ  # [𝑛3, 𝑛4]
      𝑛·1·1 := 𝑛5·1  # 𝑛
      𝑛·1·2 := 𝑛5·1  # 𝕄(𝑛·1·1)