An Extensible Proof Text Editor

Thomas Hallgren and Aarne Ranta

Introduction

Computer algebra systems, such as Mathematica [mathematica-homepage] and Maple [maple-homepage], are widely used by mathematicians and students who do not know the internals of these systems. Proof editors, such as Coq [coq-homepage], LEGO [LEGO-homepage], Isabelle [Isabelle-homepage], and ALF [magnusson:phd], are less widely used, and require more specialized knowledge than computer algebras. One important reason is, of course, that the structures involved in manipulating algebraic expressions are simpler and better understood than the structures of proofs, and typically much smaller. This difference is inescapable, and it may well be that formal proofs will never be as widely interesting as formal algebra. At the same time, there is one important factor of user-friendliness that can be improved: the language used for communication with the system. While computer algebras are reasonably conversant in the ``ordinary language'' of mathematics, that is, expressions that occur in ordinary mathematical texts, proof editors only read and write artificial languages that are designed by logicians and computer scientists but not used in mathematical texts.

Making proof editors conversant in the language of ordinary proofs is clearly a more difficult task than building support for algebraic expressions. There are two main reasons for this: first, ordinary algebraic symbolism is quite formal already, and reflects the underlying mathematical structures more closely than proof texts in books reflect the structure of proofs. Second, the realm of proofs is much wider than algebraic expressions, which is already shown by the fact that proofs can contain arbitrary algebraic expressions as parts and that they also contain many other things.

We are far from a situation in which it is possible to take an arbitrary mathematical text (even a self-contained one) and feed it into a proof editor so that the machine can check whether the proof is correct, or even return a list of open problems if the proof contains leaps too long for the machine to follow. What is within reach, however, is a restricted language at the same time intelligible to non-specialist users, formally defined, and implemented on a computer. With such a language, it is not guaranteed that the machine understands all input that the user finds meaningful, but the machine will always be able to produce output meaningful for the user.

The idea of a natural-language-like formal language of proofs was presented by de Bruijn under the title of Mathematical Vernacular [deBruijn:MV]. Implementations of such languages have been made in connection with at least Coq [coscoy:textproofs], Mizar [Mizar-homepage], and Isabelle [Isabelle-homepage]. Among these implementations, it is Coq that comes closest to the idea of having a language of proofs, in the same sense as type theory: a language in which proofs can be written, so that parts of the proof text correspond to parts of the formal proof. The other languages reflect the proof process rather than the proof object: they explain what commands the user has given to the machine, or what steps the machine has made automatically, when constructing the proof. While sometimes possibly more useful and informative than a text reflecting the proof object (because it communicates the heuristics of finding the proof), a description of the proof process is more system-dependent and less similar to ordinary proof texts than a description of the proof object.

Like the ``text extraction'' functionality of Coq [coscoy:textproofs], the present work aims to build a language of proofs whose structures are similar to the structures of proof objects. The scope of the present work is wider in certain respects:

• We do not only consider proofs but propositions and definitions as well.
• Our language can be used not only for output but for input as well ( An extension of the Coq interface [coscoy:thesis], however, has a reversible translation of proofs to texts.).
• Our language can be extended by the user in the same way as proof editors are extended by user-defined theories.

• We do not study automatic optimizations of the text.

The focus of this paper is on the architecture and functionalities of a natural language interface to a proof editor. Little will be said about the linguistic questions of mathematical texts; some of the linguistic background work can be found in [ranta:torino,ranta:paris].

Proof Editors, Type Theory and Functional Programming

Alfa [hallgren:alfa-homepage] is a graphical, syntax-directed editor for the proof system Agda. Agda [agda-homepage] is an implementation of structured type theory (STT) [coquand:stt-lfm99], which is based on Martin-Löf's type theory [martin-lof:padova]. The system is implemented completely in Haskell, using the graphical user interface toolkit Fudgets [carlsson98:fudgets_thesis].

Like its predecessors in the ALF family of proof editors [magnusson:phd], Alfa allows the user to, interactively and incrementally, define theories (axioms and inference rules), formulate theorems and construct proofs of the theorems. All steps in the proof construction are immediately checked by the system and no erroneous proofs can be constructed.

Alternatively, since Martin-Löf's type theory is a typed lambda calculus, one can view Alfa as a syntax-directed editor for a small purely functional programming language with a powerful type system.

1introexample gives an idea of what the system looks like.

