1
Q
What is soundness?
A
- Proofs only give true statements.
- Only proves true things
- If a theorem can be proved, it must be true.
2
Q
What is completeness?
A
- If something is always true (tautology), we can prove it.
- can prove all true things
3
Q
What is a tautology?
A
- Always true
4
Q
What is consistency?
A
- No contradictions
- Cannot prove something and also prove its opposite
5
Q
What is a sequent?
A
P1, P2, …, Pn ⊢ P
- using assumptions P1 -> Pn we can prove P.
- ⊢ is syntactic entailment
6
Q
What is ⊢?
A
- syntactic entailment
7
Q
What is an assumption rule?
A
From {P}, we can prove P. This does not mean P -> P
8
Q
What is and ∧ introduction?
A
- Rule name: ∧-I
- From: P and Q
- To: P ∧ Q
9
Q
What is Modus Ponens?
A
- → Elimination
- From: P → Q and P
- To: Q
- Rule name: →-E
10
Q
What is → introduction?
A
- Add assumption: P
- Prove: Q
- Then conclude: P → Q
- Rule name: →-I
11
Q
What is ¬ Negation?
A
- From: P and ¬P
- To: false
- Then: ¬P from false
- Rule name: ¬-E and ¬-I
12
Q
What is False (⊥)?
A
- No intro rule
- Elimination: From false, anything follows
13
Q
What is True (⊤)?
A
- Intro rule: Always true
- No elimination rule
14
Q
What is Law of Excluded Middle?
A
- Statement: P ∨ ¬P
- Either the proposition or its negation must be true
- Used in: Classical logic
- Not used in: Intuitionistic logic
15
Q
What is Semantic Entailment?
A
- Symbol: ⊨
- Meaning: If assumptions are true, conclusion is true in all cases.
16
Q
What is enumerability?
A
- can list all proofs though maybe never finishes
17
Q
What is decidability?
A
- can decide if something is provable or true
18
Q
Define the theorem for type soundness.
A
If ⊢ e : τ and e →* e′ and e′ cannot step further, then e′ is a value and ⊢ e′ : τ.
Progress + Preservation = Type Soundness.
This guarantees: Well‑typed programs don’t go wrong.
In other words, typing rules are a safety net: if the type checker accepts a program, it won’t crash due to type errors at runtime.
19
Q
Define the preservation lemma.
A
If ⊢ e: τ and e → e′ then ⊢ e′: τ .
20
Q
What is →*?
A
→ is one step, →* is zero or more steps
21
Q
Every expression has type. How do we write this in haskell?
A
expression :: type
22
Q
State the property of subject reduction and explain why it’s a key correctness property for type systems.
A
Subject reduction (type preservation) means that if a term is well‑typed and it evaluates to another term, the resulting term has the same type. This ensures types remain consistent during execution and is a key part of type soundness, guaranteeing that well‑typed programs don’t produce type errors at runtime.
23
Q
Describe how a type checker for a dependently typed language uses the conversion rule.
A
Idea: Types can depend on terms, so equality up to computation matters.
Rule: If Γ⊢𝑡:𝑇 and 𝑇≡𝑇′ (definitional equality via β/η/δ-reduction), then
Γ⊢𝑡:𝑇′.
Use: The checker normalizes or compares types for convertibility to accept terms when their types reduce to the same canonical form.
24
Q
Reduce the following terms to normal form using beta reduction. Show the reduction steps for each.
(i) (λx.x)(yz)
(ii) (λx.xy)(λz.z)
(iii) (λx.λy.xy)
(iv) (λx.λy.yx)
A
(i)
(𝜆𝑥. 𝑥)(𝑦𝑧)
Step: Apply β: substitute
𝑥:=𝑦𝑧.
Result:
𝑦𝑧.(𝜆𝑥. 𝑥)(𝑦𝑧) →𝛽 𝑦𝑧
(ii)
(𝜆𝑥. 𝑥𝑦)(𝜆𝑧. 𝑧)
Step 1: Apply β: substitute
𝑥:=𝜆𝑧. 𝑧.
Step 2: No more redexes (free 𝑦).
Result:
(𝜆𝑧. 𝑧) 𝑦.(𝜆𝑥. 𝑥𝑦)(𝜆𝑧. 𝑧) →𝛽 (𝜆𝑧. 𝑧) 𝑦
(iii)
(𝜆𝑥. 𝜆𝑦. 𝑥𝑦)
Observation: Already an abstraction; no application.
Result:
𝜆𝑥. 𝜆𝑦. 𝑥𝑦 (normal form).
(iv)
(𝜆𝑥. 𝜆𝑦. 𝑦𝑥)
Observation: Already an abstraction; no application.
Result:
𝜆𝑥. 𝜆𝑦. 𝑦𝑥 (normal form).
25
Given the following lambda functions, S, K, B and I, reduce S(K I) and BI to normal form, and show that both normal forms are equivalent to I.
(i) S = λx.λy.λz.xz(yz)
(ii) K = λx.λy.x
(iii) B = λx.λy.λz.x(yz)
(iv) I = λx.x
1. K I → λy.I
2. Apply S to this: S (λy.I) → λy.λz. (λy.I) z (y z)
3. Simplify to λy.λz. I (y z)
4. I = λx.x, so I (y z) → y z
5. this is can be shown equivalent to I with eta reduction.
1.Apply B to I - sub x:= I into B=λx.λy.λz.x(yz):
𝐵 𝐼=𝜆𝑦.𝜆𝑧. 𝐼 (𝑦 𝑧)
2. Use identity combinator:
𝐼=𝜆𝑥. 𝑥, so 𝐼 (𝑦 𝑧)→𝑦 𝑧.
3. Final result: 𝜆𝑦.𝜆𝑧. 𝑦 𝑧
4. to show it is equivalent to I, we must eta reduce:
Rule:
𝜆𝑣. 𝑓 𝑣 ≡ 𝑓 if 𝑣 is not free in 𝑓.
- eta step to inner lambda: 𝜆𝑧. 𝑦 𝑧 ≡ 𝑦 as z not free in y
- apply to outer lambda: 𝜆𝑦. 𝑦 = 𝐼
26
What’s the difference between leftmost‑outermost and rightmost‑innermost reduction? How do they link to lazy vs strict evaluation?
Leftmost‑outermost (LO):
- Reduce the outside, leftmost redex first.
- Lazy evaluation → don’t touch arguments unless needed.
- Finds normal forms if they exist.
Rightmost‑innermost (RI):
- Reduce the inside, rightmost redex first.
- Strict evaluation → arguments are evaluated before applying.
- Can diverge even if a normal form exists.
27
What are the three kinds of terms in the untyped λ‑calculus
Variable: x
Abstraction: λx.t
Application: t t
28
What is the Beta (outermost) rule?
(λx.t) u → t[x := u]
Substitute u for x in t.
This is the main reduction step.
29
What is the App‑Left rule? E-App1
If t1 → t1′, then t1 t2 → t1′ t2:
t1 → t1′
-------------------
t1 t2 → t1′ t2.
Reduce the leftmost operator first.
Enforces leftmost evaluation.
E-App2:
t2 → t2′
-------------------
v1 t2 → v1 t2'.
30
What is the App‑Beta preference rule?
Don’t reduce inside the argument before contracting the outer redex.
Only create new redexes by moving left.
Enforces outermost evaluation.
31
What is E-AppAbs (untyped)?
(λx.t1) v2 → [x |→ v2]t1
32
What is the Abs‑No‑Step rule?
λx.t does not reduce unless applied.
Don’t reduce inside the body until needed.
33
What does “leftmost‑outermost” mean?
Always reduce the first redex you see from the left, at the outer level.
Don’t dive deep inside until the outside is handled.
34
What does it mean for an expression to be in weak head-normal form? Explain how this differs from head-normal form and normal form.
WHNF: Stop as soon as you see the outermost wrapper.
- don't look inside arguments.
HNF: Unwrap the outer box, make sure each argument is at least opened once.
- still do not fully simplify everything inside.
NF: Everything is fully simplified. No wraps left, no hidden work still to do.
35
Consider the following expressions:
1) λz . (λx . λy . z + (x + y)) 4 5
2) λy . (λz . (λx . z + (x + y)) 2) 4
Give the normal forms of both expressions.
1) Make sure to add al brackets...λz . ((λx . λy . z + (x + y)) 4 5)
1. Apply inner function:
(𝜆𝑥.𝜆𝑦. 𝑧+(𝑥+𝑦)) 4 → 𝜆𝑦. 𝑧+(4+𝑦)
2. Apply that to 5: (𝜆𝑦. 𝑧+(4+𝑦)) 5 → 𝑧+(4+5) = 𝑧+9
- note: not doing the arithmetic here would have left it in HNF
3. wrap with the outer lambda: 𝜆𝑧. 𝑧+9
2) Again, make sure to fully wrap if not already λy . ((λz . (λx . z + (x + y)) 2) 4)
1. Reduce inner application, noting y is free inside: (𝜆𝑥. 𝑧+(𝑥+𝑦)) 2 → 𝑧+(2+𝑦)
2. Apply to z = 4: (𝜆𝑧. 𝑧+(2+𝑦)) 4 → 4+(2+𝑦) = 𝑦+6
- note: not doing the arithmetic here would have left it in HNF
3. Wrap with outer lambda: 𝜆𝑦. 𝑦+6
36
Consider the following expressions:
1) λz . (λx . λy . z + (x + y)) 4 5
2) λy . (λz . (λx . z + (x + y)) 2) 4
Give a weak head-normal form of both expressions which is not also a normal form.
1) A valid WHNF that is not NF:
- λz . ((λy . z + (4 + y)) 5)
Explanation: The whole expression is a lambda (so it’s WHNF). Inside, there’s still an application reducible ((λy …) 5), so it’s not in normal form.
2) A valid WHNF that is not NF:
- λy . ((λz . z + (2 + y)) 4)
Explanation: The whole expression is a lambda (WHNF). Inside, there’s still an application reducible ((λz …) 4), so it’s not in normal form.
37
Why is lambda calculus a good fit for describing denotational semantics of programming languages?
Pure + Minimal:
-Only functions and application.
-Matches clean mathematical models.
Compositional:
-Whole program meaning = built from parts.
-Structure of λ‑calculus mirrors this.
-Abstraction + Higher‑order:
-Functions as first‑class citizens.
-Variables handled by environments.
Extensible:
-Extra effects (state, IO, etc.) can be added with monads/domain theory.
-Core stays simple.
38
What is Eta expansion?
Rule: e ≡ λx. e x (if x not free in e).
It rewrites a function e as λx. e x.
Means: “wrap the function in a λ and apply it to a fresh variable.”
39
Why isn’t Eta expansion a computation step?
It doesn’t reduce or simplify anything.
No redex (no β‑reduction).
It just changes the form of the function.
No progress, no cost reduction.
40
Show Eta expansion with identity.
Identity: I = λx. x
Eta‑expanded: λx. I x
Both are equal by η‑equivalence.
But there’s no β‑step to go from one to the other.
41
What is the Curry-Howard Isomorphism? Give examples to illustrate your answer.
Big idea:
-Logic ↔ Types
-Proofs ↔ Programs
-Proof steps ↔ Program evaluation
Examples:
-Implication (A → B) ↔ Function type (A → B)
--A proof is a function.
-Conjunction (A ∧ B) ↔ Product type (A × B)
--A proof is a pair ⟨a, b⟩.
-Disjunction (A ∨ B) ↔ Sum type (A + B)
--A proof is either inl(a) or inr(b).
-False (⊥) ↔ Empty type
--No values; “ex falso” means from falsehood anything follows.
42
Explain how a type system can help prevent program errors.
Static guarantees: Types rule out category mistakes (e.g., adding a number to a string), check arity/mismatches, and enforce interface contracts.
Resource and effect control: Types can constrain nullability, mutability, exceptions, and effects (e.g., linear types, effect systems).
Soundness: With subject reduction and progress, well-typed programs avoid certain runtime failures.
43
Describe two purposes of a type system, other than to prevent program errors.
Documentation and design: Types serve as precise, machine-checked specifications that aid readability and refactoring.
Optimization and compilation: Types enable better code generation (unboxing, specialization, inlining) and guide correctness-preserving transformations.
44
Define the grammar of the abstract syntax of terms t and values v.
t ::=
true
| false
| if t then t else t
| 0
| succ t
| pred t
| iszero
::=
true
| false
45
Show a derivation for λx.λy.λz.(xz)(yz) : (σ → τ → ρ) → (σ → τ) → (σ → ρ) and therefore that the term has the corresponding type.
1) Γ = { x:σ→τ→ρ, y:σ→τ, z:σ }
2) Γ ⊢ x:σ→τ→ρ (Var)
3) Γ ⊢ z:σ (Var)
4) Γ ⊢ x z : τ→ρ (App 2,3)
5) Γ ⊢ y:σ→τ (Var)
6) Γ ⊢ y z : τ (App 5,3)
7) Γ ⊢ (x z)(y z) : ρ (App 4,6)
8) Γ \ {z} ⊢ λz.(x z)(y z) : σ→ρ (Abs on 7) - \ {z} "remove z from context"
9) Γ \ {y,z} ⊢ λy.λz.(x z)(y z) : (σ→τ)→(σ→ρ) (Abs on 8)
10) ⊢ λx.λy.λz.(x z)(y z) : (σ→τ→ρ)→(σ→τ)→(σ→ρ) (Abs on 9)
46
True or false: Term and expression are used interchangeably.
True
47
What are operational semantics?
Operational semantics specify the behavior of programs by giving rules for how each construct in the language changes the program’s state during execution.
48
What are the operational semantics of booleans?
E-iftrue:
if true then t2 else t3 → t2
E-iffalse:
if false then t2 else t3 → t3
If the condition is true, we can throw away the conditional expression and leave t2.
49
What is a redex?
A reducible expression, like
(𝜆𝑥.𝑒)𝑒′.
50
What does beta reduction do?
What is full beta-reduction?
It substitutes the argument for the variable in the function body.
Full: Any redex can be reduced at any time.
51
What is normal order evaluation?
Always reduce the leftmost, outermost redex first.
52
What is call-by-name?
Reduce outermost redex only, stop at inner ones.
53
What is call-by-value?
Evaluate arguments first, then apply function (strict).
54
When is a term in normal form?
When it has no redexes left.
55
Give an example of a normal form.
𝑥, 𝜆𝑥.𝑥.
56
What shape is a head normal form?
(𝜆𝑥.𝑦𝑒⃗), where 𝑦 is a variable.
57
Are all normal forms also head normal forms?
Yes
58
What counts as weak head normal form?
A lambda abstraction, or a variable applied to terms.
59
Are all head normal forms weak head normal forms?
Yes
60
How do normal forms, head normal forms, and weak head normal forms relate?
Normal ⊆ Head ⊆ Weak head.
61
What is Ω ((𝜆𝑥.𝑥𝑥)(𝜆𝑥.𝑥𝑥))?
Infinite loop - A term that never reaches normal form.
62
Q: What does the Y combinator do?
Q: Why is it important?
Produces fixed points: 𝑌𝑓→𝑓(𝑌𝑓).
Important as it enables recursion in lambda calculus.
63
Do all meaningful functions have normal forms?
No - some useful functions (like recursion) don’t.
64
What two properties make a type system safe? Define them.
Progress + Preservation
Progress: A well‑typed term is never stuck
Preservation: Evaluation keeps the type the same
65
What does the Inversion Lemma tell us?
The type of a term fixes its form (e.g. if true : R, then R = Bool)
66
What does the Canonical Forms Lemma say?
Values of type Bool are true/false; values of type Nat are numbers
67
What does A -> B mean?
A function that takes input of type A and gives output of type B.
The arrows always associate right. Example: A -> B -> C means A -> (B -> C)
68
What is an abstraction in typed lambda calculus?
A function definition that names a parameter and states its type. Example: λx:Bool. x.
69
What is a typing context (Γ)?
A list of variables and their types. Example: x : Int.
70
If x : T is in the context, what does that mean?
x has type T. Rule: (T‑VAR).
71
If f : A -> B and x : A, what is f x?
It has type B. Rule: (T‑APP).
72
What is Curry–Howard?
A link between logic and programs.
Proofs ↔ Programs
Propositions ↔ Types
73
What does strong normalisation mean?
Every typed term eventually reduces to a value. No infinite loops (unless recursion is added).
74
Why is x x untypable?
It would cause non‑termination.
75
What are base types?
Simple values like numbers, Booleans, strings. They have no internal structure.
76
What is an atomic type?
A base type with no operations or structure.
77
What is the Unit type?
A type with only one value: unit.
78
What does t1 ; t2 mean?
Do t1, throw away result, then do t2.
79
What does let x = t1 in t2 mean?
Evaluate t1, name it x, then use x inside t2.
80
What is a pair?
Two values grouped: {t1, t2}.
81
How do you get the first part of a pair? Second?
Use .1 → gives the first value.
Use .2 → gives the second value.
If it was a tuple...it would be .i to get the ith element.
82
What is a sum type?
A type that can be one of two kinds. Example: Either A or B.
83
How do you mark the left side of a sum? right?
Use inl.
Use inr.
84
What is a reference?
A pointer to a memory cell that stores a value.
85
What does ! r mean?
It gets (dereferences) the value stored in r.
86
What does r := v do?
It updates the reference r with the new value v.
87
What does ref e do?
It creates a new reference that stores the value of e.
88
What type does an assignment return? Why is this useful?
Unit.
It lets assignments fit into sequencing (doing steps one after another).
89
What is aliasing?
When two references point to the same memory cell.
90
In referencing, if s = r, what happens?
s and r both point to the same cell. Changing one changes the other.
91
What type does ref t have?
Ref T
92
What type does ! t have?
T (the type of the value inside).
93
What type does t1 := t2 have?
Unit.
94
What is a store?
A set of locations, each with a value.
95
How do we write an update to a store?
[l → v]σ means “store σ updated with value v at location l”.
96
What does the Preservation Theorem say?
Types are preserved when the store changes - the program stays well‑typed.
97
What does the Progress Theorem say?
A well‑typed program is either a value or can take a step forward.
98
What is a variable in lambda calculus?
A name that stands for something.
Example: x, y, z.
Variables are the simplest terms.
99
What is an abstraction (Abs)?
A function definition.
Written as λx. M.
Means: “a function that takes input x and returns M.”
Example: λx. x+1.
100
What is an application (App)?
Applying one term to another.
Written as (M N).
Means: “apply function M to argument N.”
Example: (λx. x+1) 3 → 4.
101
What are the three kinds of terms in lambda calculus?
Var, Abs, App
102
True or false: Only abstractions are counted as values in Lambda Calculus.
True.
103
What are the terms in STLC?
Variables: x
Abstractions: λx:T. M
Applications: (M N)
104
What are the types in STLC?
Base types: Bool, Nat
Function types: T1 → T2
105
What are the typing rules?
Var: If x:T in context, then x:T.
x:T ∈ Γ
----------T-VAR
Γ ⊢ x:T
Abs: If x:T1 ⊢ M:T2, then λx:T1. M : T1 → T2.
Γ, x:T1 ⊢ t:T2
------------------------------T-ABS
Γ ⊢ λx:T1. t : T1 → T2
App: If M:T1 → T2 and N:T1, then (M N):T2.
Γ⊢ t1 : T11→T12 Γ⊢ t2 : T11
----------------------------------------T-APP
Γ ⊢ (t1 t2):T12
106
How are pairs added to STLC?
Terms: (M, N), fst M, snd M.
Types: T1 × T2.
Rules: fst (M, N) → M, snd (M, N) → N.
107
How are sums added to stlc?
Terms: inl M, inr N, case M of inl x ⇒ N | inr y ⇒ P.
Types: T1 + T2.
Rules:
case (inl M) of … → N[x := M]
case (inr N) of … → P[y := N]
108
How is recursion added to lc?
Term: fix M.
Rule: fix M → M (fix M).
Allows defining recursive functions.
109
What are kinds?
The "types or types".
Keeps the system well‑formed: every type has a kind.
110
What is the base kind?
* (or Type)
Means “a proper type” - something that classifies actual values.
Example: int : *, bool : *.
111
What is a function kind?
If κ1 and κ2 are kinds, then (κ1 → κ2) is a kind.
Example:
List : * → *
Takes a type (like int) and gives back a type (List int).
Pair : * → * → *
Takes two types and gives back a type (Pair int bool).
112
How do values, types, and kinds relate?
(Ladder analogy).
Level 1: Values (e.g. 3, true)
Level 2: Types (e.g. int, bool, List int)
Level 3: Kinds (e.g. *, * → *)
113
What are the terms in arithmetic expressions?
true - constant true
false - constant false
if t then t else t - conditional
0 - constant zero
succ t - successor
pred t - predecessor
iszero t - zero test
114
What counts as a value in arithmetic expressions?
true - Boolean value
false - Boolean value
nv - numeric value
115
What are numeric values?
0 - zero value
succ nv - successor of a numeric value
116
How do we evaluate applications (right side)?
If t2 → t2′ and t1 is a value, then (t1 t2) → (t1 t2′).
117
What is (E-IfTrue)?
if true then t2 else t3 → t2
118
What is (E-IfFalse)?
if false then t2 else t3 → t3
119
What is (E-If)?
t1 → t1'
------------------------
if t1 then t2 else t3→
if t1' then t2 else t3
120
What are the evaluation rules for (untyped) arithmetic expressions?
E-Succ:
t1→ t1'
-----------------------
succ t1→succ t1'
E-PredZero:
pred 0 →0
-----------------------
pred (succ nv1) → nv1
E-PredSucc:
t1→t1'
-----------------------
pred t1 → pred t1'
E-IsZeroSucc:
iszero(succ nv1) → false
E-IsZeroZero:
iszero 0 → true
E-IsZero
t1→t1'
-----------------------
iszero t1 → iszero t1'
121
What are the typing rules for bools and nats?
T-true:
true:Bool
T-false:
false:Bool
T-If:
t1 : Bool t2 : T t3 : T
-----------------------------------
if t1 then t2 else t3 : T
T-Succ:
t1 : Nat
----------------
succ t1 : Nat
T-Pred:
t1 : Nat
------------------
pred t1 : Nat
T-IsZero:
t1 : Nat
----------------------
iszero t1 : Bool
122
What is E-AppAbs (typed)?
(λx :T11 .t12) v2 → [x |→ v2]t12
123
What is referential transparency?
An expression always means its value. You can swap equal values safely.
Basically, the program behaves the same if you swap an expression with what it evaluates to.
124
What is denotational semantics?
A way to explain programs using maths. Expressions map to mathematical objects (denotations).
125
What is an environment (Env) in denotational?
A map that tells what each variable means. Example: X → 5.
126
What is a value domain (V) in denotational?
The set of possible values. Numbers (K) or functions (V → V).
127
What does a semantic function do?
It links expressions to values. Written as ⟦E⟧p (value of E in environment p).
128
How do we evaluate a variable in denotational?
Look it up in the environment. Example: p[X] = 42.
129
How do we evaluate a constant in denotational?
Just return the constant itself. Example: ⟦2⟧p = 2.
130
How do we evaluate an abstraction (λ) in denotational?
Turn program syntax into λ‑calculus. Extend environment with the variable.
131
How do we evaluate an application (E0 E1)?
Evaluate E0, then E1, then apply one to the other.
132
What is polymorphism?
One function works for many types. Example: id :: forall a. a -> a.
133
What are dependent types?
Types that depend on values. Example: Vec a n → vector of type a with length n.
134
What is the dependent function space?
The dependent function space is the type of functions whose result type depends on their argument value.
Written as:
(𝑥:𝐴)→𝐵(𝑥)
Input: x of type A.
Output: a value of type B(x), where B is a type that depends on x.
This is called a Π‑type (Pi type). It generalizes ordinary function types:
Ordinary function:
𝐴→𝐵 (output type fixed).
Dependent function:
(𝑥:𝐴)→𝐵(𝑥) (output type varies with input).
135
What does “everything is a term” mean in dependent types?
No strict split between values and types. Terms, types, and kinds are all treated as terms.
136
What is bidirectional typing?
A type system technique that alternates between synthesizing (inferring) and checking types.
Synthesis (Inference): The system figures out the type of a term.
Checking: The system verifies a term against a given type.
Helps balance flexibility and precision in complex type systems.
137
What is the vector type?
A vector is like a list, but its length is part of the type.
Constructors:
Nil :: Vec a Zero
- Nil: the empty vector.
Cons :: a -> Vec a k -> Vec a (Succ k).
- Cons: add an element to the front.
The length is tracked at the type level. Vec Nat 3 is a vector of 3 natural numbers. Vec Bool 2 is a vector of 2 booleans.
138
What does map on vectors do?
Type: (a -> b) -> Vec a k -> Vec b k
Applies a function to each element.
Preserves the length k.map :: (a -> b) -> Vec a k -> Vec b k Preserves the length of the vector.
139
What is the equality type (Eq) in dependent type theory?
Definition: Eq a x y is the type expressing that two terms x and y of type a are equal.
Constructor:
Refl :: Eq a x x
The only way to construct an equality proof is by reflexivity: a term is equal to itself.
Usage: If you can build a term of type Eq a x y, you have a proof that x = y.
140
True or false: In polymorphism, types can depend on other types.
True
141
What is the difference between operational and denotational semantics?
Operational semantics: describe how a program runs step by step.
Denotational semantics: describe what a program means by mapping it into mathematics.
142
What is PiForall?
PiForall is a small programming language with dependent types. It mixes terms (values) and types (categories of values) in one system.
143
What are the basic building blocks in PiForall?
1. Variables (x)
2. Lambda functions (\x. a → anonymous functions)
3. Function applications (a b → applying a function)
4. Pi types ((x:A) → B → dependent function types)
5. Type (the type of all types)
144
How do we check if a term is valid?
We use a typing context (Γ). It’s a list of assumptions about variables and their types.
Notation: Γ ⊢ a : A → “In context Γ, term a has type A.”
145
What is the polymorphic identity function?
It works for any type.
1. In Haskell: id :: forall a. a -> a
2. In PiForall: id : (x : Type) -> (y : x) -> x
Definition: id = \x. \y. y
146
Why is “Type : Type” a problem?
It causes Girard’s paradox. This means every type would have a value, making the system inconsistent (all propositions become provable).
147
How does function application (piforall) work?
If a is a function (x:A) → B and b has type A, then a b has type B with b substituted for x.
148
How are Booleans defined in PiForall?
bool = (x:Type) -> x -> x -> x
true = \x. \y. \z. y
false = \x. \y. \z. z
Booleans are functions that choose between two options.
149
What is a bidirectional type system in piforall?
A system with two judgments:
1. Infer (Γ ⊢ a ⇒ A → figure out the type)
2. Check (Γ ⊢ a ⇐ A → verify against a given type)
This helps reduce the number of type annotations needed.
150
Why use bidirectional typing in piforall?
It makes type checking more algorithmic and easier to implement. It separates inferring a type from checking a type.
151
What is a Sigma type in piforall?
A Sigma type is like a pair. The second part depends on the first part.
152
Why are Sigma types useful in piforall?
Because the first part can act as a witness (proof) for the second part.
153
What is definitional equality in piforall?
It means the type system treats two types as the same if they reduce to the same form.
154
What problem happens with vectors?
To use head, the vector length must match exactly. Sometimes lengths are written differently (like succ 1 vs plus 1 1).
155
What do we use to type check that succ 1 and plus 1 1 are the same?
Equality.
156
What rules define equality in piforall?
Refl: A = A
Sym: If A = B, then B = A
Trans: If A = B and B = C, then A = C
Beta: Functions reduce when applied (like (\x.a)b = a{b/x})
157
What is propositional equality in piforall? How do we prove it?
A type that represents the statement “a = b”.
Prove with refl, which shows something equals itself.
158
What can we do with propositional equality in piforall?
subst: Replace one term with another if they are equal.
sym: Show equality works both ways.
trans: Chain equalities together.
159
How do we prove something false in piforall?
Use contra. If we can show True = False, then we can prove anything.
160
What is operational semantics?
Rules that explain how programs run step by step. They show how commands change the program’s state.
161
What is the IMP language?
A tiny programming language with numbers, booleans, and commands like if, while, and assign.
162
What is a state?
A memory snapshot. It maps each variable (location) to a number. Example: X → 5.
163
How do arithmetic expressions work in IMP?
They evaluate to numbers.
Example: (2 + 3) → 5.
Variables get their value from the state.
164
How do Boolean expressions work in IMP?
They evaluate to true or false.
Example: (3 ≤ 5) → true.
165
What does skip mean in IMP?
A command that does nothing. State stays the same.
166
How does while b do c work?
If b is true → run c, then check again.
If b is false → stop.
167
What is equivalence in semantics?
Two expressions or commands are equivalent if they always give the same result in every state.
168
Why use operational semantics?
To prove properties of programs, like correctness or equivalence, using clear rules.
169
What is Void in piforall?
A type with no values (no constructors).
170
What happens if you eliminate Void in piforall?
You can produce a value of any type (because it’s impossible).
171
What are the constructors of Nat in piforall?
Zero and Succ n (the next number after n).
172
What makes a datatype “dependent” in piforall?
Constructors have extra rules or constraints.
Example:
SillyBool
ImTrue only if value = True
ImFalse only if value = False
173
What is a telescope in type theory?
A list of arguments where later ones depend on earlier ones.
Called telescope because arguments extend out, overlapping like telescope sections.
174
How do we eliminate datatypes in piforall?
With a case expression.
175
What rule must be followed in piforall?
All constructors must be covered (exhaustive).
176
What is an example of a parameterised datatype in piforall?
Maybe (A : Type) with constructors:
Nothing
Just of (A)
177
Why use parameters?
To allow constructors to depend on a type argument.
178
What is an example of Sigma type?
A pair of a value x:A and something about x: Prod of (x:A) (B x)
179
What are indexed datatypes?
Datatypes with constraints on parameters.
Example:
Beautiful (n:Nat) with rules like:
B0 [n=0]
Bsum [n=m1+m2]
180
What are the key datatypes in PiForall?
Bool → True/False
Void → no values
Nat → numbers
Maybe → optional values
Sigma → dependent pairs
Beautiful → indexed with constraints
181
What are the leftmost‑outermost evaluation rules for applications?
App‑Left: If 𝑒1→𝑒1′, then (𝑒1 𝑒2)→(𝑒1′ 𝑒2).
App‑Beta: (𝜆𝑥.𝑒) 𝑣→𝑒[𝑥:=𝑣].
Always reduce the outermost application first.
182
Cons?
(m : Nat) → A → Vec A m → Vec A (Succ m)
183
head?
head : (A : Type) → (n : Nat) → Vec A (Succ n) → A
“Give me a type A, a natural number n, and a vector of length n+1 containing elements of type A, and I will return an element of type A.”
aka first element of the vector
184
maybe?
data Maybe (A : Type) : Type where
Nothing : Maybe A
Just : A → Maybe A
185
beautiful?
data Beautiful (n : Nat) : Type where
B0 : [n = 0]
B3 : [n = 3]
B5 : [n = 5]
Bsum : (m1 : Nat) → (m2 : Nat) →
Beautiful m1 → Beautiful m2 →
[n = m1 + m2]
revision
flashcards
Decks in class (12)
# Cards
