Wyrażenia lambda Haskella i proste formuły logiczne

Question

Mam nieporozumienie podczas konwersji prostej formuły logicznej na wyrażenie lambda (dowód tej formuły).

Mam zatem następującą formułę: ((((((A-> B) -> A) -> A) -> B) -> B gdzie -> oznacza logiczny operator implikowany.

Jak napisać wyrażenie lambda w jakimkolwiek języku funkcyjnym (najlepiej Haskell)?

mam jakieś "wyniki", ale ja naprawdę nie wiem, że to jest poprawny sposób to zrobić:

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

Jak to może być możliwe tranform wzór do lambda wyrażenie? Będzie to bardzo pomocne, jeśli wiesz, że jakiś materiał odnosi się do tego problemu.

Dzięki

Answer 1

Jest to doskonała okazja, aby skorzystać z trybu interaktywnego Agda „s. To jest jak gra. Możesz także zrobić to ręcznie, ale to więcej pracy. Oto co zrobiłem:

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

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

Zasadniczo tylko ruch mamy stosuje x, więc spróbujmy tego.

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

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

Teraz naszym celem jest typ funkcji, więc spróbujmy 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 

Musimy A i y może dać go do nas, jeśli dostarczenie jej prawego argumentu. Nie wiesz, co to znaczy jeszcze, ale y jest naszym najlepszym:

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 

Naszym celem jest typem funkcja więc użyjmy 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 

Teraz musimy B, a jedyną rzeczą, która może dać nam B jest x, więc spróbujmy jeszcze raz.

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 

Teraz naszym celem jest rodzajem funkcji powrocie A, ale mamy z który jest A więc nie trzeba użyć argumentu. Zignorujemy go i wrócimy na numer z.

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

I gotowe!