Haskell lambda表达式和简单逻辑公式

Question

将简单逻辑公式转换为lambda表达式（该公式的证明）时，我有一个误解。 （（（（A→B）→A）→A）→B）→B这里意味着蕴涵逻辑运算符。

我该如何写一些函数式语言（最好是Haskell）的lambda表达式对应它？

我有一些 “成果”，但我真的不知道它是做这个正确的方法：

• （（（拉姆达的F - >拉姆达A） - > A） - >拉姆达B） - >乙
• （（（（拉姆达A - >拉姆达B） - > A） - > A） - > B） - > B.

岂是能够变换分析式入λ表达？如果您知道某些材料涉及此问题，这将非常有帮助。

感谢

Answer 1

这是一个伟大的时刻使用Agda的交互模式。这就像一场比赛。你也可以手动完成它，但这是更多的工作。下面是我所做的：

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

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

基本上我们唯一的举动是应用x，所以让我们尝试。

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

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

现在我们的目标是一个函数类型，所以我们来试试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 

我们需要一个A，并y可以把它给我们，如果我们为它提供正确的说法。不知道那是什么呢，但y是我们最好的选择：

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 

我们的目标是函数类型，因此我们使用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 

现在我们需要一个B，这可以给我们一个B的唯一事情是x，让我们再试一次。现在

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 

我们的目标是函数类型返回A，但我们有z这是一个A所以我们并不需要使用的参数。我们将忽略它并返回z。

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

然后你去！