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.
- names
- operators
- numbers
- 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
- atomic type 0
- atomic type 1
- 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:
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 (+)