Recursive Formation and First-Class Reuse of Compositional Capabilities

Hang Lin

cs.PL Oct 14, 2026 · v1 cs.AI

Read PDF arXiv abstract Code

TL;DR

Lean 4 is the independent proof checker in a propositional microdomain, verifying ten theorem reuses generated from composite capabilities.

Abstract

We introduce FormCraft, a framework for representing acquired operations as first-class capabilities that can be recursively composed, directly invoked, and selectively retained in a persistent library through domain-specific verification. The framework separates capability well-formedness and public callability from later admission to persistent storage while preserving formation provenance and operational identity. We formalize recursive compositional closure over a uniform capability space and show that formed composites can be reused through the same public interface without re-forming their historical derivation. Experiments across continuous, discrete, propositional, and sequence domains demonstrate instance-independent reuse, independent checking, persistent acquisition, and reduced reuse-time search work under first-class exposure.

Problem

Program synthesis and library-learning systems produce useful operations, but it is unclear what makes a formed operation a reusable object, separate from the derivation that produced it, and how it should be retained for later use.

Approach

FormCraft represents primitive and composite capabilities in one well-formed capability space with typed public ports, external parameters, and recorded formation provenance. Recursive composition of compatible capabilities yields another first-class capability. Domain-specific verification is applied only when deciding whether to admit a capability to a persistent library. Experiments cover continuous, character-substitution, Lean-checked propositional, and sequence domains.

Results

The authors prove finite compositional closure and show that first-class exposure removes the need to re-form a composite's historical derivation. In the propositional microdomain, 5/5 composites were formed and Lean accepted all 10 generated theorem checks. In the sequence domain, the persistent store grew from 12 to 26 to 38 records, and reuse-time search work decreased.

Measure	Result
Composite capabilities formed	5/5
Composite theorem reuses	10/10
Lean checks accepted (exit code 0)	10/10
Capability-record hash and formation provenance preserved	Yes

Composite capability reuse in the Lean-checked propositional microdomain

Papers With

Recursive Formation and First-Class Reuse of Compositional Capabilities