Titan

Foundations for the people

Synopsis

Titan is a development platform for incremental optimisable search and enumeration, based directly on formal substructural logic and the foundations of mathematics. For this, Titan defines:

A reference language in which to express these rules;
A standard library by which to facilitate development; and
Implementation constraints to provide performance guarantees.

The major intended objectives are:

Accessible and scalable proof capabilities; and
Optimisability sufficient for efficient embedded programming.

Semantics and Reference Language

Owing to the complexity of Titan's objectives, and the complexity of the foundations of mathematics in general, two semantics are given for the Titan Reference Language:

An informal semantics drawing from database theory; and
A formal denotational semantics (actually TBD, but likely to be based on formal topology).

Though separable, Titan's reference language and semantics were designed together to minimise complexity. In the Titan platform, programs and data are specified as extended patterns of sets of rows. An extended pattern is essentially a function which returns either an indicator function or another extended pattern, and terms are identified with their singletons, enabling them to match/filter as well. The major tricks added to this, however, are:

Relations can be partially applied, yielding the projection of the search for the rows with the given values in the corresponding columns onto the other columns (selective projection);
A row of a single column decays to the value in that column; and
A sum of a single row decays to that row.

The following outputs of an example implementation of the euclidean algorithm illustrate this succinctly:

(gcd 111 259) => 37
(gcd 111 259 37) => []

(gcd) =>

{
	[@_1  0    @_1]
	[@_1  @_2  (gcd @_2 (% @_1 @_2))]
}

(gcd 111) =>

{
	[0    111]
	[@_2  (gcd @_2 (% 111 @_2))]
}

(gcd @_1 259) => [@_1 (gcd 259 (% @_1 259))]

A brief summary of the language's grammar, taken from the upcoming design document, is provided below.

Alphabet

The alphabet of the Titan reference language is in the Unicode 10 character set. Several subsets are named here for future reference:

Letters, consisting of the Unicode General Category L, named letter;
Digits, consisting of the Unicode General Category N, along with the following subsets:
- the decimal digits 0123456789, named digit,
  and the nonzero digits ndigit = digit - 0;
- the binary digits 01, named bdigit;
- the octal digits 01234567, named odigit;
- the hexadecimal digits 0123456789ABCDEF, named hdigit;
Alphanumerics, named alpha = digit|letter;
Punctuation and delimiters, consisting of ()[]{}'"@;
Symbols, consisting of `.\/%^*+-#&|~=<>!?:;,, named symbol;
Whitespace, consisting of the union of the Unicode General Categories Zs, Zl, Zp and Cc; and
The underscore _.

Tokens

The delimiters () [] {};
Names, denoted by the regular expression name
(_|letter|symbol)(_|alpha|symbol)^*
Variables, defined by the regular expression variable
@name
Numbers, defined by the regular expressions number
-^?ndigit(digit ⁺(.digit ⁺)^?|(.digit ⁺)^?(e-^?ndigit digit ^*)^?)^?
0(.digit⁺|bbdigit⁺|oodigit⁺|xhdigit⁺)^?
'((\|')^-|\(\|'))'
Strings, defined by the regular expression string
"("^-|\("|\))^*"
Comments, defined by the regular expressions
\*(*\)^-*\
\\(newline)^-newline

Grammar

The full grammar of the Titan reference language is:
E ::= | AE
A ::= name | variable | number | string | [E] | {E} | (E)
Note that there are no reserved identifiers.

Standard Library

Titan's standard library is divided into three major parts: Language, Environment, and Algorithms. All definitions in the standard library are abstract data/negative types, meaning they are defined in terms of their projection relations. Only the Language part is mandatory, and the two other parts can be defined in terms of it.

Language

The Language part supports the core constructs of the language and provides models of many domains of mathematics, from statistics to topology to geometry.

Algorithms

The Algorithms part supports decision problems going all the way to the class RE.

Environment

The Environment part supports interaction with the real world, ranging from the underlying hardware/implementation to ontologies to the sciences.

Reference Implementation

Titan's reference implementation will be code-named Othrys, after the mountain home of the Greek titans (as opposed to Olympus, the home of the Olympian deities).

Bootstrap Implementation

Titan's bootstrap implementation, in progress, is code-named Chaos, after the root deity of the Greek Pantheon.