Totality

PFCL language reference · composure.systems

1.Scope

The guarantee applies to composed functions in a catalog, considered admitted by an analyzer. Each term is fixed by the specification.

1. A composed function is a function whose body is a PFCL expression, as distinct from a primitive whose body is external code.
2. A catalog is a set of function definitions addressed by the SHA-256 of the body expression.
3. An analyzer is an implementation of the admission rules stated in section 3. A conforming analyzer decides admission for every input catalog in bounded time.
4. A function is admitted iff the analyzer produces the admitted verdict on its body under the rules of section 3.
5. A function terminates on an input iff its evaluation under the PFCL operational semantics reaches a value in finitely many steps.

2.Statement

Let f be a composed function admitted by a conforming analyzer, and let x be an input of f's declared type. Then one of the following holds:

1. f(x) terminates at a value of f's declared output type, or
2. f's body contains a call to the fuel channel (section 3.3), the caller-supplied budget is exhausted during evaluation, and f(x) terminates at the defined exhaustion value for that call.

No third outcome is admitted by the specification.

3.Admission rules

The analyzer admits a body by satisfying at least one of the following rules on each recursion carrier that appears in the body. A body containing no recursion carrier is admitted unconditionally.

3.1Scheme operators

A recursion carrier is admissible under this rule if it is a scheme operator whose termination is a property of the operator and holds for every well-typed callback. The set of scheme operators is fixed by the language and is enumerated in the analyzer specification. A body composed of scheme operators, non-recursive primitives, and previously admitted composed functions is admitted.

3.2Declared witness

A recursion carrier is admissible under this rule if the enclosing definition carries a termination witness in one of the recognized kinds and the analyzer discharges the witness syntactically. The recognized witness kinds are:

• Structural. The recursion argument is a strict subterm of a value of an inductive type in every recursive call.
• Numeric. A declared measure expression over the recursion parameters strictly decreases on every recursive call, with the decrease established by linear-arithmetic inspection of the call arguments.
• Fuel. A declared caller-supplied budget parameter strictly decrements on every recursive call by a declared positive integer.

Witness discharge does not execute the body. The analyzer confirms the witness by inspection of the body's abstract syntax.

3.3Fuel channel

A recursion carrier is admissible under this rule if the body's only recursion is a call to fold_until with a caller-supplied budget expression and a defined exhaustion value. The analyzer requires the budget expression to be declared in the enclosing definition's witness block. Budget exhaustion at evaluation is not an error; it produces the defined value at the exhaustion boundary.

3.4Refusal

A body containing a recursion carrier that is admitted under none of the above rules is refused. A catalog containing at least one refused body does not load.

4.Reproducibility

The verdict of a conforming analyzer on a body is a function of the body and the analyzer's version. Every conforming analyzer of the same version reaches the same verdict on the same body.

1. A verdict record consists of the body's SHA-256, the admission rule under which the body was admitted, and the analyzer version that produced the verdict.
2. A verdict record produced by analyzer version N is valid for verification by any conforming analyzer of version ≥ N that retains the acceptance rules of version N.
3. A verdict record produced under one rule is not degraded by a later analyzer's acquisition of stricter rules under a different rule.

This property is what extends the guarantee to third-party bodies. A body admitted on the author's analyzer is verified locally by the consumer's analyzer under the same rules. The consumer's trust rests on the local analyzer, not on the author.

5.Exclusions

The guarantee does not cover the following.

1. The analyzer's own soundness is established by inspection and by test corpus, not by mechanical proof. Mechanical verification of the analyzer's rules is future work.
2. The guarantee is termination, not correctness. A total function returning a value inconsistent with its intended semantics remains total.
3. Bodies that use the fuel channel terminate at the exhaustion value on inputs where the budget is insufficient. This is a defined outcome, not an unbounded computation, and is included in the guarantee. It is called out here because it is the sole shape in which termination is decoupled from the input.
4. Primitives are outside the specification's scope. A composed function calling a primitive terminates only if the primitive terminates. Primitive termination is established by external audit of the primitive's implementation.

6.Verification

A reader who wants to reproduce a verdict on a given catalog obtains the catalog, obtains a conforming analyzer, and runs the analyzer's admission pass. The verdict record produced is a function of the two inputs. The record's fields are described in the analyzer specification.