Representing Syntax

This page is part of the introduction to proving metatheorems with STELF.

To use STELF, you need to know how to represent deductive systems using the LF logical framework. LF is a very convenient language for representing deductive systems that involve TODO and hypothetical judgements, such as programming languages and logics. However, we won’t see any examples of such uses of LF until later. The goal of the first part of this guide is to take a broad sweep through LF and STELF; you will see how to represent and prove properties of a very simple language, which will prepare you for more sophisticated (and more impressive) content later on.

Our first task is to introduce LF and see how to represent the syntax of a deductive system in it. We refer to a language that we are formalizing in LF as an object language (the language that it is the object of our study). In contrast, we sometimes refer to LF as the meta-language. To keep things simple, we use the natural numbers as first example object language.

Natural numbers

Metatheoretic Definition

The syntax of the natural numbers is defined in the metatheory is as follows ¹:

$${ {} \over \Gamma \vdash \text{zero} \ \text{nat} } { \Gamma \vdash n \ \text{nat} \over \Gamma \vdash \text{succ}(n) \ \text{nat} }$$

That is,

• In any context, zero is a natural number
• If in a context $\Gamma$, $n$ is a natural number, then in $\Gamma$, $\text{succ}(n)$ is a natural number.

Indeed, this would be the way define the natural numbers in Prolog:

nat(zero).
nat(succ(N)) :- nat(N).

LF representation

LF is a typed lambda-calculus². We represent an object language in LF by giving an LF signature that declares the LF types and constants that represent the syntax of the object language. For example, we can represent the syntax of the natural numbers with the following LF signature:

%sort nat
%term z nat
%term s %pi nat %-> nat

Intuitively, the LF type nat classifies the LF representations of natural numbers. The LF constant z corresponds to $\mathsf{zero}$ and the LF constant s corresponds to $\mathsf{succ}$.

• The signature declares that z has type nat, which makes sense because $\mathsf{zero}$ is a natural number.

• The signature declares that s has function type %pi nat %-> nat. An LF term of function type can be applied to another LF term of the appropriate type to form a new term. For example, the constant s can be applied to the constant z to form the term s z representing the number $\mathsf{succ}(\mathsf{zero})$. Then s can be applied to this term to form s (s z), and so on. An informal natural number $\mathsf{succ}(n)$ is represented by the LF term s N where $n$ is represented by N.

We can state the relationship between the informal presentation of the object language and its LF representation by giving an encoding judgement relating an informal object with its representation:

$${ {\,} \over {\mathsf{0} \leadsto \mathtt{z}} } \qquad { {n \leadsto n' } \over {\mathsf{succ}(n) \leadsto \mathtt{s}(n')} }$$

Adequacy

TODO

Footnotes

1. $\Gamma$ being a metavariable representing the context, and $n$ being a term metavariable. ↩

2. for those familiar with the Lambda Cube, LF is the canonical fragment of the $\lambda\Pi$ calculus. ↩