Markdown for LLMs

LDC-E2110 — A recursive function with no termination proof

The source Markdown for this article. Copy it into your assistant or download it as a text file.

# 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

```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

```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:

```text
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](/constructs/vocabulary/) — how callable names enter a package.