Du befindest dich hier: FSI Informatik » Prüfungsfragen und Altklausuren » Hauptstudiumsprüfungen » Lehrstuhl 8 » Propositions as Types
Inhaltsverzeichnis
The atmosphere was OK but not great, at points I struggled to understand what the question was about, especially when the questions were very vague.
Propositions as Types
- We start with the concept of „Propositions as types“, and what that is all about.
- The idea is that we can think of a proposition that is satisfiable as a type that can be inhibited.
- Can I give an example?
- The first one that comes to my mind is that function type (A →
B) correspond to logical implication (ϕ → ψ).
- There is a simpler example?
- The next one that comes to mind is that the pair type (A \times B) corresponds logical conjunction (ϕ ∧ ψ).
- Even simpler!
- How about the correspondence between the empty type (⊥) and falsum or the unit type (⊤) and truth?
- This is what he wanted to hear?
Dependent Pairs and Sums
- What to dependent pairs (Π) and dependent sums (Σ) correspond to?
- Universal and existential quantification. I also add that the thing about existential quantification in constructive logic is that it requires a witness to prove the quantified statement, and this is the first element of the pair.
- Can I show how to create a disjunct union (coproducts, \uplus) using a dependent pair?
- I misunderstand the question and write down how to create an (independent) product „∃ A (λ _ . B)“, but quickly notice that I was mistaken and write down „∃ Bool (λ b . if b then A else B)“
- Can I show how to create a pair (\times) using a dependent pair?
- I point to my mistaken previous definition for disjunct unions, but there was some misunderstanding and my answer was not accepted. I insisted in confusion that this should be the solution, and after a moment the confusion is resolved.
MLTT
- What is MLTT all about?
- What do you mean?
- I try to remember the HOTT slides but cannot recall everything correctly.
- How many rules are there?
- The answer 5 is wrong
- Can I give the rules for contex construction.
- I fail to guess what he is talking about.
Guest Contribution: MLTT
(The following is what the MLTT chapter was supposed to be about, from what a friend told me)
- What is MLTT?
- It is a formal system.
- What are the „ingredients“?
- Terms which also serve as types
- Typing judgements
- Judgemental equality
- Contexts and well-formed context judgements
- What is the elimination rule for the bottom type?
- (See HOTT slides)
Agda
- Can I formalise „(A → ¬ A) → A → B“ in Agda?
- I translate the proposition into a type and try to prove it but get stuck because I was unnecessarily confused by the „(A → ¬ A)“. I explain that this is actually „(A → A → ⊥)“, but forget to mention ⊥ means you cannot inhibit the type. Before I waste more time I am asked another question
- Can I formalise disjunction elimination „(A → C) → (B → C) → (A ∨ B) → C“?
- I write down the type and definition without too many issues.
Closing Notes
- I am asked if I can write down the definition of the J eliminator.
- No. (It appears this was just a bonus question)
The final grade is 1.7 (where I had both a 1.7 in the exam and the exercises). I am disappointed but to be fair, I had no idea what the exam will be about and didn't study the stuff that was actually part of the exam, so in practice I went in unprepared. Considering that, 1.7 wasn't that bad.