The Logical Framework LF

Languages are encoded for study in Beluga using the Logical Framework LF [1]. New syntactic categories are defined using the LF toplevel definition, which defines a new LF (indexed) type together with its constructors.

Basic example: natural numbers

LF nat : type =
  | zero : nat
  | succ : nat -> nat
;

The first line defines a new simple LF type nat and the following lines define its constructors, zero and succ. The number three is written succ (succ (succ zero)) in this encoding.

One can define relations on natural numbers by defining indexed types. For example, we can encode a less-than-equals relation on nat as follows.

LF le : nat -> nat -> type =
  | le_z : le zero N
  | le_s : le N M ->
           % ------------------
           le (succ N) (succ M)
;

Terms of this type encode proofs. As a concrete example, a term of type le (succ zero) (succ (succ zero)) would represent a proof that 1 is less than 2.

First, observe the presence of free variables M and N. Any free variable is automatically Pi-quantified at the very front of the constructor being defined. Thus, the internal type of le_s is really {N : nat} {M : nat} le N M -> le (succ N) (succ M). (Beluga uses curly braces to write Pi-types.) We call such automatically quantified variables implicit parameters. The types of implicit parameters are determined by type reconstruction. It is not possible for the user to explicitly provide an instantiation for an implicit parameter. Instantiations for implicit parameters are automatically found via unification, based on the types of provided arguments. In other words, when one writes a term le_s Q for some argument proof Q, it is via the type of Q that the instantiations for N and M are found.

Next, the rule le_s has been suggestively written with a commented line to illustrate that one would ordinarily write this as an inference rule. In Beluga, we use LF declarations to uniformly represent the syntax and the inference rules of object languages. (Semantic predicates about encodings are defined using Inductive Types.)

One can state a theorem about such an encoding using Contextual LF and one can prove them by writing a functional program or interactively.

HOAS example: lambda calculus

Beluga is a domain-specific language for reasoning about formal systems, and one of the simplest such systems is the lambda calculus. Unlike in the natural numbers, lambda-terms contain binders. The philosophy of LF is to represent binders using higher-order abstract syntax (HOAS). That is, the functions of the metalanguage (LF) are used to represent the binding structure of the object-language (lambda calculus). Here is how we define untyped lambda terms using HOAS.

LF tm : type =
  | lam : (tm -> tm) -> tm
  | app : tm -> tm -> tm
;

One immense benefit of HOAS is that the object-language inherits the substitution properties of the metalanguage. In practice, this means that one needs not define substitution, but rather simply use LF function application. For example, consider the following encoding of a small-step, call-by-name operational semantics for the lambda calculus.

LF step : tm -> tm -> type =
  | e_app : step M M' ->
            % -----------------------
            step (app M N) (app M' N)

  | beta : step (app (lam M) N) (M N)
;

First, observe that step is not a simple type. It is indexed by two terms, so we understand it as a binary relation between terms.

Finally, the rule beta demonstrates HOAS in action. We use LF function application to implement the beta reduction of the lambda calculus. The type of the variable M in this constructor is inferred by type reconstruction as tm -> tm, given that it appears as the first argument to the constructor lam.

To complete the example encoding of the lambda calculus, we will now turn our attention to a simple type assignment system for this language. First, we will define the syntax of types.

LF tp : type =
  | base : tp
  | arr : tp -> tp -> tp
;

Second, we define the typing judgment as an indexed type. In this case, we understand oft as relating a term tm to a type tp.

LF oft : tm -> tp -> type =
  | t_app : oft M (arr A B) -> oft N A ->
            % ---------------------------
            oft (app M N) B

  | t_lam : ({x : tm} oft x A -> oft (M x) B) ->
            % ----------------------------------
            oft (lam M) (arr A B)
;

We will concentrate on the rule t_lam. Here, the variable M is understood as the body of the lambda-abstraction, and it has type tm -> tm. The premise of this rule reads “for any term x, if x is of type A, then M x is of type B”. This precisely captures the parametric reasoning used on paper when proving that a lambda-abstract has an arrow-type. Here it is necessary to explicitly write a Pi-type for x as leaving it implicit would have it incorrect quantified at the level above.

To reason about these definitions, one would formulate a theorem and prove it. Theorems are stated and proven in Beluga’s computation language. Whereas LF is used as a metalanguage for encoding various formal systems, Beluga’s computation language is used as a metalanguage for Contextual LF. To prove a theorem, one either writes a functional program in Beluga or uses Harpoon.

[1]	TODO cite LF paper