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' keeps no stall the step budget made. The
# formation 'f' is first fired deep inside the operand of 'L_wrap', where the
# budget runs out before 'arg' comes down, so the firing gets stuck. Before
# #1514 the stall was kept, and the firings of the same formation under
# 'Φ.q.φ' and 'Φ.f', where the budget is enough, were told it bare, with
# nothing answered in between. Now the firing under 'Φ.q.φ' brings 'arg'
# down and answers, and the walk leaves that answer in 'f', so it fires
# nothing more when it reaches 'Φ.f' (#1720).
symbolic: |
  - λ: L_outer
    dataize:
      𝛿1: ξ.arg
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
  - λ: L_wrap
    dataize:
      𝛿1: ξ.w
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
deep: true
partial: true
acyclic: plausible
steps: 10
input: >
  ⟦ x ↦ ⟦ w ↦ Φ.p, λ ⤍ L_wrap ⟧,
    p ↦ ⟦ φ ↦ Φ.q ⟧,
    q ↦ ⟦ φ ↦ Φ.f ⟧,
    f ↦ ⟦ arg ↦ Φ.c, λ ⤍ L_outer ⟧,
    c ↦ ⟦ φ ↦ Φ.d ⟧,
    d ↦ ⟦ φ ↦ Φ.e ⟧,
    e ↦ ⟦ Δ ⤍ 01- ⟧ ⟧
protocol: |
  𝕄(Φ):
    𝕄(Φ.x):
      𝔼(L_wrap):
        𝔻(Φ.a🌵0):
          𝔼(L_outer):
            𝔻(Φ.a🌵1):
              𝕄(Φ.a🌵1):
                starved(10)
            stuck(L_outer)
        stuck(L_outer)
    𝕄(Φ.q):
      𝕄(Φ.q.φ):
        𝔼(L_outer):
          𝔻(Φ.a🌵2):
            𝛿·3·1 := 01-
          𝛿1·3 := 𝛿·3·1  # 𝔻(ξ.arg)
          𝑛·3·1 := 𝜎1:λ  # 𝑛
          𝑛·3·2 := 𝜎1:λ  # 𝕄(𝑛·3·1)