[Document under construction]

Alfa - User's Guide

Last updated: 25 June 2001

Introduction

Alfa is a WYSIWYG proof editor. It allows you 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. The logical framework used is Agda, implemented by Catarina Coquand, based on work by Thierry Coquand. It is a version of Per Martin-Löf's Type Theory.

Alternatively, you can view Alfa as a syntax-directed editor for a small purely functional programming language with a type system that provides dependent types. In fact, the functional language is very similar to the language Cayenne by Lennart Augustsson.

This document describes how to use the WYSIWYG editor, but it does not explain Type Theory.

Warnings

Before you start playing with Alfa, please note that Alfa is currently under development and that you are using a test version only. Beware that Alfa

Fore more details, see Limitations of the current version.


Contents


Using Alfa

Starting and stopping Alfa

Alfa is started with the command

alfa [ rtflags ] [ - flags ]

where

rtflags
is an optional list of flags for the Haskell run-time system. A useful flag is -HheapsizeM, which sets the heap size to heapsize megabytes. The default is 30 (25 in older versions), which is enough for editing small documents. A 30MB heap is too big if you run Alfa on a computer with 32MB of RAM or less.
flags
is an optional list of flags interpreted by Alfa. For details, see Command line syntax. Notice the single - preceding these flags.

Alfa can be stopped by selecting the Quit command from the File menu.

Windows and Menus

When Alfa is started it opens two windows:

[Main Editing Window] [Menu Window]

Closing the main editing window is the same as quitting Alfa. Closing the menu window causes it to disappear, but you can get it back with a command in the Utils menu.

The size of the info display at the bottom of the main editing window is adjusted automatically to fit the currently displayed message, but you can also resize it manually by dragging the separating line.

Keyboard shortcuts

The commands shown in the various menus can be executed by selecting them using the mouse, but most of them also have keyboard shortcuts that can be used instead.

Loading and saving files - the File menu

The File menu in the editing window contains the following items: [File menu image]


Editing

