• "type formation" rules say how to create the type from existing ones.
• "term introduction" rules define the canonical terms and constructor functions, like "pair" and "S".
• "term elimination" rules define the other functions like "first", "second", and "R", i.e., how to use a term of a given type ⇒ eliminates types of some introduced terms.
• "computation" rules specify how computation is performed with the type-specific functions.

"Type theory" gets its name from the fact that every expression has an associated type.

$\equiv$ means definitional equality, $=_A$ means type equality.

There is also untyped lambda-calculus where the type of the function argument is not specified, while in STLC, we write $\lambda x: \tau .e : A$ instead of $\lambda x.e$.

Tips

You will find more about the detailed implementation of lambda calculus interpreter on course CSCI B521 at IU using racket like this:

(define lambda-exp?
	(lambda (exp)
		(match exp
			[`,y #:when (symbol? y) #t]
			[`(lambda (,x) ,body) #:when (symbol? x)
				(lambda-exp? body))]
			[`(,rator ,rand) (and (lambda-exp? rator) (lambda-exp? rand))])))

Types

Let $\mathcal{B} = \{ \top, \bot, Ans \}$, if $x \in \mathcal{B}$, then $x \space \text{Type}$; we call this basic rule:

$$ \underline{A \in \cal B} \\ A \space \text{Type} $$

Of course, functions are types:

$$ \underline{A \space \text{Type}, B \space \text{Type}} \\ A \to B \space \text{Type} $$

Some conventions:

• The function mapping is left-associative: $A \to B \to C \Leftrightarrow A \to (B \to C)$. This allows us to “define” multivariate functions.
• Function application is right-associative: $MNR = (MN)R$.
• $\top$ only has formation and introduction rule; $\bot$ only has elimination and uniqueness rule ($\forall C: Type, \bot \to C$ holds unconditionally).

Contexts