System I

WORK IN PROGRESS

Variables

Type variables: x_n;p

Expansion variables: E_n;p

Where n ∈ ℕ and p ∈ ℕ^* (sequences of integers)

Trees

Many objects in System I use the notion of boxed tree.

For all set S, if s ∈ S, then t ∈ Tree(S) is defined by the following pseudo syntax:

t ⩴ ω | {s} | t₁ ∧ t₂ | E t

The name boxed tree comes from the construction (E t), for which tree t is said to be inside the box named E.
Applying a substitution targetting E effectively performs an operation on the entire content of box E.

Boxed trees are identified up to the folllowing equivalence relation:

• F ω ≡ ω
• ω ∧ t ≡ t
• (t₁ ∧ t₂) ∧ t₃ ≡ t₁ ∧ (t₂ ∧ t₃)
• t₁ ∧ t₂ ∧ t₂ ∧ t₁
• t ∧ t ≡ t

Thus, ω can be intepreted as the empty set, { } as singleton set construction, and ∧ as set union.

Note that curly braces are omitted when it is unambiguous to do so.

Types

τ ∈ SmallType ⩴ x_n;p | τ → τ

where τ ∈ Type = Tree(SmallExpansion × SmallType).

Constraints Solving

Reduction to T-normal form solve all constraints between small types; it always terminates.

Flow Graph

Mozilla+SVG

Unicode Characters Testing