Repository navigation
Termination: bend2 accepts a self-call on a rebuilt constructor, the kernel rejects it #1167
Description
What you did
bend nested.bend && bend nested.bend --verdict
What happened
$ bend nested.bend
ALL PROOFS CHECK
Use --verdict for mathematical validity.
$ bend nested.bend --verdict
SOME PROOFS FAIL
Sorry - this is a mismatch between the TypeScript implementation, and the formalized BendTT kernel. [...]
$ bend nested.bend -o nested.bendtt && bendtt nested.bendtt # kernel built from bend2/bendtt.lean, Lean v4.34.0
SOME PROOFS FAIL
In height:
affine live code, calls that descend
height recurses on Node{rest}, a constructor rebuilt around a part of its input. The guide says recursive calls must use "smaller parts of their inputs, obtained through pattern matching", which this is not, yet bend2 accepts it and only the kernel refuses. One of the two should change so that they agree. This shape comes naturally with two datatypes that name each other, since mutual recursion is not allowed.
The file
import Base
type Tree is Data:
Leaf{}
Node{children: Forest}
type Forest is Data:
End{}
Cons{tree: Tree, rest: Forest}
def height(t: Tree) -> Nat:
match t:
case Leaf{}: 0n
case Node{End{}}: 1n
case Node{Cons{+x, rest}}: Nat.max(1n+height(x), height(Node{rest}))bend --version
bend 2.0.32
uname -sm
Darwin arm64
clang --version (the first line)
Apple clang version 21.0.0 (clang-2100.3.34.2)
Metadata
Metadata
Assignees
Labels
No labels
Activity
yavuzerayut commentedon Sep 28, 2026
Confirming on 2.0.32 (573002f): the
nested.bendshape reproduces (bend2 accepts, kernel rejects). Two boundary probes suggest bend2's acceptance here is size-decreasing only, so it looks like incompleteness rather than an unsound acceptance:case Leaf{}: f(Leaf{})over both constructors) — bend2 rejects with "a decreasing self-call";case Cons{x, rest}: f(Cons{x, Cons{x, rest}}), size grows) — bend2 rejects the same way.So the accepted shape is specifically "rebuild the constructor shell around a strictly deeper subterm" (parts dropped), which always decreases tree size, while the kernel demands a literal subterm. Happy to share the probe files if useful.
The kernel checks a self-call's descent by size, so a constructor reb…
The kernel checks a self-call's descent as bend2's term_descend does,…
The kernel checks a self-call's descent against the column's pattern,…
A dead field descends when it is the variable the case tree bound the…
A pair's tail is eq when it is the variable the case tree bound there…
A self-call is smaller when it is no bigger than another field of the…
Pat.fields checks the piece itself, so a constructor's tail recurses …
The kernel checks a self-call's descent against the column's pattern,…