Finding equivalent program to proof in typed lambda calculus

Question

I have the following proof that assuming A and B, one can derive A ∧ B:

I am trying to find an equivalent program to this proof, in typed lambda calculus using Haskell-style syntax for pairs. It is assumed that a : A and b : B.

Translating this proof to types, one gets: assuming x :: (B,A) one wants to construct (A,B).

I am stuck between two options for this:

(1) (λx. (𝗌𝗇𝖽 x,𝖿𝗌𝗍 x)) (b,a)

(2) (𝗌𝗇𝖽 (b,a),𝖿𝗌𝗍 (b,a))

I believe that it is option (2) that is correct, since it is not an implication (which translates to a function) that is being proved. However I am not sure if my reasoning is correct. Since we are considering this proof in terms of types, where x :: (B,A) is option (1) more appropriate? Any insights are appreciated.

Answer 1

Here is the correct line of reasoning. We will start with a "hole", and slowly expand the hole following the next proof rule. I'll follow your lead and assume there are two terms in scope, named a (of type A) and b (of type B). We start with just a hole:

_

The last proof rule used is →-E (arrow elimination); in the lambda calculus, this corresponds to function application.

_ _

Since the proof term for the second hole is smaller, let's start with that one. That rule is ∧-I (conjunction introduction); the corresponding lambda term is (,).

_ (_, _)

The assumptions used by the conjunction introduction are B and A; our corresponding lambda terms are b and a. So:

_ (b, a)

This concludes this branch of the proof term. Now we must ascend the left branch. The rule used to supply the function is →-I^δ (arrow introduction using variable δ); in lambda calculus, the corresponding term is a lambda.

(\δ -> _) (b, a)

Next up is a conjunction introduction. As before, the corresponding term is (,).

(\δ -> (_, _)) (b, a)

Here the proof branches. For consistency with our previous go, we'll follow the right branch first, then the left branch. The next rule up in the right branch is ∧-E₁ (conjunction elimination 1); the corresponding term in lambda calculus is fst.

(\δ -> (_, fst _)) (b, a)

The last rule in this branch is δ (variable elimination of variable δ); the corresponding lambda calculus term is δ.

(\δ -> (_, fst δ)) (b, a)

Now following the left branch of the proof, the next rule used is ∧-E₂ (conjunction elimination 2) -- snd in the lambda calculus.

(\δ -> (snd _, fst δ)) (b, a)

The final rule used is again variable elimination (again with variable δ).

(\δ -> (snd δ, fst δ)) (b, a)

We have now reached the top of every branch of the proof term (and filled all the holes), so we are done building our lambda calculus term. Looks like it corresponds with your (1)! Can you see how the proof term would have to change to correspond with your (2)?