defers-a-copy-whose-phi-reads-nothing-of-its-own.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The copy 'step( tup ↦ Φ.items.tail )' of a 'step' whose φ reads nothing of
# its own object. A 'defer' line asks no such thing of a copy (#1933): 'tup'
# reads to the bare symbol '𝜎1', so the line answers the copy with a fresh
# symbol and writes a 'deferred' line naming the call the copy stands for,
# whatever the φ of the copy would have come to.
symbolic: |
  - λ: L_hold
    morph:
      𝑛1: $.b
    defer:
      𝑛2: 𝑛1
    𝑛: ⟦ φ ↦ 𝑛2 ⟧
location: 'Q.y'
input: '⟦ done ↦ ⟦⟧, step(tup) ↦ ⟦ φ ↦ Φ.done ⟧, items ↦ ⟦ tail ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, y ↦ ⟦ b ↦ Φ.step( tup ↦ Φ.items.tail ), λ ⤍ L_hold ⟧.φ ⟧'
result: '𝜎2:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_hold):
      𝕄(Φ.a🌵0):
        𝑛·1·1 := Φ.step( tup ↦ Φ.items.tail )
      𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.b)
      deferred 𝜎2 := Φ.step( tup ↦ 𝜎1:λ )  # 𝕄(𝑛1.φ)
      𝑛·1·2 := 𝜎2:λ:φ  # 𝑛
      𝑛·1·3 := 𝜎2:λ:φ  # 𝕄(𝑛·1·2)