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 |