The Language Pt. 1

The language is an extention of Rusellian type theory made to resemble a programming language.

ATOMS

There are four types of atom.

1. names
2. operators
3. numbers
4. number patterns

NAMES

Names in the program consist of a letter followed by any combination of letters, numbers or underscores. Names can always be prefixed by a namespace sequence, which is a dot followed by a sequence of names followed by dots. e.g. x is a valid name, .x is a valid name and .myns.x is also a valid name. The namespaces aren't that useful in the program's current state but they will be in the future.

OPERATORS

The expression a+b can also be written as (+)(a,b). By using the operator in brackets notation we can refer to the operator by itself without arguments and use namespaces with the operator. (≡) is the universal identity operator. It is a special polymorphic operator that can never appear in bracketed form. The (-) operator can only be used with 1 argument (i.e. it can only be used for negation, not subtraction). Subtraction therefore has to be refered to with expressions like a+(-b).

NUMBERS

Numbers are represented with sequences of digits. The can always have namespace prefixes.

NUMBER PATTERNS

A number pattern is just the '#' character with or without a namespace prefix.

SEMANTIC TYPES

There are three types of semantic type

1. atomic type 0
2. atomic type 1
3. Compound

ATOMIC TYPE 0

Type 0 is represented with the single digit 0.

ATOMIC TYPE 1

Type 1 is represented with the single digit 1.

COMPOUND SEMANTIC TYPES

A Compound type consists of a non-empty comma separated list of semantic types in square brackets, called the domain-list, followed by a right arrow operator, followed by another semantic type, called the range type. If the domain-list has only one element, the surrounding square brackets can be omitted. Some examples of valid compound types are:

• 0→1
• [0→1,0]→(0→1)
• [0→1,0]→(0→[0→1,0]→(0→1))

JUSTIFICATIONS

A justification starts with a justification rule, which is a string starting with a letter and ending with letters or digits, possibly followed by an argument list of atoms. Some examples could be:

• Rep(T4)
• Ded(T5)
• UG(T6,w)

REGULAR EXPRESSIONS

In this program regular expressions are used in conjunction with namespaces. You can use letters, numbers, the number sign, or regular expression macros. Use (U) for or, (+) for Kleene plus and (*) for Kleene star. There is a macro for every operator as well as some other macros.

• {equals} matches the (=) operator
• T{alpha}* matches names starting with T and ending with 0 or more letters
• {alnum}+⋃{plus} matches any alpha-numeric name or the operator (+)