Espressioni lambda Haskell e formule a logica semplice

Question

Ho un malinteso durante la conversione di una formula logica semplice in un'espressione lambda (prova di tale formula).

Quindi, ho la seguente formula: ((((A-> B) -> A) -> A) -> B) -> B dove -> significa operatore logico implicato.

Come posso scrivere un'espressione lambda in qualsiasi linguaggio funzionale (Haskell, preferibilmente) corrispondente ad esso?

devo alcuni "risultati" ma sono in realtà non sono sicuro che sia corretto modo per farlo:

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

Come può essere possibile trasformata di formula in lambda espressione? Sarà molto utile se sai che alcuni materiali si riferiscono a questo problema.

Grazie

Answer 1

Questo è un grande momento di utilizzare la modalità interattiva Agda s'. È come un gioco. Puoi anche farlo manualmente ma è più lavoro. Ecco quello che ho fatto:

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

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

In sostanza l'unica mossa che abbiamo è di applicare x, quindi cerchiamo di provare che.

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

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

Ora il nostro obiettivo è un tipo di funzione, quindi proviamo un 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 

abbiamo bisogno di un A, e y può dare a noi se mettiamo a disposizione con l'argomento giusto. Non sono sicuro di cosa si tratta ancora, ma y è la nostra migliore scommessa:

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 

Il nostro obiettivo è un tipo di funzione in modo usiamo un 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 

Ora abbiamo bisogno di un B, e l'unica cosa che ci può dare una B è x, quindi proviamo di nuovo.

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 

Ora il nostro obiettivo è un tipo di funzione che restituisce A, ma abbiamo z che è un A quindi non c'è bisogno di utilizzare l'argomento. Lo ignoreremo e restituiremo z.

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

E ci si va!