Alfa allows you to edit a document, which is a sequence of declarations. A declaration is a group of (possibly) mutually recursive definitions. A definition associates a name with a type and a value of that type (x = a : A). (The syntax and meaning of expressions follow Agda's definitions and is not covered in this document.) The names introduced in a declaration are in scope in that declaration and following declarations.

The two most common editing operations are probably adding declarations and filling in place holders (instantiating meta variables). The former is explained below. The latter can be done in many ways, as noted on the quick reference page Top 10 ways to fill in a place holder.

Adding and deleting declarations

You can add a new declaration to the end of the document by selecting the command New Declaration from the Edit menu in the editing window. You will then have to enter the names to be defined in the declaration in a pop-up window. The names should be separated by commas. You can also include the names of formal parameters in the list.

You can also add declarations in arbitrary places in the document by clicking in the empty space just above or below an existing declaration and then selecting the command Insert New Declaration in the menu window and proceeding as above. (Note: this way of adding declaration is less efficient since is not directly supported in the proof engine and requires the entire module to be rechecked.)

Provided the names defined in a declaration are not in use, the declaration can be deleted by selecting it and executing the Delete operation (which is shown in menu window). You can actually delete a declaration, even if the names are in use. Affected declaration will then be marked with an error bar.

Selecting and operating

Most editing is done by selecting a part of the document, usually a place holder, declaration or expression, and performing an editing operation on it. Applicable editing operations are displayed in the menu window. They can be executed by clicking on them or by typing the key combination shown in square brackets. (Note: the keyboard shortcuts are generated dynamically, so the same alternative may be assigned different keys in different contexts.) Further editing operations are provided in the Edit menu.

Note: some of the commands in the Edit menu may not be applicable, but there is no visual feedback for this in the current version.

By clicking at some point in the editing window you select the smallest syntactic unit containing that point. You can also use the following keys:

Cut-and-Paste editing

Cut-and-Paste editing works in much the same way as in other programs.

The currently selected part of the document can be copied to the (invisible) clipboard by executing the Copy command in the Edit menu. It can then be pasted in other places in the document. It can also be pasted in other X Windows programs, e.g., emacs, usually by pressing the middle mouse button (in emacs you can also use C-y). When a place holder is selected and the clipboard contains an expression of a suitable type, the place holder can be replaced with the expression by executing the Paste command in the Edit menu. A syntax error may occur if the clipboard contains some text (from a text editor) that does not form a syntactically correct expression.

You can paste a declaration when the empty space immediately above or below a declaration is selected and the clipboard contains a declaration.

You can also paste on top of existing expressions and declarations. If a type error occurs, you get an error bar.

Adding and deleting constructors

You add new constructors to an existing data type by selecting the data expression and picking the command Add constructor from the menu window. After this, you probably also need to add branches for the new constructors in some case expressions. This is done in the same way, i.e., select the case expression and pick the command Add branch from the menu window.

The type checker may not accept case expression that aren't exhaustive, so adding a constructor to a data type may give rise to an error, causing declarations containing affected case expressions to be marked with an error bar. It is still possible to add a branch for the new constructor.

It is also possible to delete branches from case expressions and constructors from data types. To do this, select the branch or constructor and pick the Delete command from the menu window (or the Edit menu). Deleting a constructor that is still in use somewhere will cause affected declarations to be marked as erroneous.

Entering the text representation

In some situations, e.g., when using the Give command and when constructing case expressions, you have to enter expressions as text. The syntax to use in these cases is the same syntax Alfa uses for storing documents in files. (See the documentaton of Agda for details.) This means for example that constructors should be suffixed with @_ and that you can not leave out hidden arguments. You can use place holders (? or {| |}) for subexpressions you don't want to fill in.

User Defined Layout

Alfa currently provides the following ways for the user to influence the layout:

About Argument hiding

Terms in the monomorphic type theory often contain a lot of redundant type information. This type information is often inferred by the proof engine and does not have to be filled in by the user. The argument hiding mechanism is provided as a way of hiding some redundant information and thereby making the terms smaller and more readable.

You can set the number of hidden arguments for an identifer as described below. In expressions where an identifier with n hidden arguments is applied to some arguments, the first n arguments will be invisible. (In earlier versions of Alfa, they were represented by a °, allowing you to see that there was something hidden.)

Note that argument hiding is a lexical property of an identifier and is not connected to the scope of a certain binding.

The View menu contains commands for switching on and off the argument hiding mechanism.

As an example of the effect of argument hiding, consider the definition of the list function map:

Without argument hiding With 2 hidden arguments
[Def of map without argument hiding] [Def of map with 2 hidden arguments]

Setting the layout options for an identifier

The layout options for an identifier can be edited by clicking on a binding occurence of the identifier and choosing the command Change layout options shown in the menu window. This pops up a window where you can change the various options.

[Layout editor window]

The layout options show in this window, from top to bottom are:

Number of hidden arguments
Enter a number here to set the number of hidden arguments.
Display As
If present, the string entered in this field will be shown instead of the real name of the identifier. This string can be any combination of characters, not just legal identifiers, and it does not affect the abbreviations shown in the menu window.

Use Symbol Font
The identifier will be displayed using the symbol font instead of the ordinary font.

Use Image File
The string entered in the Display As: field is interpreted as the name of a file containing an image in the xbitmap format to show intstead of the real name.

Nonfix/Infix/Postfix
This affects how an application of the identifier to some arguments are displayed:

NonfixInfixPostfix
opopop
op x(x op)x op
op x yx op y(x op) y
op x y z(x op y) z(x op) y z

Infix ternary/Infix 4ary
These options are like Infix but arguments are also put above and/or below the operator.
Quantifier
This option switches on quantifier notation. A quantifiers is a function that normally is applied to a lambda abstraction. For example, the application Forall (\(x::A)->B x), could appear as Forall x:A . B x. The domain of quantification can be shown, as in this example, or be hidden.

Big Operator
This option causes applications of the form f a b c to be displayed as
b
fc
a
and applications of the form f a b (\ i -> c) to be displayed as
b
fc
i=a
Tuple
This options shows the arguments of the function in angle brackets, separated by commas. The name of the function will not be visible.
Fraction
For functions applied to two arguments, this option displays the argument vertically, separated by a horizontal line. The name of the function will not be visible.
Mixfix operator
This option allows you to interleave arguments and arbitrary strings. The arguments will be inserted in place of _ characters in the name of the function (or the Display As string, if given). For example, the application
if_then_else_ x y z
would be displayed as
if x then y else z

It is also possible to use digits to refer to arguments at specific positions. For example, by changing the Display As string for the above function to

2 if 1, 3 otherwise
the same application would be displayed as
y if x, z otherwise
Associativity and precedence
This affects where parentheses are insterted when expressions contain nested applications of infix/mixfix/distfix operators.

Compact Notation

The View menu contains commands for switching on and off compact notation. In the current version, compact notation means that function types and lambda expressions are abbreviated:

Full notation Compact notation
(a:A) -> (b:B) -> C (a:A,b:B) -> C
(a:A) -> (b:A) -> C (a,b:A) -> C
\ x -> \ y -> e \ x y -> e

It also causes nested case expressions to be displayed in a more compact way. Definitions where the right hand side is a case expression is displayed in an equational style. Nested case expressions are displayed as nested patterns.

Example:
NormalCompact
[Nested case expression] [Nested pattern]
[Definition with case expression] [Equational definition]

Bug warning: some editing operations don't work properly when compact notation is in use, so you might want to turn it off temporarily. For example, if you change (a,b:A)->C to (a,b:B)->C you will see (a,b:B)->C, but you will get (a:B,b:A)->C.

Proof Style

Provided they are constructed in a certain way, proofs can be presented in natural deduction style, and other similar styles. See the separate tutorial on Natural Deduction Style Proofs for further details.

Evaluating Expressions

The command Evaluate Expressions in the Utils menu pops up a window where you can enter expressions to be evaluated. The expressions have to entered as text (as explained above). When a place holder is selected, the expressions will be evaluated in the context of that place holder. Otherwise they will be evaluated in the top level context (i.e., all identifiers defined on the top level are in scope).

Note: there is a termination test, so if you try to evaluate an expression that doesn't terminate, or one that requires too many computation steps, you will get an error message.

[Evaluate Expressions
Window]

The arrow buttons in this window allow you to step back and forth in the evaluation (the < and > buttons) or go directly to the original form and the normal form of the expression (the << and >> buttons).

Error Handling

Syntax Errors

Since Alfa is a syntax directed editor, it is not possible to construct syntactically incorrect documents. However, text representing expressions or other syntactic entities can of course contain errors and can enter the system in the following ways:

Type Errors

Everything entered into Alfa is immediately type checked, so it is usually impossible to create type incorrect documents. However, there are some cases when editing operations that lead to type errors are allowed:

The Error Bar

The error bar is a red vertical bar to the left of a declaration. It indicates that the type checking of the declaration (or some declaration preceeding it) has failed and that it has been left in an unchecked state.

When a declaration is in the unchecked state, only limited editing operations are available inside it. In particular, you can not see the type of place holders, and things you fill in aren't type checked. After making some changes, you can use the command Check Again to have the type checker re-check the declaration and, if the error has been corrected, return it to the normal, type checked state.


8 Jan 2003 05:02 Thomas Hallgren