Haskell lambda expressions and simple logic formulas

Question

I have a misunderstanding while converting simple logic formula to lambda expression (proof of that formula).

So, I have the following formula: ((((A->B)->A)->A)->B)->B where -> means implication logical operator.

How can I write some lambda expression in any functional language (Haskell, preferably) corresponding to it?

I have some "results" but I am really not sure that it is correct way to do this:

• (((lambda F -> lambda A) -> A) -> lambda B) -> B
• ((((lambda A -> lambda B) -> A) -> A) -> B) -> B.

How can it be possible to tranform the formula into lambda expression? It will be very helpful if you know some material refers to this issue.

Thanks

Answer 1

This is a great time to use Agda's interactive mode. It's like a game. You can also do it manually but it's more work. Here's what I did:

f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
f x = ?

Goal: B
x : (((A -> B) -> A) -> A) -> B

Basically the only move we have is to apply x, so let's try that.

f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
f x = x ?

Goal: ((A -> B) -> A) -> A 
x : (((A -> B) -> A) -> A) -> B

Now our goal is a function type, so let's try a lambda.

f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
f x = x (\y -> ?)

Goal: A 
x : (((A -> B) -> A) -> A) -> B
y : (A -> B) -> A

We need an A, and y can give it to us if we provide it with the right argument. Not sure what that is yet, but y is our best bet:

f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
f x = x (\y -> y ?)

Goal: A -> B
x : (((A -> B) -> A) -> A) -> B
y : (A -> B) -> A

Our goal is a function type so let's use a lambda.

f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
f x = x (\y -> y (\z -> ?))

Goal: B
x : (((A -> B) -> A) -> A) -> B
y : (A -> B) -> A
z : A

Now we need a B, and the only thing that can give us a B is x, so let's try that again.

f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
f x = x (\y -> y (\z -> x ?))

Goal: ((A -> B) -> A) -> A
x : (((A -> B) -> A) -> A) -> B
y : (A -> B) -> A
z : A

Now our goal is a function type returning A, but we have z which is an A so we don't need to use the argument. We'll just ignore it and return z.

f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B
f x = x (\y -> y (\z -> x (\_ -> z)))

And there you go!