Abstract of Licenciate Thesis
Programming in Martin-Löf Type Theory: Unification - A non-trivial Example.
Martin-Löf type theory is a constructive type theory originally conceived as a formal language in which to carry out constructive mathematics. However, it can also be viewed as a programming language where specifications are represented as types and programs as objects of the types. In this work, the use of type theory as a programming language is investigated. As an example, a formalisation of a unification algorithm for first-order terms is considered.
Unification can be seen as the process of finding a substitution that makes all the pairs of terms in an input list equal, if such a substitution exists. Unification algorithms are crucial in many applications, such as type checkers for different programming languages. Unification algorithms are total and recursive, but the arguments on which the recursive calls are performed satisfy no syntactic condition that guarantees termination. This fact is of great importance when working with Martin-Löf type theory since there is no direct way of formalising such an algorithm in the theory.
The standard way of handling general recursion in Martin-Löf type theory is by using the accessibility predicate Acc which captures the idea that an element a in A is accessible if there exists no infinite decreasing sequence starting from a. As this is a general predicate, it contains no information that can help us when formalising a particular general recursive algorithm, and then its use in the formalisation of the unification algorithm produces an unnecessarily long and complicated algorithm. On the other hand, functional programming languages like Haskell impose no restrictions on recursive programs, and then writing an algorithm like the unification algorithm is straightforward. In addition, functional programs are usually short and self-explanatory. However, there does not exist a powerful framework that allows us to reason about the correctness of Haskell-like programs.
Then, the goal of this work is to present a methodology that combines the advantages of both programming styles and that can be used for the formalisation of the unification algorithm. In this way, a short algorithm that can be proven correct by using the expressive power of constructive type theory is obtained.
The main feature of the methodology presented here is the introduction of an inductive predicate, specially defined for the unification algorithm, that can be thought of as defining the set of \lspt for which the algorithm terminates. This predicate contains an introduction rule for each of the cases that need to be considered and provides an easy syntactic condition that guarantees termination. The information contained in this predicate simplifies the formalisation of both the algorithm and the proof of its partial correctness. In this way, both the algorithm and the proof are short, elegant and easy to follow. In addition, it is possible to define a methodology that extracts a Haskell program from the type theory formalisation of the unification algorithm that is defined by using this special-purpose predicate.