Glossary
Key terms used throughout the ImandraX documentation.
A
Admissibility — The process of checking that a new definition (type or function) satisfies the criteria for a conservative extension. For functions, this primarily means proving termination.
Auto — The primary automated tactic. Invokes the full inductive waterfall: simplification, unrolling check, destructor elimination, fertilization, generalization, and induction.
Axiom — A proposition asserted without proof. Axioms bypass the conservative extension discipline and can introduce inconsistency if not carefully chosen.
B
Bounded verification — See Unrolling.
Boyer-Moore — The foundational work by Robert S. Boyer and J Strother Moore on automated induction and theorem proving. ImandraX's waterfall is directly inspired by their system (ACL2 and its predecessors).
C
Conservative extension — A new definition that doesn't allow proving any new theorems about previously defined concepts. ImandraX's definitional principle ensures every new type and function is a conservative extension, preserving logical consistency.
Counterexample — A concrete input value that violates a property. In ImandraX, counterexamples are first-class executable values that can be computed with.
Cross-fertilization — A step in the waterfall where an inductive hypothesis (an equality) is used to substitute one side for the other in the conclusion. More disciplined than general fertilization.
D
Destructor elimination — A waterfall stage that replaces "destructor" terms (like List.hd x and List.tl x) with "constructor" terms (like fresh variables a :: b), simplifying the proof structure.
E
ε₀ (epsilon-zero) — The smallest ordinal not reachable by finite iterations of exponentiation from ω. ImandraX supports ordinal-valued termination measures up to ε₀.
Elimination rule — A proved theorem installed with [@@elim] that guides destructor elimination in the waterfall.
F
Fertilization — A waterfall stage that uses equalities in the hypotheses to simplify the conclusion.
Forward-chaining rule — A proved theorem installed with [@@fc] that derives new facts from existing hypotheses during simplification.
Functional induction — Induction schemes derived from recursive function definitions, using the function's recursion pattern to structure the proof.
G
Generalization — A waterfall stage that strengthens the goal by replacing common subterms with fresh variables, making the goal more amenable to induction.
Generalization rule — A proved theorem installed with [@@gen] that constrains how the waterfall generalizes terms.
H
HOL (Higher-Order Logic) — A family of formal logics supporting quantification over functions and predicates. ImandraX's logic is a computational fragment of HOL.
I
IML (Imandra Modelling Language) — The pure, higher-order subset of OCaml used as ImandraX's programming language and logic.
Incremental checking — ImandraX's ability to re-verify only those definitions and proofs whose dependencies have changed, rather than re-checking everything.
Induction scheme — A structured way of proving a property by base cases and inductive steps. ImandraX synthesizes schemes from recursive function definitions.
L
Lambda lifting — The process of converting anonymous functions (lambdas) into named top-level definitions, part of ImandraX's specialization pipeline.
Lemma — A proved theorem, conventionally used for intermediate results that support a larger proof. Syntactically identical to theorem.
M
Measure — An ordinal-valued function that assigns each recursive function call a value that strictly decreases. Used to prove termination.
Monomorphization — Instantiating polymorphic type parameters to concrete types, part of the specialization pipeline.
O
Opaque function — A function declared with [@@opaque] whose definition is hidden from the logic. Cannot be unrolled or expanded during proofs.
Ordinal — An equivalence class of well-orderings. ImandraX uses ordinals up to ε₀ as termination measures.
P
Permutative rewrite rule — A rewrite rule annotated with [@@perm] that only fires when the result is lexicographically smaller than the input, preventing infinite rewrite loops.
R
Region — A subset of the input space defined by a conjunction of constraints, with an invariant describing the function's behavior. See Region decomposition.
Region decomposition — Exhaustive decomposition of a function's input space into disjoint regions, each with distinct behavior. One of ImandraX's unique capabilities.
Rewrite rule — A proved theorem installed with [@@rw] that directs left-to-right term rewriting during simplification.
S
Simplification — The most important stage of the waterfall. Applies rewrite rules, forward-chaining rules, decision procedures, and case-splitting to reduce goals.
Skolemization — Replacing existentially quantified variables with Skolem functions, part of the specialization pipeline.
Specialization — The process of reducing higher-order definitions to first-order form through lambda lifting, monomorphization, and function specialization.
Structural induction — Induction over the constructors of an algebraic datatype, as opposed to functional induction derived from recursive definitions.
T
Tactic — A proof command that transforms the current goal into simpler subgoals. ImandraX has 45+ tactics that can be composed with combinators.
Termination — The property that a function halts on all inputs. Required for all recursive functions in ImandraX's logic.
Theorem — A named, proved property. Theorems can be installed as rewrite rules, forward-chaining rules, etc.
Trigger — An annotation [@trigger] on a term that tells the simplifier when to activate a forward-chaining or generalization rule.
U
Unrolling — Bounded model checking. Systematically expands recursive function calls and checks satisfiability modulo ground decision procedures. Excellent for finding counterexamples.
W
Waterfall — ImandraX's automated proof pipeline, inspired by Boyer-Moore. Combines simplification, unrolling, destructor elimination, fertilization, generalization, and induction.
Well-founded — A type or ordering with no infinite descending chains. All IML types must be well-founded, and all termination measures must use well-founded orderings.