Gentzen

Gentzen is an alternative syntax for proofs in the LK sequent calculus, with several shortcuts. O, actually, it is a programming language.

Syntax

• Name: Consists of ASCII letters, numbers, and underscores, without starting with a digit. An underscore by itself is not a valid name either. The name is case-sensitive.
• Number: Number written in decimal, or in hex with 0x at front, or in octal with 0o at front. Hex digits have to be uppercase but the 0x and 0o at front has to be lowercase. There are no negative numbers. You can also use apostrophe before and after some ASCII character for its ASCII code.
• String: A string literal in quotation marks. It is considered to be a list of numbers.
• Comments: Start with # followed by a exclamation mark or space, and last until the end of the current line of input.

Numeric and string literal values can be used as if rules of types () / (|- |\|) and () / (|- .. |\|).

Object types:

• ~ x - A continuation accepting a value of type x.
• x /\ y - Contains both x and y.
• x \/ y - Contains either x or y (not both).
• @ x - A potentially infinite loop that results in x if it halts.
• |\| - Natural numbers.
• ++ - Type with only one possible value.
• _|_ - Similar to ~ ++ and is like a "pausing" for a function.
• .. x - List of x.
• [] x - A value of type x which is made independently of any input (although the input can be used to decide what value to make, and you can still use another input [] value).
• <> x - Same as ~ [] ~ x.
• !a - An atomic type. You cannot normally create values of this type.
• {x} - Put a rule definition body in between braces. It is not a type by itself, but can be used as parameters to other types.

(Note: there is no function type. There are also other built-in and user-defined types, which use ordinary names, instead of symbols.)

Object type markers:

• ?a - Any type; you can have more than one the same, if applicable, to mean the same type. It can be used within other types. If the name a is replaced with a single underscore, then it is distinct from any others.
• !?a - Similar to above, except that it is a distinct opaque atomic type for each use of the rule.
• *a - A placeholder for zero or more terms on the input or output side of a sequent. It can be used within other types, in which case it means each term has that correspondence.
• $n(x) - After the slash in any rule type, indicate position of input objects into the rule. Before the slash, it instead represents the input objects of rules the invocation uses. It cannot be used within other types.

Rule types:

• Consists of zero or more sequents in parentheses, delimited by semicolons, followed by a slash and then exactly one sequent in parentheses.
• A |- B - A sequent. Can contain types and markers, with commas in between, on each side. It means the type of a function which, given a value of each type on the left, produces a value for one of the types on the right (if there are duplicates, then you may be able to tell the difference which one is output even though they have the same type). The other of terms on one side doesn't matter.

Definitions

The program consists of several definitions, each of which ends with a semicolon.

Kind of definitions:

• Type synonym: Consists of a name, zero or more names of parameters, and then := followed by the definition. Recursive definitions are allowed (although difficult to use), and it is allowed to refer to types defined later. It is allowed for a type to have the same name as a rule without interference. For an opaque type, put ??? as the definition.
• Type/class definition: Put a number of typeclass definitions in braces. These definitions each end with a semicolon.
• Rule type declaration: Rule name, followed by a colon, and the rule type. Any types it refers to must be defined ahead of time. The name may be followed by a slash and another name, to indicate a variant of the rule which has a different type. It can be invoked without specifying the variant.
• Rule definition: The rule name (possibly including a variant name too), followed by an equal sign and the definition. It must be somewhere after the type of the rule is declared, although there can be any number of other things in between. It cannot invoke any rules unless their type declarations are given before the type declaration of this rule.
• Import: You import by specifying the <- followed by the name of library to import (in quotation marks), optionally followed by a list of subset of what to import. Library names are case sensitive.
• Export: Export by specifying -> and then optionally a name of library in quotation marks, and then items to export. If you put a question mark in front of any item, it exports a type as opaque.
• Macro: Specify a macro name, the parameters, two equal signs, and then the definition which can contain tokens other than a semicolon at the outer level and otherwise must have matching delimiters. When calling the macro, you need parentheses or other matching delimiters to have more than one token in an argument.

Implicit rules

If you use a term of a ~ type on the wrong side (input/output) of a sequent than it is expected, it can use it as if the ~ at front is omitted, as follows:

