68 Theorems

Experimental: theorem declarations are a possible future language feature. Their syntax and semantics are not yet settled, and implementations are not required to support them. This chapter records the main design possibilities rather than specifying current behaviour.

A theorem would state a property expected to follow from a type's definitions and constraints. It would differ from a constraint: a constraint restricts which values belong to a type, whereas a theorem claims something about values which already belong to it.

For example, a type could constrain a balance to be non-negative and state the same property as a theorem for a derived availability value:

value Account
{
    Real balance where balance ≥ 0;
    Real reserved where reserved ≥ 0;
    → Real available = balance - reserved;

    constraints
    {
        reserved ≤ balance;
    }

    theorems
    {
        available ≥ 0;
    }
}

The constraint reserved ≤ balance excludes invalid accounts. The proposed theorem available ≥ 0 does not further define Account; it records a consequence which should follow from the attribute definitions and constraints.

Nominal types that support theorems

If theorem declarations become part of Predica, every nominal type constructor should support them: value types, entity types, enum types, variant types, and quotient types. There is little benefit in making theorem eligibility depend on the kind of nominal type. A theorem is simply a claim about values of its enclosing type, interpreted in that type's ordinary receiver context.

Some type kinds will naturally have more interesting theorems than others. Value and entity types can state consequences of their attributes and constraints. Variant types can state properties shared by their attributes. Quotient types can state properties which are independent of the chosen representative. Even enums can have useful theorems, particularly when they have derived attributes:

enum TrafficLight
{
    red,
    amber,
    green,

    → Boolean stop = this = red;
    → Boolean proceed = this = amber ∨ this = green;

    theorems
    {
        stop ≠ proceed;
    }
}

An enum with no derived properties may have little need for a theorem block, but that is not a reason to forbid one. Uniform support keeps generic tooling and the language model simple.

Possible semantics

Several useful interpretations are possible. They have different consequences and should not be treated as interchangeable merely through compiler policy.

Static proof obligation

The compiler could require every theorem to be proved from the type definition, its constraints, and other established facts. Compilation could fail when a theorem is false or cannot be proved. Alternatively, an inconclusive proof attempt could produce a warning. This interpretation gives a theorem a precise role without changing the values belonging to the type.

value Rectangle
{
    Real width where width ≥ 0;
    Real height where height ≥ 0;
    → Real area = width * height;

    theorems
    {
        area ≥ 0;
    }
}

Here the theorem is a simple proof obligation derived from the two attribute constraints and the definition of area.

Runtime verification

A theorem could instead be checked when a value is constructed or updated, much like a class invariant. A failed check would raise an exception or report a contract violation. Checks might be enabled only in diagnostic builds, or controlled by a deployment policy.

This interpretation requires rules defining exactly when checks occur. In particular, the language would need to say whether a sequence of updates may temporarily violate a theorem, how persisted or external values are checked, and what happens when evaluating a theorem is expensive. If a runtime theorem rejects values in every build, it is difficult to distinguish from a constraint.

Compiler information

A compiler could use an established theorem to simplify checks or generate more efficient code. For example, after proving available ≥ 0, it might remove a redundant test of that condition. Only proved facts are unconditionally safe for this purpose. A debug-only runtime check does not justify assuming the theorem in a release build.

Trusted assumption

The language could allow the programmer to assert a theorem without proof and permit the compiler to rely on it. This is powerful but dangerous: an incorrect assumption could produce incorrect program behaviour rather than a useful diagnostic. If Predica eventually supports trusted assumptions, an explicit construct such as assume may communicate that risk more clearly than a theorems block.

Documentation or external verification

Theorems could also serve as machine-readable claims for documentation or for a separate verification tool, without affecting compilation or runtime behaviour. This is simple for the compiler, but offers little advantage over Boolean functions or tests unless external tools have a defined way to consume the declarations.

Relationship to assertions and constraints

The possible meanings may ultimately deserve separate language constructs:

• constraints define the valid values of a type;
• assertions check conditions at specified runtime points;
• theorems are properties to be established by proof; and
• assumptions, if supported, are facts trusted without proof.

Predica need not provide every one of these constructs. Keeping their roles distinct avoids a theorem silently changing from a proof obligation into a runtime check or an unsafe optimisation assumption when build policy changes.

Possible staged introduction

A conservative design would introduce theorems first as verification-only declarations. A compiler or verifier would classify each theorem as proved, disproved, or unknown. Project policy could decide whether an unknown result is informational, a warning, or an error. Only proved theorems would be made available to optimisation. Runtime assertions could be considered separately.

Before theorem syntax becomes normative, the language specification must decide what evidence establishes a theorem, what happens when proof is inconclusive, where runtime checks occur (if any), and whether theorem expressions must be pure and terminating. Until those decisions are made, theorems remains experimental future syntax.