Syntax of terms

The BNF grammar of Lambdapi is in lambdapi.bnf.

Identifiers

An identifier can be:

  • a regular identifier: / or an arbitrary non-empty sequence of UTF-8 codepoints not among \t\r\n :,;`(){}[]".@$|?/ that is not an integer number

  • an escaped identifier: an arbitrary sequence of characters enclosed between {| and |}

Remark: for any regular identifier i, {|i|} and i are identified.

Convention: identifiers starting with an uppercase letter denote types (e.g. Nat, List), and identifiers starting with a lowercase letter denote constructors, functions and proofs (e.g. zero, add, refl).

Qualified identifiers

A qualified identifier is an identifier of the form dir1. … dirn.file.id denoting the function symbol id defined in the file dir1/ … /dirn/file.lp. To be used, dir1. … dirn.file must be required first.

Remark: dir1, …, dirn cannot be natural numbers.

Terms

A user-defined term can be either:

  • TYPE, the sort for types

  • an unqualified identifier denoting a bound variable

  • a qualified or a non-qualified symbol previously declared in the current file or in some previously open module, possibly prefixed by @ to disallow implicit arguments

  • an anonymous function λ (x:A) y z,t mapping x, y and z (of type A for x) to t

  • a dependent product Π (x:A) y z,T

  • a non-dependent product A → T (syntactic sugar for Π x:A,T when x does not occur in T)

  • a let f (x:A) y z : T ≔ t in u construction

  • an application written by space-separated juxtaposition, except for symbols having an infix notation (e.g. x + y)

  • an infix symbol application x + y

  • an identifier wrapped in parentheses to access its notationless value (e.g. (+))

  • a metavariable application ?0.[x;y] that has been generated previously. ?0 alone can be used as a short-hand for ?0.[].

  • a pattern-variable application $P.[x;y] (in rules only). $P alone can be used as a shorthand for $P.[], except under binders (to avoid mistakes).

  • _ for an unknown term or a term we don’t care about. It will be replaced by a fresh metavariable in terms, or a fresh pattern variable in a rule left-hand side, applied to all the variables of the context.

  • a term enclosed between square brackets [ … ] for explicitly giving the value of an argument declared as implicit

  • a string enclosed between double quotes if the following builtin is defined:

builtin "String" := …; // : TYPE

  • a (signed) integer if the following builtins are defined:

builtin "0"  ≔ …; // : T
builtin "1"  ≔ …; // : T
…
builtin "10" := …; // : T
builtin "+" := …; // : T → T → T
builtin "*" := …; // : T → T → T
builtin "-" := …; // : T → T // (optional)
type 42;

Subterms can be parenthesized to avoid ambiguities.

Decimal notation

The system can also print the values of various types using a decimal notation by defining the following builtins:

  • Natural numbers in base 1 (Peano numbers):

builtin "nat_zero" ≔ ...; // : N
builtin "nat_succ" ≔ ...; // : N → N

  • Positive natural numbers in base 2:

builtin "pos_one" ≔ ...; // : P
builtin "pos_double" ≔ ...; // : P → P
builtin "pos_succ_double" ≔ ...; // : P → P

  • Integer numbers in base 2:

builtin "int_zero" ≔ ...; // : Z
builtin "int_positive" ≔ ...; // : P → Z
builtin "int_negative" ≔ ...; // : P → Z