introexample A window dump of Alfa.

The user has defined the natural numbers and is working on the definition of addition. Question marks are metavariables, also called place holders, and allows the user to make a definition by starting from a skeleton and gradually refine it into a complete definition in a top down fashion. When a metavariable is selected, its type is displayed at the bottom of the window, and the menu indicates which ones of the identifiers in scope may be used to construct an expression of the required type.

ndexample A natural deduction proof in progress in Alfa.

In virtue of being based on Martin-Löf type theory, STT can draw on the Curry-Howard isomorphism and serve as a unified language for propositions and proofs, specifications and programs. This allows Alfa to be used many ways:

• As a tool for pure logic. Alfa has in fact been used in undergraduate courses, allowing the students to practice doing natural deduction style proofs in propositional logic and predicate logic. As shown in 1ndexample, Alfa has a mode of editing where terms are displayed as natural deduction style proof trees.

• As a tool for functional programming with dependent types. The language STT is closely related (The differences are to some extent due to the fact that Cayenne was designed to be used with an ordinary text editor and a batch compiler, whereas STT is designed for use in interactive proof editors.) to the language Cayenne [augustsson:cayenne], a full-fledged functional programming language with dependent types.

• As a tool for programming logic. The power of the language makes it possible to express both specifications and programs and to construct the proofs that the programs meet their specifications.

The Grammatical Framework

GF (Grammatical Framework) [GF-homepage] is a formalism for defining grammars. A grammar consists of an abstract syntax and a concrete syntax. The abstract syntax is a version of Martin-Löf's type theory, consisting of type and function definitions. The concrete syntax is a mapping of the abstract syntax, conceived as a free algebra, into linguistic objects. The mapping of a functional term (= abstract syntax tree) is called its linearization, since it is the flattening of a tree structure into a linear string. To give an example, the following piece of abstract syntax defines the category CN of common nouns, and two functions for forming common nouns:

  cat CN
  fun Int : CN
  fun List : CN -> CN

  param Num = sg | pl
  lincat CN = {s : Num => Str}

  lin Int = {s = tbl {{sg} => "integer" ; {pl} => "integers"}}

  oper regCN : Num => Str = 
    \str -> tbl {{sg} => str ; {pl} => str + "s"}

  lin Int = {s = regCN "integer"}
  lin List A = {s = tbl {n => regCN "list" ! n ++ "of" ++ A.s!pl}}

List (List Int)

 {s = tbl {
       {sg} => ["list of lists of natural numbers"] ;
       {pl} => ["lists of lists of natural numbers"]}}

The concrete-syntax part of a grammar can be varied: for instance, the judgements

  param Num = sg | pl
  param Gen = masc | fem
  oper regCN : Num => Str = 
    \str -> tbl {{sg} => str ; {pl} => str + "s"}
  oper de : Str = 
    pre {"de" ; "d'"/strs {"a";"e";"i";"o";"u";"y"}}
  lincat CN = {s : Num => Str ; g : Gen}
  lin Int = {s = regCN "entier" ; g = masc}
  lin List A = 
    {s = tbl {n => regCN "liste" ! n ++ de ++ A.s ! pl ; g = fem}}

The class of grammars definable in GF includes all context-free grammars but also more ( The most important departure from context-free grammars is the possibility to permute, reduplicate, and suppress arguments of syntactic constructions. Rules using parameters, although conceptually non-context-free, can be interpreted as sets of context-free rules.). Thus GF is applicable to a wide range of formal and natural languages. The implementation of GF includes a generic algorithm of linearization, but also of parsing, that is, translating from strings back to functional terms ( The parsing algorithm is context-free parsing with some postprocessing. Suppressed arguments give rise to metavariables, which, in general, can only be restored interactively. ).

GF-Alfa: an Interface to Alfa

The GF interface to Alfa consists of two kinds of GF grammars:

• Core grammars, defining the translations of framework-level expressions.

• Syntactic annotations, defining translations of user-defined concepts.

