Introduction to Programming in ATS:
Prev		Next

Chapter 12. Programming with Theorem-Proving

Table of Contents
Circumventing Nonlinear Constraints
Example: Safe Matrix Subscripting
Specifying with Enhanced Precision
Example: Another Verified Factorial
Example: Verified Fast Exponentiation

Programming with Theorem-Proving (PwTP) is a rich and broad programming paradigm that allows cohesive construction of programs and proofs in a syntactically intwined manner. The support for PwTP in ATS is a signatory feature of ATS, and the novelty of ATS largely stems from it. For people who are familiar with the so-called Curry-Howard isomorphism, I emphasize that PwTP as is supported in ATS makes little, if any, essential use of this isomorphism (between proofs and programs): The dynamics of ATS in which programs are written is certainly not pure and the proofs encoded in ATS/LF are not required to be constructive, either. However, that proof construction in ATS can be done in a style of (functional) programming is fundamentally important in terms of syntax design for ATS, for the need to combine programs with proofs would otherwise be greatly more challenging.

In this chapter, I will present some simple but convincing examples to illustrate the power and flexibility of PwTP as is supported in ATS. However, the real showcase for PwTP will not arrive until after the introduction of linear types in ATS, when linear proofs can be combined with programs to track and safely manipulate resources such as memory and objects (e.g, file handles). In particular, PwTP is to form the cornersone of the support for imperative programming in ATS.

Please find on-line the code employed for illustration in this chapter plus some additional code for testing.

Circumventing Nonlinear Constraints

The constraint-solver of ATS is of rather diminished power. In particular, constraints containing nonlinear integer terms (e.g., those involving the use of multiplication (of variables)) are immediately rejected. This weakness must be properly addressed for otherwise it would become a crippling limitation on practicality of the type system of ATS. I now use a simple example to demonstrate how theorem-proving can be employed to circumvent the need for handling nonlinear constraints directly.

A function template list_concat is implemented as follows:

//
// [list_concat] does typecheck in ATS2
// [list_concat] does not typecheck in ATS1
//
fun{
a:t@ype
} list_concat{m,n:nat}
(
  xss: list (list (a, n), m)
) : list (a, m * n) =
  case+ xss of
  | list_nil () => list_nil ()
  | list_cons (xs, xss) => list_append<a> (xs, list_concat xss)
// end of [list_concat]

where the interface for list_append is given below:

fun{
a:t@ype
} list_append {n1,n2:nat}
  (xs: list (a, n1), ys: list (a, n2)): list (a, n1+n2)

Given a list xss of length m in which each element is of the type list(T,n) for some type T, list_concat<T>(xss) constructs a list of the type list(T,m*n). When the first matching clause in the code for list_concat is typechecked, a constraint is generated that is essentially like the following one:

m = m1 + 1 implying n + (m1 * n) = m * n holds for all natural numbers m, m1 and n.

This contraint may look simple, but it was once rejected by the ATS constraint solver as it contains nonlinear integer terms (e.g., m1*n and m*n). In order to overcome (or rather circumvent) the limitation, we can make use of theorem-proving. Another implementation of list_concat is given as follows:

fun{
a:t@ype
} list_concat{m,n:nat}
(
  xss: list(list(a, n), m)
) : [p:nat] (MUL(m, n, p) | list(a, p)) =
(
//
case+ xss of
| list_nil () =>
    (MULbas() | list_nil())
| list_cons (xs, xss) => let
    val (pf | res) = list_concat (xss)
  in
    (MULind pf | list_append<a> (xs, res))
  end // end of [list_cons]
//
) (* end of [list_concat] *)

Given a list xss of the type list(list(T,n),m), list_concat(xss) now returns a pair (pf | res) such that pf is a proof of the prop-type MUL(m,n,p) for some natural number p and res is a list of the type list(T,p), where the symbol bar (|) is used to separate proofs from values. In other words, pf acts as a witness to the equality p=m*n. After proof erasure is performed, this implementation of list_concat is essentially translated into the previous one (as far as dynamic semantics is concerned). In particular, there is no need for proof construction at run-time.

Prev	Home	Next
Programmer-Centric Theorem-Proving	Up	Example: Safe Matrix Subscripting