What is Lambdapi?

Lambdapi is an interactive proof system featuring dependent types like in Martin-Lőf’s type theory, but allowing to define objects and types using oriented equations, aka rewriting rules, and reason modulo those equations.

This allows to simplify some proofs, and formalize complex mathematical objects that are otherwise impossible or difficult to formalize in more traditional proof systems.

Lambdapi is mostly compatible with Dedukti in the sense that it can take Dedukti files as input and output Dedukti files as well.

Definitions and proofs written in Lambdapi can be exported to Coq as well, to some extent. Lambdapi can thus be used as an interoperability tool.

Finally, Lambdapi is a logical framework, that is, it does not come with a pre-defined logic. Instead, one has to start defining its own logic. It is usually not too difficult to define a logic with a few symbols and rewrite rules, and Lambdapi comes with a repository of pre-defined logics. See for instance, the file FOL.lp which defines (polymorphic) first-order logic. There also exist definitions for the logics of HOL-Light, Coq or Agda.

Here are some of the features of Lambdapi:

  • Emacs and VSCode plugins (based on LSP)

  • support for unicode (UTF-8) and user-defined infix operators

  • symbols can be declared commutative, or associative and commutative

  • some arguments can be declared as implicit: the system will try to find out their value automatically

  • symbol and rule declarations are separated so that one can easily define inductive-recursive types or turn a proved equation into a rewriting rule

  • support for interactive resolution of typing goals, and unification goals as well, using tactics

  • a rewrite tactic similar to the one of SSReflect in Coq

  • the possibility of calling external automated provers

  • a command is provided for automatically generating an induction principle for (mutually defined) strictly-positive inductive types

  • Lambdapi can call external provers for checking the confluence and termination of user-defined rewriting rules by translating them to the XTC and HRS formats used in the termination and confluence competitions

Some bibliographic references