• (*a, ?x |- *b) / (*a |- ~ ?x, *b) - Creates a continuation and returns it. Once the continuation is called, it goes back and calls the above function, returning *b.
• (*a |- ?x, *b) / (~ ?x, *a |- *b) - Call the above function, and if it returns ?x then call the continuation it received.

These happen implicitly and there is no special syntax to invoke them. Note that it is possible for the function on top just to return (or call) the continuation again, since a term is usable any number of times.

You can also use a term on either side more than once or not at all; no special syntax is needed for this either.

Rule definition syntax

The definition of a rule starts with list in square brackets of variable names defined during its use. In case of more sequents above the line, put those first, followed by a forward slash, and can be called as functions. For example [x,y] init x y is the same as the standard init rule. You can also just specify an existing rule without using the square brackets syntax. You can ignore something by using an underscore in place of a variable name.

The invocation of a rule always consists of the rule, followed by its $ parameters of the bottom, followed by the functions it calls (a function is similar to a rule having () / at the front of its type; it can be used interchangeably).

Typeclass definition syntax

Type name: The name, followed by parameter names (if any), which are used in the rest of the program inside of the typeclass. If the parameter is a type, use square brackets around it, and the kind is indicated by a name or _ followed by () for each parameter of kind "*", name or _ followed braces containing a type (which can use the repeating of names given in the kind) for {} types, and name or _ followed by parentheses containing parameter kind for those with parameters. Any ? parameters in the kind cross the entire declaration, and so do names of types which kinds correspond to. For value parameters, use braces, and the name is followed by a colon and the rule type.

Class rule: Uses a standard rule declaration and definition syntax. However, the new types defined in this block are usable only at the outer level of a term (although they may be marked, and the $1 and $2 and so on are usually mandatory). You should write a definition of the rule; the type is good enough by itself.

Normal rule: You can also define a rule, like above, except that you give a type and definition in the normal way, with the same normal restrictions (rather than those of class rules). It can therefore be used privately and/or exported.

Type synonym: You can also define type synonyms inside of the block. You cannot refer to types defined later if those later types are outside of the class. You cannot define opaque types, although they can be exported as opaque.

Export: Export from the class using -> and the name(s) of what to export; the library name cannot be used here. Types which are not defined as synonyms, if not exported as opaque, allow defining additional class rules in further classes (and their corresponding cut-eliminations); you must specify if rules which are going to be defined is primary or secondary by a & or % prefix in such a case. Any rules not specified then are exported as "protected", so they can be used in the declaration of cut-elimination rules.

You also have to define cut-elimination rules in the case of each pair of class rules defined here where one uses a newly defined type on the left and one uses the same type on the right (including the same rule twice), if all the parameters to these types are also the same on each side.

The type of a cut-elimination rule is not defined explicitly; it is implicit. The class rule with the term on the right side of the sequent is called a primary rule, and the one having the term on the left is a secondary rule. The top is all the primary rule's top sequents followed by all the secondary rule's top sequents, while the bottom consists of the combination of all of all antecedents of both and all succudents of both, with the exception of the term being cut, which is omitted. Parameter numbers have all the primary rule's numbers first and then all secondary rule's numbers.

The definition is then given by giving the name of the primary rule, the $ and number of the object being cut, and then the name of secondary rule, the $ and number of that object being cut, and the equal sign and definition, as any other rule will be defined. Rules defined in a {} type can then be called by using the parameter name (defined where the outer type is defined).

Standard library

string := .. |\|;

Represents a text string.

left/and : ($1(?x), *a |- *b) / ($1(?x /\ ?_), *a |- *b);

Call the function ignoring the right part of the conjunction.

right/and : ($1(?x), *a |- *b) / ($1(?_ /\ ?x), *a |- *b);

Call the function ignoring the left part of the conjunction.

split/and : (*a |- $1(?x), *b; *a |- $2(?y), *b) / (*a |- $1(?x /\ ?y), *b);

If the first function returns $1, then call the second function with the same inputs, and if it returns $2, then the resulting function returns $1, otherwise the resulting function returns *b.

left/or : (*a |- $1(?x), *b) / (*a |- $1(?x \/ ?_), *b);

If the function returns $1, then return the value into the left side of the disjunction type $1.

right/or : (*a |- $1(?x), *b) / (*a |- $1(?_ \/ ?x), *b);

If the function returns $1, then return the value into the right side of the disjunction type $1.

split/or : ($1(?x), *a |- *b; $2(?y), *a |- *b) / ($1(?x \/ ?y), *a |- *b);

