modeling languages
- functions - f : A \to
B a total mapping that associates an element of A to a single element of B
- relations - R \subseteq A
\times B relates elements A with
B
- induction (on natural numbers) - prove R(0) then prove R(n) \implies R(n+1). This proves \forall n \in \N R(n)
- inductively defined sets - base cases (elements
that are in S), inductive rules (ways
to construct new elements of S)
- indexed family of sets - inductively defined sets
where the inductive rules define a new set indexed by something
syntax
The description of terms/values of a language.
semantics
The description of how terms/values are reduced