Using the GF plug-in to produce Natural Language Translations of Formal Proofs

By using the GF plug-in, formal proofs developed in Alfa can be translated to natural language. Currently, translations to English, French and Swedish are available, and more languages can be added by the user (but some linguistic knowledge and familiarity with GF is required).

The GF plug-in knows how to translate all Alfa built-in syntax (the various forms of definitions and expressions), and provides default translations of user-defined identifiers. However, to obtain nice text, the user is expected to provide sutiable translations along with any new definitions introduced in a proof. These translations are specified by adding grammatical annotations to definitons. The grammatical annotions are written in a simple language provided by GF.

An example

To activate the GF plugin, start Alfa with the following command:
alfa - -plugins GF
As a simple example, let's see how to translate the definition of natural numbers and addition of natural numbers to English. We start by defining these things in the usual way in Alfa:

[Def of Nat and +]

We can already obtain an English translation of this. By selecting GF: Eng as the default declaration view from the View menu, we get the following:

[GF: Eng view before adding grammatical annotations]

It is also possible to select definition(s) and apply commands from the menu window to choose how to present them, e.g., GF: Show in Eng, GF: Show all translation, Show default declaration view. You can also select parts of expressions and apply similar commands to them.

The next step is to tell GF how to translate Nat and + to English.

We start by considering the translation of Nat. Names of data types (sets) are usually translated into nouns. In this case we want to use the phrase natural number. Nouns may be used in both singular and plural forms, so the translation have to indicate both forms. Fortunately, the grammatical annotation language provides some auxiliary functions to make this easy. In the case of regular nouns, for which the plural form is obtained by adding an s to the end of the word, it is particularly easy.

To enter the translation of Nat in Alfa, select the definition of Nat (or just the name in the LHS of the definition) and choose the command GF: Change Eng translation of Nat in the menu window. You should now see a text editor window containing the default translation of Nat:

[Editor with default grammatical annotation for Nat]

We can now replace the default translation with the desired one:

[Editor with user provided grammatical annotation for Nat]

Note that strings enclosed in quotes (") should contain single words and that the operator ++ is used to form phrases containg more than one word. The function regCN takes care of adding an s to the last word of the argument phrase, in the places where it is used in the plural form.

When we press OK, the translation of the definitions in the main window will be updated accordingly:

[Main window with improved translation of Nat]

Note that Nat is appropriately translated to a natural number or natural numbers depending on the context.

We continue with the translation of the constructors Zero and Succ. (To be able to select them and edit their translations, you probably first have to switch back the declaration view to Complete definitions.)

While the names of sets behave like nouns, constructors and other elements of sets behave more like proper names. For Zero and Succ, we enter the following translations:

Zero@_ = mkPN "zero"
Succ@_ n = likeSucc "successor" n
The function mkPN creates simple proper names and likeSucc constructs phrases like the xxx of yyy, where xxx is a word and yyy is another proper name:

Finally, we add a translation for the operator +. We choose to translate a+b to the phrase the sum of a and b, which can be used as a proper name.

+ a b = likeSum "sum" a b
We now have completed our example, and the final translation to English is:

[Final English translation of Nat and +]

Known bugs and limitations

See Also

5 Jul 2012 19:45 Thomas Hallgren