> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/350-type-theory/itt/inductive-definition.md). # Inductive definition * type, has type, is of type * judgement * inductive definition, induction * inference rules (axioms) * derivation * typing rules ## Static Semantics Foundations of Programming Languages: Static Semantics by Jan Hoffmann at OPLSS 2018 * **Judgement**: the expr `e` has type `τ`, denoted by `|- e : τ` * We define what judgements mean by induction (by inductive definitions) For example, to define binary trees, we say that * `Leaf` is a tree (base case), `|- Leaf : tree` * if `n` is a number and `t₁` and `t₂` are trees, then `Node n t₁ t₂` is a tree, `n : ℕ, t₁ : tree, t₂ : tree |- Node n t₁ t₂ : tree` * This inductive definition defines a judgement that `t` is a tree, `t : tree` * Actually, (I've used a turnstile above, but) the turnstile signifies derivations obtaind from the rules of inference (axioms), which is not the same. * turnstile signifies derivations: you can derive this judgment from these rules * **Inductive definition** is saying that something is a set and that the set is closed under the application of some inference rules (axioms). So, a binary tree is defined as being closed under the 2 inference rules, which also means that binary trees are all things that could be derived from them. * In PLT, these rules are called inference rules * **Inference rules** are for inductively defining judgements * Their general form is premises on top and conclusions under the line * these two rules below are inference rules (axioms) ``` Rules for binary trees: n : ℕ t₁ : tree t₂ : tree ----------- (t1) ----------------------------- (t2) Leaf : tree Node n t₁ t₂ : tree Rules for natural numbers: n : ℕ ----- (n1) --------- (n2) 0 : ℕ S(n) : ℕ ``` * **Derivations** (use turnstile) are used to prove a claim * for example, to prove that `Node S(0) Leaf Leaf` is a tree, you would use the rules of inference to derive this judgement ``` ----------- #n1 0 : ℕ ----------- #n2 ----------- (#t1) ----------- (#t1) S(0) : ℕ Leaf : tree Leaf : tree ----------------------------------------------- (#t2) Node S(0) Leaf Leaf ``` ## Typing rules Typing rules are also given by the set of inference rules ``` ----------------- (1) ------------------- (2) ---------------- (3) Γ |- num(n) : num Γ |- bool(n) : bool Γ, x: τ |- x : τ ----------------------- (4) Γ |- let (e₁; x.e₂) : τ ``` (1) and (2) The first two rules above just state that numbers have type `num`, and that Booleans have type `bool`. They state the evident type that literals of that type (should) have. (3) This rule about variables is more complex since the type of a variable depends on the *context*. This context that tracks the types of variables is the **typing context** or **environment**, and it is commonly denoted by the Greek capital letter `Γ`. (3) The line `Γ, x: τ |- x : τ` states that the context Γ *extended* with the var x of type τ (since we have recorded in the env that var x has type τ), means that (indeed) var x has type τ. It could be also said: if the context is extended with the fact that x has type τ, then var x has type τ indeed. This means that after type-checking the code, we found that var x must have type τ, so we have record this fact in the typing env Γ; on the subsequent lookups for type of x, we'll find that it has type τ (in the context Γ). > The typing context (typing environment) maps variables (var names) to types. Γ |- e : τ The typing context is denoted by `Γ` and it is a mapping, meaning that every expression (`e`) can only have a single type (`τ`). (4) In the typing rule for let-expr, `let (e₁ x e₂)` == `let x = e₁ in e₂`