Call one of two functions depending on which one $1 is (the left or right part of a disjunction).

cut : (*a |- *b, $1(?x); *a, $1(?x) |- *b) / (*a |- *b);

Call the first one. If it returns $1, then call the second one with its result. You can also use the infix + operator which means the same thing as this rule.

init : () / ($1(?x) |- $2(?x));

Identity function.

true : () / (|- ++);

Make up a single value of a type.

false : () / (_|_ |-);

Do nothing.

succ : () / ($1(|\|) |- $2(|\|));

Make the succession of a natural number.

neces : ($1(*a) |- $2(?b)) / ($1([] *a) |- $2([] ?b));

Call the function inside of the boxed context.

count : ($1(?x), *a |- $2(?x), *b) / ($1(|\|), $2(?x), *a |- $3(?x), *b);

Iterate the function on top the given number of times, with the possibility to break out of the loop.

loop : ($1(?x), *a |- $2(?x), $3(?y)) / ($1(?x), *a |- $2(@ ?y));

Potentially infinite loop; call top function until the $3 result is returned (or it breaks out due to calling a continuation in *a).

lcopy : ($1(?x), *a |- $2(?y), *b) / ($1(@ ?x), *a |- $2(@ ?y), *b);

If the loop halted, then pass its value and return its result, otherwise it doesn't halt.

nil : () / (|- $1(.. ?_));

Make an empty list.

cons : () / ($1(?a), $2(.. ?a) |- $3(.. ?a));

Add an item to a beginning of a list.

fold : ($1(?x), $2(?y), *a |- $3(?y), *b) / ($1(.. ?x), $2(?y), *a |- $3(?y), *b);

Call function for each element of the list (with possibility to break out of the loop early). If the list is empty, the resulting function simply copies $2 to $3.

cmp : (*a |- *b; *a |- *b; *a |- *b) / ($1(|\|), $2(|\|), *a |- *b);

Compare the numbers. Call first one if is less, second one if equal, third one if first greater than the second one.

Variables library

var x := ???;

Type of variables having a value of type x.

new : () / ($1(?x) |- $2(var ?x));

Create a new variable with an initial value.

get : ($1(?x), *a |- *b) / ($1(var ?x), *a |- *b);

Call function above using the variable's value in place of the variable.

modify : ($1(?x), *a |- $2(?x), *b) / ($1(var ?x), *a |- $2(?x), *b);

Calls the function above with the value of the variable, and passes through the result, but if the result is $2 then it also updates the value of the variable.

I/O library

iosys := ???;

Represents an I/O system.

inbyte : () / ($1(iosys) |- $2(|\|));

Read a byte from standard input.

outbyte : () / ($1(iosys), $2(|\|) |- $3(++));

Send a byte to standard output.

outtext : () / ($1(iosys), $2(string) |- $3(++));
outtext = [io,s,z] cut true [t] fold s t z [ch,_,k] outbyte io ch k;

Output a text string.

Examples

Hello, World program:

<- "stdlib";
<- "iolib";
main : () / ($1(iosys) |- $2(++));
main = [x,y] cut "Hello, World!" [z] outtext x z y;
-> main;

Truth-machine program:

<- "stdlib";
<- "iolib";
do_zero : () / ($1(iosys) |- $2(@ ++));
do_zero = [io,lp] cut '0' [x] loop x lp [_,_,k] outbyte io x k;
do_one : () / ($1(iosys) |- $2(@ ++));
do_one = [io,lp] cut '1' [x] loop x lp [_,k,_] outbyte io x k;
truth : () / ($1(iosys), $2(|\|) |- $3(@ ++));
truth = [io,n,lp] cut '0' [z] cmp n z (do_zero io lp) (do_zero io lp) (do_one io lp);
main : () / ($1(iosys) |- $2(@ ++));
main = [x,y] cut ([z] inbyte x) ([z] truth x z y);
-> main;

Class of booleans:

{
  boolean;
  no : () / (|- $1(boolean));
  yes : () / (|- $1(boolean));
  test : (*a |- *b; *a |- *b) / (*a, $1(boolean) |- *b);
  no $1 test $1 = [x,_/] x;
  yes $1 test $1 = [_,x/] x;
  -> no yes test ?boolean;
};
-> no yes test boolean;

References

• Sequent calculus on Wikipedia