Category: Type Theory
-
Type Theory – The Untyped Lambda Calculus
The Untyped Lambda Calculus or the pure lambda calculus forms the computational substrate for most of the type systems. Peter Landin observed that complex programming languages can be understood as having a tiny core with all the complex features implemented in the tiny core. Lambda Calculus can be viewed as a simple programming language or…
-
Type Theory – Untyped Arithmetic Expressions
The following are present in this first language: true and false. conditional expressions. The numeric constant 0. The arithmetic operators succ and prec. A testing operation iszero. t = true false if t then t else t 0 succ t prec t iszero t Programs A program in the above language is a term built…
-
Type Theory – Mathematical Preliminaries
1. Sets, Relations and Functions Definition 1 Countable Set: A set is countable if it can be placed in one-to-one correspondence with the set of natural numbers . Definition 2 n-place Relation: An n-place relation on a collection of sets is a set of tuples . We say that elements through are related by if…