User:Hppavilion1/List Theory

List Theory is the mathematical study of lists (particularly Pythonic ones), which are basically Sets with a sense of position in the list. It was discovered by Hedwig Notta in the surreal year √(ω)+π.

Primitives

The first primitive of List Theory is the predicate empty(l). It returns True when l is the empty list, otherwise false.

The empty list, represented by [], is the list with no items in it. It is the only solution to empty(l).

Other predicates include is_tail(l, t) and is_head(l, e), where l is a list, t is a list of length less than of l, and e is an element of a list. The predicates return true when their second argument matches the respective parts of the list l.

Axioms

• For any list l that is not the empty list, there is some element e that satisfies is_head(l, e) and some list t (which may be the empty list) that satisfies is_tail(l, t).

• For any two lists l and m, there is a list n which satisfies is_head(n, l) and is_tail(n, m).

• Say that if you have a function f from a list to maybe-a-list, as well as a list x, then there's a list that goes like [x, f(x), f(f(x)), f(f(f(x))), ...], stopping once f decides to return not-a-list. (ripped directly from IRC)

• Lists cannot contain themselves. Just no.

Constructions

To be determined