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

This is a complex problem. The intuitionistic sequent calculus LJ and its related results play key roles in its "standard" solution. The Djinn tool is a "famous" implementation of a proof search in this system (roughly), and the Curry-Howard isomorphism allows to present these proofs as lambda terms. — chi
– chi, Commented Feb 8, 2015 at 18:50
Further, there's no such a thing as "converting" a formula into a lambda expression. That would amount to "converting" theorems into their proofs, which is nonsense -- theorems admits many distinct proofs, in general. At best, you can do proof search, where you look for one such proof. — chi
– chi, Commented Feb 8, 2015 at 18:56
Thank you for clarification. I really glad to so much useful information in short time. — Peter Leontev
– Peter Leontev, Commented Feb 8, 2015 at 20:09

luqui · Accepted Answer · 2015-02-08 19:09:58Z

10

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!

answered Feb 8, 2015 at 19:09

luqui

60.7k12 gold badges153 silver badges210 bronze badges

Sign up to request clarification or add additional context in comments.

4 Comments

Peter Leontev Over a year ago

Wow! That is really best and quickest answer I've ever seen here. Thank you a lot. I've installed Coq and have tried to used it but I can't read the output. It is too complicated :(

Peter Leontev Over a year ago

I will try to use Agda following your advice. It is strange that we do not consider such applications and did all the things by hands even without mentioned rules! Thank you a lot.

Peter Leontev Over a year ago

Ehm, if I understood you right the answer can be rewritten in the following way: x(lambda y -> y(\lambda z -> x (z))) ?

luqui Over a year ago

Not quite. We don't apply z to x, but rather the function which ignores its argument and returns z. In haskell this is written const z or \_ -> z, or lambda q -> z in your notation where q is any unused variable.

Collectives™ on Stack Overflow

Haskell lambda expressions and simple logic formulas

1 Answer 1

4 Comments

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

4 Comments

Your Answer

Sign up or log in

Post as a guest

Related