parks-an-entry-that-answers-with-a-firing-of-itself.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# The same entry answering with a firing of itself, under '_acyclic': morphing
# comes back to the very term it is already reducing, so it stops there instead
# of going round until the budget is gone. The budget is generous here, so what
# ends the run is the cut and not the limit.
symbolic: |
  - λ: L_loop
    𝑛: ⟦ λ ⤍ L_loop ⟧
location: 'Q.x'
acyclic: proven
steps: 250
input: '⟦ x ↦ ⟦ λ ⤍ L_loop ⟧.foo ⟧'
result: 'L_loop:λ.foo'
protocol: |
  𝕄(Φ.x):
    𝔼(L_loop):
      𝑛·1·1 := L_loop:λ  # 𝑛
      𝑛·1·2 := L_loop:λ  # 𝕄(𝑛·1·1)
    looped(L_loop:λ)  # proven