Formula language user guide

The formula language is a chain-mirrored fragment of EigenTT that lives at urn:eigenius:formulas: — a small typed expression-tree language shared by every numerical institution on the platform. A single payload shape that Symbolics.jl, IntervalArithmetic.jl, Catalyst.jl, OrdinaryDiffEq.jl, and JuMP+HiGHS all consume directly.

This guide is grounded in D32 — Chain-Mirrored EigenTT Inductives and the implementation in ontologies/formulas/, kernel/src/esl/parser.rs, and kernel/src/validation/. Every claim in this guide can be exercised against the kinase-institutions notebook (notebooks/examples/kinase-institutions.json).

How to read this guide

Read sequentially if it’s your first encounter. The chapters build on each other:

1. Introduction — what the formula language is, why it exists at urn:eigenius:formulas: rather than under any one institution, and the three-surface mental model (EigenTT fragment / chain encoding / ESL formula(...) sublanguage).
2. The EigenTT fragment — the six constructors (Var, LitFloat, OpRef, App, Lam, Pi), what they correspond to in EigenTT, and why two binders (Lam / Pi) sit alongside the four expression-shaped ones.
3. Eigon-JSON embedding — the tagged-dict shape {"ctor", "args"}, left-spined App currying for multi-arg operators, the validator’s inductive-value rule, and how every chain commit gets type-checked.
4. The operator catalog — formulas:Operator resources, the on-chain operator_signature (Pi-spine), the App-spine arity check, and how to author a new operator.
5. The ESL formula(...) sublanguage — Pratt-parsed surface for + - * / ^, function calls, parens, unary minus. Operator precedence, the lexer’s unary-minus subtlety, and how the result is a Value::CtorApp literal mirroring the FormulaTerm tree.
6. Sharing across institutions — why FormulaTerm-speaking institutions can comorphism-bridge each other with mostly identity transformations; how Symbolics, IntervalArithmetic, Catalyst, DiffEq, and JuMP-HiGHS all consume the same shape.
7. Common failure modes — operator arity mismatch, unknown ctor, free variable in handler, lexer surprises.
8. Appendix — references, source index, related design docs.

Most important chapters

• 1. Introduction for the framing.
• 3. Eigon-JSON embedding for hand-authoring FormulaTerm values.
• 5. ESL formula(...) sublanguage for authoring values inside ESL programs.

Cross-references

• ESL user guide — surface syntax for ontologies and programs; formula(...) sublanguage detailed reference is here.
• EigenQL user guide — surface syntax for queries; FIBER param coercion across institutions sharing FormulaTerm.
• Platform §11 — Runtime substrate — the hosting layer for institutions that consume FormulaTerm.
• Symbolics tutorial — the most thorough worked example of FormulaTerm end-to-end.
• D32 — Chain-Mirrored EigenTT Inductives — the canonical design specification.

---

Ready to start? → 1. Introduction