stops-an-accumulator-recursion-under-plausible.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# A factorial with an accumulator, under '--acyclic=plausible'. Every round
# wraps the accumulator in one more 'pair' and the counter in one more 'dec',
# so no two rounds are ever the same formation up to a renaming of symbols and
# '--acyclic=proven' never cuts it. The body of 'fact' dispatches 'φ' off its
# 'if', so 'ml' fires it, and the 'morph' operand of 'L_if' reduces the
# recursive call the same way. The 'if' it reaches on the second round holds
# the one fired on the first, under the wrappers it gained, which is what the
# plausible guard compares by, so the second firing is cut before it opens and
# its 'looped' line names the mode that cut it (#1451). The operand hands back
# the term the cut left, which no 'join' can pair with the datum of the other
# branch, so the first 'L_if' gets stuck and '--partial' parks it.
symbolic: |
  - λ: L_zero
    dataize:
      𝛿1: $.x
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
  - λ: L_dec
    dataize:
      𝛿1: $.x
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
  - λ: L_if
    dataize:
      𝛿1: $.c
    morph:
      𝑛1: $.left
      𝑛2: $.right
    symbolize:
      𝑛3: 𝑛1
      𝑛4: 𝑛2
    join:
      𝑛5: [𝑛3, 𝑛4]
    𝑛: 𝑛5
location: 'Q.x'
acyclic: plausible
partial: true
input: >
  ⟦ if ↦ ⟦ c ↦ ∅, left ↦ ∅, right ↦ ∅, λ ⤍ L_if ⟧,
    zero ↦ ⟦ x ↦ ∅, λ ⤍ L_zero ⟧,
    dec ↦ ⟦ x ↦ ∅, λ ⤍ L_dec ⟧,
    pair ↦ ⟦ head ↦ ∅, tail ↦ ∅ ⟧,
    fact ↦ ⟦ n ↦ ∅, acc ↦ ∅, φ ↦ Φ.if( c ↦ Φ.zero( x ↦ ξ.n ), left ↦ ξ.acc, right ↦ Φ.fact( n ↦ Φ.dec( x ↦ ξ.n ), acc ↦ Φ.pair( head ↦ ξ.n, tail ↦ ξ.acc ) ).φ ).φ ⟧,
    x ↦ Φ.fact( n ↦ ⟦ λ ⤍ 𝜎1 ⟧, acc ↦ ⟦ Δ ⤍ 00- ⟧ ).φ ⟧
result: 'Φ.if( c ↦ Φ.zero( x ↦ 𝜎1:λ ), left ↦ 00-:Δ, right ↦ Φ.fact( n ↦ Φ.dec( x ↦ 𝜎1:λ ), acc ↦ Φ.pair( head ↦ 𝜎1:λ, tail ↦ 00-:Δ ) ).φ ).φ'
protocol: |
  𝕄(Φ.x):
    𝑛·0·1 := Φ.fact( n ↦ 𝜎1:λ )
    𝑛·0·2 := 𝑛·0·1( acc ↦ 00-:Δ )
    𝑛·0·3 := Φ.if( c ↦ Φ.zero( x ↦ 𝜎1:λ ) )
    𝑛·0·4 := 𝑛·0·3( left ↦ 00-:Δ )
    𝑛·0·5 := 𝑛·0·4( right ↦ Φ.fact( n ↦ Φ.dec( x ↦ 𝜎1:λ ), acc ↦ Φ.pair( head ↦ 𝜎1:λ, tail ↦ 00-:Δ ) ).φ )
    𝔼(L_if):
      𝔻(Φ.a🌵0):
        𝕄(Φ.a🌵0):
          𝑛·1·1 := Φ.zero( x ↦ 𝜎1:λ )
        𝔼(L_zero):
          𝛿1·2 := 𝔻(𝜎1:λ)  # 𝔻(ξ.x)
          𝑛·2·1 := 𝜎2:λ  # 𝑛
          𝑛·2·2 := 𝜎2:λ  # 𝕄(𝑛·2·1)
      𝛿1·1 := 𝔻(𝜎2:λ)  # 𝔻(ξ.c)
      𝑛1·1 := 00-:Δ  # 𝕄(ξ.left)
      𝕄(Φ.a🌵3):
        𝑛·1·2 := Φ.fact( n ↦ Φ.dec( x ↦ 𝜎1:λ ) )
        𝑛·1·3 := 𝑛·1·2( acc ↦ Φ.pair( head ↦ 𝜎1:λ, tail ↦ 00-:Δ ) )
        𝑛·1·4 := Φ.if( c ↦ Φ.zero( x ↦ Φ.dec( x ↦ 𝜎1:λ ) ) )
        𝑛·1·5 := 𝑛·1·4( left ↦ Φ.pair( head ↦ 𝜎1:λ, tail ↦ 00-:Δ ) )
        𝑛·1·6 := 𝑛·1·5( right ↦ Φ.fact( n ↦ Φ.dec( x ↦ Φ.dec( x ↦ 𝜎1:λ ) ), acc ↦ Φ.pair( head ↦ Φ.dec( x ↦ 𝜎1:λ ), tail ↦ Φ.pair( head ↦ 𝜎1:λ, tail ↦ 00-:Δ ) ) ).φ )
        looped(𝑛·0·5)  # plausible
      𝑛2·1 := 𝑛·1·3.φ  # 𝕄(ξ.right)
      𝔻(𝜎3:λ) == 00-
      𝑛3·1 := 𝜎3:λ  # 𝑛1
      𝔻(𝜎4:λ) == 00-
      𝑛4·1 := 𝑛·1·2( acc ↦ Φ.pair( head ↦ 𝜎1:λ, tail ↦ 𝜎4:λ ) ).φ  # 𝑛2
      unjoined(L_if)  # 𝜎3:λ vs 𝑛·1·2( acc ↦ Φ.pair( head ↦ 𝜎1:λ, tail ↦ 𝜎4:λ ) ).φ