defers-a-copy-whose-argument-reads-to-a-bare-symbol.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The loop of #1729 without the walk of --deep: the branch 'b' of the fork is
# the copy 'step( tup ↦ Φ.items.tail )', and 'Φ.items.tail' reads to the bare
# symbol '𝜎1', an object nobody knows. Unfolding the copy would morph its φ,
# which asks '𝜎1' for 'next' and gets stuck. An 'unfold' line that says
# 'defer: true' does not enter such a copy: it answers it with a fresh
# symbol, writes a 'deferred' line naming the call the copy stands for, and
# the 'join' line pairs that symbol with the one the other branch holds
# (#1892, #1921).
symbolic: |
  - λ: L_fork
    morph:
      𝑛1: $.a
      𝑛2: $.b
    unfold:
      𝑛3: {of: 𝑛2, defer: true}
    join:
      𝑛4: [𝑛1, 𝑛3]
    𝑛: ⟦ φ ↦ 𝑛4 ⟧
location: 'Q.y'
input: '⟦ step(tup) ↦ ⟦ φ ↦ tup.next ⟧, items ↦ ⟦ tail ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, y ↦ ⟦ a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ Φ.step( tup ↦ Φ.items.tail ), λ ⤍ L_fork ⟧.φ ⟧'
result: '𝜎4:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝑛1·1 := 𝜎2:λ  # 𝕄(ξ.a)
      𝕄(Φ.a🌵1):
        𝑛·1·1 := Φ.step( tup ↦ Φ.items.tail )
      𝑛2·1 := 𝑛·1·1  # 𝕄(ξ.b)
      deferred(𝜎3) := Φ.step( tup ↦ 𝜎1:λ )  # 𝕄(𝑛2.φ)
      𝔻(𝜎4:λ) ∈ { 𝔻(𝜎2:λ), 𝔻(𝜎3:λ) }
      𝑛4·1 := 𝜎4:λ  # [𝑛1, 𝑛3]
      𝑛·1·2 := 𝜎4:λ:φ  # 𝑛
      𝑛·1·3 := 𝜎4:λ:φ  # 𝕄(𝑛·1·2)