phino-0.0.154: test-resources/evaluate-packs/fires-a-stalled-formation-again-once-something-was-answered.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 only while nothing new was
# answered. 'L_pair' first reduces 'x', whose firing brings 's' down, which
# fires 'f', whose operand 'big' is brought down inside the box of 's'. Since
# 's' is within 'big', the mode cuts the operand and the firing of 'f' gets
# stuck. Then the 'evaluate' lines of 'L_pair' fire 'g', which answers, and
# 'f' again, where nothing cuts it. Before #1495 that firing took the stall
# the first one met and reduced nothing; now it brings 'big' down and
# answers (#1874).
symbolic: |
  - λ: L_f
    dataize:
      𝛿1: $.arg
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
  - λ: L_g
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
  - λ: L_pair
    morph:
      𝑛1: $.x
      𝑛2: $.g
      𝑛3: $.f
    evaluate:
      𝑛4: 𝑛2
      𝑛5: 𝑛3
    𝑛: ⟦ φ ↦ 𝑛5 ⟧
location: 'Q.p'
partial: true
acyclic: plausible
input: >
  ⟦ p ↦ ⟦
      x ↦ ⟦ λ ⤍ L_f, arg ↦ Φ.s ⟧.φ,
      g ↦ Φ.g,
      f ↦ Φ.f,
      λ ⤍ L_pair ⟧.φ,
    g ↦ ⟦ λ ⤍ L_g ⟧,
    f ↦ ⟦ λ ⤍ L_f, arg ↦ Φ.big ⟧,
    s ↦ ⟦ φ ↦ Φ.f ⟧,
    big ↦ ⟦ φ ↦ Φ.k( x ↦ Φ.f ) ⟧,
    k ↦ ⟦ x ↦ ∅, φ ↦ ⟦ Δ ⤍ 01- ⟧ ⟧ ⟧
result: '𝜎2:λ'
protocol: |
  𝕄(Φ.p):
    𝔼(L_pair):
      𝕄(Φ.a🌵0):
        𝔼(L_f):
          𝔻(Φ.a🌵1):
            𝔼(L_f):
              𝔻(Φ.a🌵2):
                looped(Φ.f:φ)  # plausible
              stuck(L_f)
          stuck(L_f)
      𝑛1·1 := ⟦ λ ⤍ L_f, arg ↦ Φ.s ⟧.φ  # 𝕄(ξ.x)
      𝑛2·1 := L_g:λ  # 𝕄(ξ.g)
      𝑛3·1 := ⟦ λ ⤍ L_f, arg ↦ Φ.big ⟧  # 𝕄(ξ.f)
      𝔼(L_g):  # 𝔼(𝑛2)
        𝑛·4·1 := 𝜎1:λ  # 𝑛
        𝑛·4·2 := 𝜎1:λ  # 𝕄(𝑛·4·1)
      𝑛4·1 := 𝑛·4·2  # 𝔼(𝑛2)
      𝔼(L_f):  # 𝔼(𝑛3)
        𝔻(Φ.a🌵5):
          𝕄(Φ.a🌵5):
            𝑛·5·1 := Φ.k( x ↦ Φ.f )
          𝛿·5·1 := 01-
        𝛿1·5 := 𝛿·5·1  # 𝔻(ξ.arg)
        𝑛·5·2 := 𝜎2:λ  # 𝑛
        𝑛·5·3 := 𝜎2:λ  # 𝕄(𝑛·5·2)
      𝑛5·1 := 𝑛·5·3  # 𝔼(𝑛3)
      𝑛·1·1 := 𝜎2:λ:φ  # 𝑛
      𝑛·1·2 := 𝜎2:λ:φ  # 𝕄(𝑛·1·1)