The syntactic categories of the interface are, essentially, those of the syntax of type theory used in the implementation of Alfa. The most important ones are expressions, constants (=user-defined expressions), and definitions:

  cat Exp ; Cons ; Def

  param ExpForm = cn Num | sent | pn | text ; Num = sg | pl
  lincat Exp = {s : ExpForm => Str}

  lin emptySet = {s = tbl {
    (cn {sg}) => ["element of the empty set"] ;
    (cn {pl}) => ["elements of the empty set"] ;
    {sent}    => ["the empty set is inhabited"] ;
    {pn}      => ["the empty set"] ;
    {text}    => ["we use the empty set"]}}

  oper mkPN : Str -> {s : ExpForm => Str} = \str -> {s = tbl {
    (cn {sg}) => ["element of"] ++ str ;
    (cn {pl}) => ["elements of"] ++ str ;
    {sent}    => str ++ ["is inhabited"] ;
    {pn}      => str ;
    {text}    => ["we use"] ++ str}}
  lin emptySet = mkPN ["the empty set"]

  lin emptySet = {s = tbl {
    (cn {sg}) => ["impossible element"] ;
    (cn {pl}) => ["impossible elements"] ;
    {sent}    => ["we have a contradiction"] ;
    {pn}      => ["the empty set"] ;
    {text}    => ["we use the empty set"]}}

The abstract syntax of the core grammars is extended every time the user defines a new concept in Alfa. The extension is by a function whose value type is Cons. For instance, the Alfa judgement

  List (A::Set) :: Set = ...

  fun List : Exp -> Cons

  lin List A = mkPN ("List" ++ A.s ! pn)

  lin List A = 
    mkCN (tbl {n => regCN "list" ! n ++ "of" ++ A.s ! (cn pl)})

The reading given to proofs is not different from other type-theoretical objects. For instance, the conjunction introduction rule, which in Alfa reads

  ConjI (A::Set)(B::Set)(a::A)(b::B) :: Conj A B = ...

  lin ConjI A B a b = mkText (
    a.s ! text ++ "." ++ b.s ! text ++ "." ++ 
    "Altogether" ++ A.s ! sent ++ "and" ++ B.s ! sent)

On the top level, an Alfa theory is a sequence of definitions. Even theorems with their proofs are definitions of constants, which linguistically correspond to names of theorems. The linearization of a definition depends on whether the constant defined is intrinsically a proper name, common noun, etc. This intrinsic feature is by default proper name, but can be changed in a syntactic annotation. In the following section, examples are given of definitions of common nouns (``natural number'') and proper names (``the sum of a and b''). Section 8 shows a definition of a constant conceived as the name of a theorem.

Natural Language Output

The primary and most basic function of GF in Alfa is to generate natural language text from code. Any definition or expression visible in the editor window can be selected and converted into one of the supported languages by using a menu command.

As an example, the default linearization of the (completed) definitions shown in 1introexample would be as follows:

By adding the following grammatical annotations,

   Nat     = mkRegCN ["natural number"]
   Zero    = mkPN "zero"
   Succ n  = mkPN (["the successor of"] ++ n.s ! pn)
   (+) a b = mkPN (["the sum of"] ++ a.s!pn ++ "and" ++ b.s!pn)

and similar grammatical annotations for Swedish and French, we obtain the following versions of the above definitions:

Definition. A natural number is defined by the following constructors:
- zero
- the successor of n where n is a natural number.
Definition. Let a and b be natural numbers. Then the sum of a and b is a natural number, defined depending on a as follows:
- for zero, choose b
- for the successor of n, choose the successor of the sum of n and b.

Définition. Les entiers naturels sont définis par les constructeurs suivants :
- zéro
- le successeur de n ou n est un entier naturel.
Définition. Soient a et b des entiers naturels. Alors la somme de a et de b est un entier naturel, qu'on définit dépendant de a de la manière suivante :
- pour zéro, choisissons b
- pour le successeur de n, choisissons le successeur de la somme de n et de b.

Definition. Ett naturligt tal definieras av följande konstruerare:
- noll
- efterföljaren till n där n är ett naturligt tal.
Definition. Låt a och b vara naturliga tal. Summan av a och b är ett naturligt tal, som definieras beroende på a enligt följande:
- för noll, välj b
- för efterföljaren till n, välj efterföljaren till summan av n och b.

It is possible to switch between the usual syntax, different language views and multilingual views by simple menu commands.

Symbolic parts of natural-language expressions

