walks-a-binding-reading-its-copy-in-every-copy.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The synonym of '--acyclic=plausible' lets the walk enter a binding of an
# object of the world in the first copy it meets and leave it as written in
# every later one (#1480). A body reading ξ reads the copy it stands in, and
# two copies filling 'v' with different numbers make two different programs of
# the φ of 'dbl', so that φ is walked in every copy and 'L_twice' fires under
# 'a' and under 'b', each with a symbol of its own (#1485).
symbolic: |
  - λ: L_id
    morph:
      𝑛1: $.x
    𝑛: 𝑛1
  - λ: L_twice
    dataize:
      𝛿1: $.ρ
    𝑛: Φ.num( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )
deep: true
partial: true
acyclic: plausible
steps: 32
input: >
  ⟦ num ↦ ⟦ φ ↦ ∅, twice ↦ ⟦ ρ ↦ ∅, λ ⤍ L_twice ⟧ ⟧,
    dbl ↦ ⟦ v ↦ ∅, φ ↦ ξ.v.twice ⟧,
    a ↦ ⟦ λ ⤍ L_id, x ↦ Φ.dbl( v ↦ Φ.num( φ ↦ ⟦ Δ ⤍ 2A- ⟧ ) ) ⟧,
    b ↦ ⟦ λ ⤍ L_id, x ↦ Φ.dbl( v ↦ Φ.num( φ ↦ ⟦ Δ ⤍ 2B- ⟧ ) ) ⟧ ⟧
protocol: |
  𝕄(Φ):
    𝕄(Φ.a):
      𝕄(Φ.a.x):
        𝑛·0·1 := Φ.num( φ ↦ 2A-:Δ )
        𝑛·0·2 := Φ.dbl( v ↦ 𝑛·0·1 )
      𝔼(L_id):
        𝕄(Φ.a🌵0):
          𝑛·1·1 := Φ.dbl( v ↦ 𝑛·0·1 )
          𝕄(Φ.a🌵0.v):
            𝑛·1·2 := Φ.num( φ ↦ 2A-:Δ )
          𝕄(Φ.a🌵0.φ):
            𝑛·1·3 := Φ.num( φ ↦ 2A-:Δ )
            𝑛·1·4 := Φ.num( φ ↦ 2A-:Δ )
            𝔼(L_twice):
              𝔻(Φ.a🌵1):
                𝕄(Φ.a🌵1):
                  𝑛·2·1 := Φ.num( φ ↦ 2A-:Δ )
                𝛿·2·1 := 2A-
              𝛿1·2 := 𝛿·2·1  # 𝔻(ξ.ρ)
              𝑛·2·2 := Φ.num( φ ↦ 𝜎1:λ )  # 𝑛
              𝕄(𝑛·2·2):
                𝑛·2·3 := Φ.num( φ ↦ 𝜎1:λ )
              𝑛·2·4 := 𝑛·2·3  # 𝕄(𝑛·2·2)
        𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.x)
        𝑛·1·5 := 𝑛1·1  # 𝑛
        𝑛·1·6 := 𝑛1·1  # 𝕄(𝑛·1·5)
    𝕄(Φ.b):
      𝕄(Φ.b.x):
        𝑛·0·3 := Φ.num( φ ↦ 2B-:Δ )
        𝑛·0·4 := Φ.dbl( v ↦ 𝑛·0·3 )
      𝔼(L_id):
        𝕄(Φ.a🌵2):
          𝑛·3·1 := Φ.dbl( v ↦ 𝑛·0·3 )
          𝕄(Φ.a🌵2.v):
            𝑛·3·2 := Φ.num( φ ↦ 2B-:Δ )
          𝕄(Φ.a🌵2.φ):
            𝑛·3·3 := Φ.num( φ ↦ 2B-:Δ )
            𝑛·3·4 := Φ.num( φ ↦ 2B-:Δ )
            𝔼(L_twice):
              𝔻(Φ.a🌵3):
                𝕄(Φ.a🌵3):
                  𝑛·4·1 := Φ.num( φ ↦ 2B-:Δ )
                𝛿·4·1 := 2B-
              𝛿1·4 := 𝛿·4·1  # 𝔻(ξ.ρ)
              𝑛·4·2 := Φ.num( φ ↦ 𝜎2:λ )  # 𝑛
              𝕄(𝑛·4·2):
                𝑛·4·3 := Φ.num( φ ↦ 𝜎2:λ )
              𝑛·4·4 := 𝑛·4·3  # 𝕄(𝑛·4·2)
        𝑛1·3 := 𝑛·3·1  # 𝕄(ξ.x)
        𝑛·3·5 := 𝑛1·3  # 𝑛
        𝑛·3·6 := 𝑛1·3  # 𝕄(𝑛·3·5)