Recursor

A universal natural-number language for program synthesis and evolution.

Recursor includes a direct interpreter, a compiler to closed lambda terms, a text parser, scope-aware genetic operators, evolutionary search and program and ancestry plots.

Requires Wolfram Language 15.0 or later.

Documentation · Wolfram resource · Releases

A compact DSL provides a structured search space for generating, testing and evolving programs, with explicit rules for scope and execution. Recursor compiles these programs directly to lambda expressions, giving them a portable representation and a basis for formal reasoning.

Wolfram Language supports the experiments and visualizations. Arbitrary WL expressions can depend on definitions, attributes, evaluation order and side effects; a faithful lambda translation would need to reproduce those behaviors. WL can implement the system, while Recursor gives generated programs a small, explicit semantics that can be translated and verified independently.

Install and load the paclet:

PacletInstall[ResourceObject["https://wolfr.am/1IuTobNWg"]]
Needs["WolframInstitute`Recursor`"]

Compute a factorial:

EvaluateRecursor[RecursorExamples["Factorial"], 6]
(* 720 *)

Run a countdown:

EvaluateRecursor[WhileLoop[Var, Acc, Pred[Acc]], 100]
(* 0 *)

WhileLoop provides unbounded iteration. ToRecursor translates counter machines and partial-recursive codes. Lean checks the formal language's universality theorem. The evaluator uses finite resource budgets by default and returns Failure when one is exhausted. Each budget accepts Infinity.

Open the local library installer:

SetupRecursor[]

For scripts, install the selected libraries directly:

InstallRecursorLibraries[{"LeanLink", "MathlibLink", "Lambda"}]

Use RecursorLibraries[] to check their status. See library installation for setup details.

Run CheckRecursorProofs[] to build and check the packaged Lean proofs.

• Guides and function reference.
• Computational walkthrough — runnable Input cells with saved results.
• Language semantics — syntax, scope and evaluation.
• Formal verification — checked statements and their scope.
• Evolving lambda expressions — candidate programs, finite fitness and portable lambda terms.
• Universal computation — counter machines and the checked universality theorem.
• Arithmetic patterns — recurrences, binary digits and residues.
• Halting and budgets — trajectories and finite observation.
• Lambda reductions — compiled terms and reduction graphs.
• Evolutionary experiments — mutation, search and ancestry.

Load the source paclet from this repository:

PacletDirectoryLoad[FileNameJoin[{Directory[], "Recursor"}]]
Needs["WolframInstitute`Recursor`"]

See GUIDE.md for development conventions and API naming for public-name conventions. The CI and release guide describes automated checks and publication.

Released under the MIT license.