LDC-E2110 — A recursive function with no termination proof

What it means

Functions in an executable package must provably terminate: a function that calls itself with no termination argument could run forever, and the compiler rejects the cycle outright rather than risking it. The diagnostic points at the function caught in the loop.

Restructuring so the function no longer calls itself — or otherwise showing the recursion bottoms out — is the fix. A plain non-recursive definition never triggers this.

Example

Arxo Law

language "law.core" version "0.2";
package demo.diagnostics version "0.1.0";
namespace "urn:law:demo:diagnostics";

function Loop(x: Integer) -> Integer = Loop(x);

Fix

Arxo Law

language "law.core" version "0.2";
package demo.diagnostics version "0.1.0";
namespace "urn:law:demo:diagnostics";

function Next(x: Integer) -> Integer = x + 1;

Engine message

The engine reports this in its own wording:

Output

example.law:5:10: error LDC-E2110: function "Loop" is part of a recursive call cycle without a termination certificate (§46/§264); core-executable requires statically proven termination

Related

• Vocabulary — how callable names enter a package.