walks-a-binding-of-an-object-once-however-many-copies-hold-it.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The synonym of '--acyclic=plausible': every dispatch on 'Φ.num' copies the
# object, and the deep walk entered the bindings of every copy as if they were
# new, so the test of 'num' was brought to its normal form and fired once
# under 'a', once under 'b' and once under 'c' (#1480). The copy goes by a
# name in the world, 'Φ.num( φ ↦ … )', and the object part of that name is a
# synonym of it, so the walk enters 'test' of 'Φ.num' in the first copy it
# meets and leaves it as written in every later one. The φ each copy fills is
# an argument of that copy and not a binding of 'Φ.num', so it is entered
# every time.
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 ⟧, test ↦ Φ.num( φ ↦ ⟦ Δ ⤍ 01- ⟧ ).twice ⟧,
    a ↦ ⟦ λ ⤍ L_id, x ↦ Φ.num( φ ↦ ⟦ Δ ⤍ 2A- ⟧ ) ⟧,
    b ↦ ⟦ λ ⤍ L_id, x ↦ Φ.num( φ ↦ ⟦ Δ ⤍ 2B- ⟧ ) ⟧,
    c ↦ ⟦ λ ⤍ L_id, x ↦ Φ.num( φ ↦ ⟦ Δ ⤍ 2C- ⟧ ) ⟧ ⟧
protocol: |
  𝕄(Φ):
    𝕄(Φ.a):
      𝕄(Φ.a.x):
        𝑛·0·1 := Φ.num( φ ↦ 2A-:Δ )
      𝔼(L_id):
        𝕄(Φ.a🌵0):
          𝑛·1·1 := Φ.num( φ ↦ 2A-:Δ )
          𝕄(Φ.a🌵0.test):
            𝑛·1·2 := Φ.num( φ ↦ 01-:Δ )
            𝑛·1·3 := Φ.num( φ ↦ 01-:Δ )
            𝔼(L_twice):
              𝔻(Φ.a🌵1):
                𝕄(Φ.a🌵1):
                  𝑛·2·1 := Φ.num( φ ↦ 01-:Δ )
                𝛿·2·1 := 01-
              𝛿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·4 := 𝑛·1·1  # 𝑛
        𝑛·1·5 := 𝑛·1·1  # 𝕄(𝑛·1·4)
    𝕄(Φ.b):
      𝕄(Φ.b.x):
        𝑛·0·2 := Φ.num( φ ↦ 2B-:Δ )
      𝔼(L_id):
        𝕄(Φ.a🌵2):
          𝑛·3·1 := Φ.num( φ ↦ 2B-:Δ )
        𝑛1·3 := 𝑛·3·1  # 𝕄(ξ.x)
        𝑛·3·2 := 𝑛·3·1  # 𝑛
        𝑛·3·3 := 𝑛·3·1  # 𝕄(𝑛·3·2)
    𝕄(Φ.c):
      𝕄(Φ.c.x):
        𝑛·0·3 := Φ.num( φ ↦ 2C-:Δ )
      𝔼(L_id):
        𝕄(Φ.a🌵3):
          𝑛·4·1 := Φ.num( φ ↦ 2C-:Δ )
        𝑛1·4 := 𝑛·4·1  # 𝕄(ξ.x)
        𝑛·4·2 := 𝑛·4·1  # 𝑛
        𝑛·4·3 := 𝑛·4·1  # 𝕄(𝑛·4·2)