tells-a-budget-stall-to-a-firing-no-shallower.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The memo of '--acyclic=plausible' keeps a stall the step budget made beside
# the steps its firing had spent, and tells it to a firing of the same
# formation that has spent at least as many. 'L_pair' reduces 'x' and then
# 'y', and both spell the very same nest of 'L_outer'. The firing under 'x'
# runs out of steps two firings down, so the stall is kept. Before #1521 it
# was dropped, and the firing under 'y' went down the nest all over again.
# Now that firing stands as deep as the one under 'x' did, so it is told the
# stall and reduces nothing.
symbolic: |
  - λ: L_outer
    dataize:
      𝛿1: ξ.arg
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
  - λ: L_pair
    morph:
      𝑛1: $.x
      𝑛2: $.y
    𝑛: ⟦ φ ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧
location: 'Q.p'
partial: true
acyclic: plausible
steps: 4
input: >
  ⟦ p ↦ ⟦
      x ↦ ⟦ λ ⤍ L_outer, arg ↦ ⟦ λ ⤍ L_outer, arg ↦ ⟦ λ ⤍ L_outer, arg ↦ ⟦ λ ⤍ L_none ⟧ ⟧ ⟧ ⟧.φ,
      y ↦ ⟦ λ ⤍ L_outer, arg ↦ ⟦ λ ⤍ L_outer, arg ↦ ⟦ λ ⤍ L_outer, arg ↦ ⟦ λ ⤍ L_none ⟧ ⟧ ⟧ ⟧.φ,
      λ ⤍ L_pair ⟧.φ ⟧
protocol: |
  𝕄(Φ.p):
    𝔼(L_pair):
      𝕄(Φ.a🌵0):
        𝔼(L_outer):
          𝔻(Φ.a🌵1):
            𝔼(L_outer):
              starved(4)  # 𝔻(Φ.a🌵2)
          stuck(L_outer)
      𝑛1·1 := ⟦ λ ⤍ L_outer, arg ↦ ⟦ λ ⤍ L_outer, arg ↦ ⟦ λ ⤍ L_outer, arg ↦ L_none:λ ⟧ ⟧ ⟧.φ  # 𝕄(ξ.x)
      𝕄(Φ.a🌵3):
        𝔼(L_outer):
          stall(L_outer)
      𝑛2·1 := ⟦ λ ⤍ L_outer, arg ↦ ⟦ λ ⤍ L_outer, arg ↦ ⟦ λ ⤍ L_outer, arg ↦ L_none:λ ⟧ ⟧ ⟧.φ  # 𝕄(ξ.y)
      𝑛·1·1 := 𝜎1:λ:φ  # 𝑛
      𝑛·1·2 := 𝜎1:λ:φ  # 𝕄(𝑛·1·1)