fires-a-formation-again-where-the-budget-stalled-it.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The memo of '--acyclic=plausible' tells no stall the step budget made to a
# firing that has spent fewer steps than the stalled one. 'L_pair' first
# reduces 'x', whose firing brings 'p' down, which reaches the formation 'f'
# through 'q' and fires it so deep that the budget runs out before 'arg'
# comes down, so the firing gets stuck. Before #1514 the stall was kept bare,
# and a later firing of the same formation, where the budget is enough, was
# told it with nothing answered in between. Now the 'evaluate' line of
# 'L_pair' fires 'f' again at a shallower site, which brings 'arg' down and
# answers (#1521, #1874).
symbolic: |
  - λ: L_outer
    dataize:
      𝛿1: ξ.arg
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
  - λ: L_wrap
    dataize:
      𝛿1: ξ.w
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
  - λ: L_pair
    morph:
      𝑛1: $.x
      𝑛2: $.f
    evaluate:
      𝑛3: 𝑛2
    𝑛: ⟦ φ ↦ 𝑛3 ⟧
location: 'Q.r'
partial: true
acyclic: plausible
steps: 12
input: >
  ⟦ r ↦ ⟦
      x ↦ ⟦ w ↦ Φ.p, λ ⤍ L_wrap ⟧.φ,
      f ↦ Φ.f,
      λ ⤍ L_pair ⟧.φ,
    p ↦ ⟦ φ ↦ Φ.q ⟧,
    q ↦ ⟦ φ ↦ Φ.f ⟧,
    f ↦ ⟦ arg ↦ Φ.c, λ ⤍ L_outer ⟧,
    c ↦ ⟦ φ ↦ Φ.d ⟧,
    d ↦ ⟦ φ ↦ Φ.e ⟧,
    e ↦ ⟦ Δ ⤍ 01- ⟧ ⟧
result: '𝜎1:λ'
protocol: |
  𝕄(Φ.r):
    𝔼(L_pair):
      𝕄(Φ.a🌵0):
        𝔼(L_wrap):
          𝔻(Φ.a🌵1):
            𝔼(L_outer):
              𝔻(Φ.a🌵2):
                𝕄(Φ.a🌵2):
                  starved(12)
              stuck(L_outer)
          stuck(L_outer)
      𝑛1·1 := ⟦ w ↦ Φ.p, λ ⤍ L_wrap ⟧.φ  # 𝕄(ξ.x)
      𝑛2·1 := ⟦ arg ↦ Φ.c, λ ⤍ L_outer ⟧  # 𝕄(ξ.f)
      𝔼(L_outer):  # 𝔼(𝑛2)
        𝔻(Φ.a🌵4):
          𝛿·4·1 := 01-
        𝛿1·4 := 𝛿·4·1  # 𝔻(ξ.arg)
        𝑛·4·1 := 𝜎1:λ  # 𝑛
        𝑛·4·2 := 𝜎1:λ  # 𝕄(𝑛·4·1)
      𝑛3·1 := 𝑛·4·2  # 𝔼(𝑛2)
      𝑛·1·1 := 𝜎1:λ:φ  # 𝑛
      𝑛·1·2 := 𝜎1:λ:φ  # 𝕄(𝑛·1·1)