Haskell lambda expressions and simple logical formulas

Question

I have a misunderstanding when converting a simple logical formula to a lambda expression (proof of this formula).

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

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

I have some "results", but I'm really not sure if this is the right way to do this:

• (((lambda F → lambda A) → A) → lambda B) → B
• (((((lambda A → lambda B) → A) → A) → B) → B.

How can I convert a formula to a lambda expression? It will be very useful if you know that some material relates to this problem.

thanks

Answer 1

This is a great time to use Agda Interactive Mode. It is like a game. You can also do it manually, but it works more. Here is what I did:

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

Basically the only thing we have is to apply x , so try this.

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

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

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

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

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

Our goal is a type of function, so use lambda.

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

Now we need B , and the only thing B can give us is x , so try again.

 f : {AB : Set} -> ((((A -> B) -> A) -> A) -> B) -> B fx = 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 the type of function returning A , but we have z , which is A , so we do not need to use an argument. We just ignore it and return z .

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

And here you go!