Tuesday, February 18, 2014

The first idea about type systems for programming languages

Type theory (mathematics) relates to type systems (programming languages) in the representation of the domain. The algebras of set theory invoke infinite and uniform operators on an infinite and uniform domain abstraction, which produces Russell's paradox.

A programming language is far more complex than a numeric group. Its syntactic (recognition) automaton ranges over files which are finite inputs in the domain of all inputs which is constrained to files. The syntactic grammar of a programming language can violate Russell's paradox because the product of these automata is computable. Similarly, the type system of a programming language requires that a type is a member of itself.

It's also true that a type system is not a member of naive set theory for its complexity. The membership operator in the programming language type system is distinct from the membership operator in set theory: it has enough complexity to set it apart from convenient approaches via mathematical algebra. Writing it in mathematical notation is possible, but would be tedious. The notation of computer programming languages is more succinct for the complexity of its meaning including computability and finitude.

Similarly, in programming computers we have no use for infinite non deterministic automata while in mathematics every case is included.

No comments: