phino-0.0.152: test-resources/evaluate-packs/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', which no entry answers, so no two
# rounds are ever the same formation up to a renaming of symbols and
# '--acyclic=proven' goes round forever. The formation 'if' the deep walk fires
# on the second round holds the one it fired on the first, under the wrapper 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). Every round is a copy of 'Φ.fact', but its φ reads the 'n' and the
# 'acc' of the copy it stands in, so the walk enters it in every round rather
# than once for the whole object (#1485). The argument 'n' and every symbol
# 'dec' answers stand in a carrier '⟦ φ ↦ 𝜎 ⟧', since the walk defers a copy
# one of whose arguments is a bare symbol instead of entering it (#1729).
# The cut 'if' is the φ of a copy of 'Φ.fact', so the cut answers that copy
# with a fresh symbol, which the 'join' of the first 'if' pairs with the datum
# of the other branch, and the run answers a symbol instead of getting stuck
# (#1735).
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'
deep: true
acyclic: plausible
partial: true
steps: 250
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: |-
⟦ n ↦ 𝜎1:λ:φ, acc ↦ 00-:Δ, φ ↦ 𝜎8:λ ⟧
protocol: |
𝕄(Φ.x):
𝑛·0·1 := Φ.fact( n ↦ 𝜎1:λ:φ )
𝑛·0·2 := 𝑛·0·1( acc ↦ 00-:Δ )
𝕄(Φ.x.φ):
𝑛·0·3 := Φ.zero( x ↦ 𝜎1:λ:φ )
𝔼(L_zero):
𝛿1·1 := 𝔻(𝜎1:λ) # 𝔻(ξ.x)
𝑛·1·1 := 𝜎2:λ # 𝑛
𝑛·1·2 := 𝜎2:λ # 𝕄(𝑛·1·1)
𝑛·0·4 := Φ.if( c ↦ 𝜎2:λ )
𝑛·0·5 := Φ.if( c ↦ 𝜎2:λ )
𝑛·0·6 := 𝑛·0·5( left ↦ 00-:Δ )
𝑛·0·7 := Φ.dec( x ↦ 𝜎1:λ:φ )
𝔼(L_dec):
𝛿1·2 := 𝔻(𝜎1:λ) # 𝔻(ξ.x)
𝑛·2·1 := 𝜎3:λ:φ # 𝑛
𝑛·2·2 := 𝜎3:λ:φ # 𝕄(𝑛·2·1)
𝑛·0·8 := Φ.fact( n ↦ 𝜎3:λ:φ )
𝑛·0·9 := Φ.pair( head ↦ 𝜎1:λ:φ )
𝑛·0·10 := Φ.pair( head ↦ 𝜎1:λ:φ )
𝑛·0·11 := 𝑛·0·10( tail ↦ 00-:Δ )
𝑛·0·12 := Φ.fact( n ↦ 𝜎3:λ:φ )
𝑛·0·13 := 𝑛·0·12( acc ↦ 𝑛·0·11 )
𝑛·0·14 := Φ.if( c ↦ 𝜎2:λ )
𝑛·0·15 := 𝑛·0·14( left ↦ 00-:Δ )
𝑛·0·16 := 𝑛·0·15( right ↦ 𝑛·0·13 )
𝔼(L_if):
𝛿1·3 := 𝔻(𝜎2:λ) # 𝔻(ξ.c)
𝑛1·3 := 00-:Δ # 𝕄(ξ.left)
𝕄(Φ.a🌵4):
𝑛·3·1 := Φ.fact( n ↦ 𝜎3:λ:φ )
𝑛·3·2 := 𝑛·3·1( acc ↦ 𝑛·0·11 )
𝕄(Φ.a🌵4.acc):
𝑛·3·3 := Φ.pair( head ↦ 𝜎1:λ:φ )
𝑛·3·4 := Φ.pair( head ↦ 𝜎1:λ:φ )
𝑛·3·5 := 𝑛·3·4( tail ↦ 00-:Δ )
𝕄(Φ.a🌵4.φ):
𝑛·3·6 := Φ.zero( x ↦ 𝜎3:λ:φ )
𝔼(L_zero):
𝛿1·4 := 𝔻(𝜎3:λ) # 𝔻(ξ.x)
𝑛·4·1 := 𝜎4:λ # 𝑛
𝑛·4·2 := 𝜎4:λ # 𝕄(𝑛·4·1)
𝑛·3·7 := Φ.if( c ↦ 𝜎4:λ )
𝑛·3·8 := Φ.pair( head ↦ 𝜎1:λ:φ )
𝑛·3·9 := 𝑛·3·8( tail ↦ 00-:Δ )
𝑛·3·10 := Φ.if( c ↦ 𝜎4:λ )
𝑛·3·11 := 𝑛·3·10( left ↦ 𝑛·3·9 )
𝑛·3·12 := Φ.dec( x ↦ 𝜎3:λ:φ )
𝔼(L_dec):
𝛿1·5 := 𝔻(𝜎3:λ) # 𝔻(ξ.x)
𝑛·5·1 := 𝜎5:λ:φ # 𝑛
𝑛·5·2 := 𝜎5:λ:φ # 𝕄(𝑛·5·1)
𝑛·3·13 := Φ.fact( n ↦ 𝜎5:λ:φ )
𝑛·3·14 := Φ.pair( head ↦ 𝜎3:λ:φ )
𝑛·3·15 := Φ.pair( head ↦ 𝜎1:λ:φ )
𝑛·3·16 := 𝑛·3·15( tail ↦ 00-:Δ )
𝑛·3·17 := Φ.pair( head ↦ 𝜎3:λ:φ )
𝑛·3·18 := 𝑛·3·17( tail ↦ 𝑛·3·16 )
𝑛·3·19 := Φ.fact( n ↦ 𝜎5:λ:φ )
𝑛·3·20 := 𝑛·3·19( acc ↦ 𝑛·3·18 )
𝑛·3·21 := Φ.if( c ↦ 𝜎4:λ )
𝑛·3·22 := 𝑛·3·21( left ↦ 𝑛·3·16 )
𝑛·3·23 := 𝑛·3·22( right ↦ 𝑛·3·20 )
looped(𝑛·0·16) := 𝜎6 # plausible
𝑛2·3 := 𝜎6:λ # 𝕄(ξ.right)
𝔻(𝜎7:λ) == 00-
𝑛3·3 := 𝜎7:λ # 𝑛1
𝑛4·3 := 𝑛2·3 # 𝑛2
𝔻(𝜎8:λ) ∈ { 𝔻(𝜎7:λ), 𝔻(𝜎6:λ) }
𝑛5·3 := 𝜎8:λ # [𝑛3, 𝑛4]
𝑛·3·24 := 𝑛5·3 # 𝑛
𝑛·3·25 := 𝑛5·3 # 𝕄(𝑛·3·24)