• Examiner: Tadeusz Litak
• Assessor: Fabian Birkmann (or that is what they would have us believe…)
• Date: 2023-10-05
• Time: 16:00

As inductive data types, one with only one constructor and two Prop arguments, one with two constructors with two Prop arguments.

Implication, for it is notation using forall.

I first go into decidability, explaining what that is and then want to return to equality. I confuse myself, but quickly end up with the definition

forall (a b : t), a = b \/ ~(a = b)

Functional extensionality. I mistakenly write down

forall f, forall a b, f a = f b -> f =

but stop, noticing it is not what we want to define. Instead, we end up with

forall f g, forall a, f a = g a -> f = g

I hesitate, but then point out it would be possible to derive a contradiction. The example I end up with is the functions $f(x) = x$ and $f(x) = 0$ are equal at $x = 0$, and that this equality together with the above mentioned degenerated functional extensionality axiom, we could prove that $0 = 1$.

It allows us to prove anything (ex falso, sequitur quod libet). We can use discriminate… Or inversion.

(I instantly regret mentioning inversion) It introduces a new goal for each constructor and adds the necessary conditions to the context. If there are contradictory hypotheses in the context, the goal is dismissed. I want to start explaining why this helps resolve the above issue with $0 = 1$, but I am interrupted.

I list destruct and discriminate, but cannot think of the third. After a hint wrt initial algebras that doesn't help me out and me somehow mentioning that discriminate works by checking if two sides of an equality have different constructors, I get another hint to think about cases where we have the same constructors and I am reminded of injection.

My first guess is to say axiomatic and operational semantics, and that inside of operational semantics we distinguished between „big step“ and „small step“ semantics. The latter was the actually intended distinction.

I want to start with if, but remembering the braindumps I know that the interesting case is while, so we start with that. I write down the rule, explaining what the assertions mean and minor notational points along the way:

        {Q /\ b} stmts { Q }
———————————–————————————————————————--
{ Q } while b do stmts end { Q /\ ¬b }

No, it is not, because stmts doesn't necessarily terminate, which would be required. At first I believe that I have to give the rule to properly formalise complete correctness, but I am told that is not the case.

Despite the suggestion to use the example from the course, I, an idiot, have the idea to come up with a simpler example

{ X = 1 }
X = X + 1
{ X = 2 }
X = X + 2
{ X = 3 }

This is not satisfactory, so the examiner takes my paper and writes down the „swap“ example, and asks me to annotate it. I quickly write down the first and last assertion.

{ X = a /\ Y = b }
X = X + Y
{ ? }
Y = X - Y
{ ? }
X = X - Y
{ X = b /\ Y = a }

My feeble mind is incapable of writing down the correct decorations, and upon the suggestion to write down the Hoare rule

{ P[x/a] } X := a { P }

I manage to come up with the right assertion for the last hole:

{ X - Y = b /\ Y = a }

My first idea is to give some rules involving truth values, but I instructed to focus on functions instead. The first rule I give involves beta reduction

    value t
———————————————
(λx.s)t → s[x/t]

but forget the value t at first until asked, then proceed to the first application rule

value s  t → t'
———————————————
   st → st'

but forget the value s at first until asked, then proceed to the second application rule

 s → s'
————————
st → s't

I start with the soundness theorem, which turns out to have been a lemma. The actual theorems were the

1. progress theorem, that says that for each well-typed term is either a value or there exists an evaluation step to another term
2. preservation theorem, that say that an evaluation step does not change the term of a type

I sloppily don't write down any context, that initiates a discussion on what one would want to prove and what out theorem from the lecture stated. Our theorem required the terms to be well types in an empty context, since the substitution was not capture avoiding, unbound variables would invalidate the theorem.

—

I am asked to step outside, and after a short while I am allowed to return back into the examiners room. As I hesitated at a few points, and didn't solve the entire homework, the final grade is the average of 1.3 for the exam and 1.3 for the homework.

I am not sure if I forgot something in the above transcript or if all the questions occurred in the order I alleged them to.

Looking back, I should have studied the canonical examples (e.g. the decorated swap example, the peculiarities of our small step evaluation) in more detail.