Using natural language in every detail is not always desirable. A more suitable expression for addition, for instance, would often be

   (+') a b = mkPN (a.s ! pn ++ "+" ++ b.s ! pn)

the successor of zero + 2.

   param Formality = symbolic | verbal
   param ExpForm = ... | pn Formality | ...

   Zero    = mkPN "zero" "0"
   (+) a b = mkPN 
     (["the sum of"] ++ a.s!(pn verbal) ++ "and" ++ b.s!(pn verbal))
     (a.s!(pn symbolic) ++ "+" ++ b.s!(pn symbolic))

   MkSymbolic A a = mkPN (a.s!(pn symbolic)) (a.s!(pn symbolic))

   MkSymbolic (A::Type)(a::A) = a

Natural Language Input

In addition to obtaining natural language output, you can also use the parsers automatically generated by GF to enter expressions in natural language. This way, you can make definitions without seeing any programming language syntax at all. As a simple example, suppose you want to add a definition of one as the successor of zero. By using the command to add a new definition, you get a skeleton:

The first hole to fill in is the type of one. You can use the commands ``Give in English'', ``Give in French'', ``Give in Swedish'':

The last step is to enter the body of the definition,

and the final result is:

The parser understands only the fragment of natural languages we have defined, but can actually correct minor grammatical errors in the input. A completion mechanism helps in finding accepted words. The smiley in the input window gives feedback from the parser.

Since GF covers arbitrary context-free grammars (and more), it is possible for the concrete syntax to be ambiguous. When an ambiguous string is entered, Alfa asks the user to choose between the resulting alternative terms.

Ambiguous structures belong intimately to natural language, including the informal language of mathematics. Banning them from the proof editor interface would thus be a drastic limitation. Syntactic ambiguity is not so disastrous as one might think: careful writers use potentially ambiguous expressions only in contexts in which they can be disambiguated. The disambiguating factor is often type checking. For instance, the English sentence

for all numbers x, x is even or x is odd

(∀x ∊N)(Ev(x) ∨Od(x)),

(∀x ∊N)Ev(x) ∨Od(x).

Since the annotation language of GF permits the user to introduce ambiguous structures, the parsing facility plays an important role even in natural language output: the question whether a text generated from a proof is ambiguous can be answered by parsing the text. Even a user who does not care about the natural language input facility of GF-Alfa may want to use the GF parser to find ambiguities in natural language output.

An Example: Insertion Sort

As a small, but non-trivial, example where GF and many features of Alfa are used together, we show some fragments from a correctness proof of a sorting algorithm.

We have defined insertion sort for lists of natural numbers in the typical functional programming style:

The English translation of the definition of sort is

As a specification of the sorting problem, we use the following:

We have chosen ``ys is a sorted version of xs'' as the English translation of SortSpec xs ys. The body of SortSpec translates to ``ys is a permutation of xs and ys is sorted''.

After proving some properties about permutations and the insert function, we can fairly easily construct the correctness proof for sort by induction on the list to be sorted. The proof is shown in natural deduction style in 1sortiscorrectnd.

sortiscorrectnd The correctness proof for insertion sort. See section sorting-example.

The specification SortSpec xs ys is defined to mean that ys is a permutation of xs, denoted xs ~ys, and ys is sorted, denoted IsSorted ys.

The same proof can also be viewed in English. The beginning of it is: (We omit the rest of the proof for the time being. Some fine tuning is needed to make the text look really nice.)

Using the above proof, we can easily prove the proposition

The English translation of the proof is:

Conclusion

While Alfa dates back to 1995 and GF to 1998, the work on GF-Alfa only started at the end of 1999. It has been encouraging that the overall concept of integrating GF and Alfa works. Moreover, there is nothing particular to Alfa that makes this type of interface work; an earlier interface with the same architecture (i.e. core grammar + syntactic annotations) was built for the completely different formalism of extended regular expressions [ranta98:regexp]. Similar lessons can be learnt from both systems:

• Formal structures can be mapped to natural-language structures so that arbitrarily complex expressions always give grammatically correct results. Thus it is possible to translate from formal to natural languages.

• Complex expressions are harder to understand in natural than in formal languages. Thus it is important to structure the code and break it into small units (such as lemmas), in order for the resulting text to be readable.

• It is useful to define equivalent variants of formal objects and equip them with different linearization rules. In this way stylistic variation can be included in the text. Linearization rules can also implement different degrees of information hiding.

• Natural-language input is only useful for small expressions, since entering a long expression runs the risk of falling outside the grammar.

• The interactive construction of a formal object is helped by a simultaneous view of the object as informal text.

• Ambiguities need not be forbidden in natural language, since they can be handled by interaction. Moreover, syntactic ambiguities are often automatically resolved by type checking.