parks-a-firing-whose-operand-loops.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# A loop met while an operand is being brought down to data, one whole run of 𝔻
# below the spine. That run reduces the operand under a synthetic attribute of
# its own, so what it parks on is no term of the program; the spine around the
# firing is what answers instead, with the term it had reached when the firing
# started (see 'down' in 'Morph'). The entry never fires, and the protocol keeps
# the firing it opened and the loop it met underneath.
symbolic: |
  - λ: L_outer
    dataize:
      𝛿1: ξ.arg
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
  - λ: L_loop
    𝑛: ⟦ λ ⤍ L_loop ⟧
location: 'Q.x'
acyclic: proven
steps: 250
input: >
  ⟦ x ↦ ⟦ arg ↦ ⟦ λ ⤍ L_loop ⟧.foo, λ ⤍ L_outer ⟧.bar ⟧
result: '⟦ arg ↦ L_loop:λ.foo, λ ⤍ L_outer ⟧.bar'
protocol: |
  𝕄(Φ.x):
    𝔼(L_outer):
      𝔻(Φ.a🌵0):
        𝕄(Φ.a🌵0):
          𝔼(L_loop):
            𝑛·2·1 := L_loop:λ  # 𝑛
            𝑛·2·2 := L_loop:λ  # 𝕄(𝑛·2·1)
          looped(L_loop:λ)  # proven