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

Question

我在将简单的逻辑公式转换为 lambda 表达式（该公式的证明）时遇到了误解。

所以，我有以下公式： ((((A->B)->A)->A)->B)->B 其中 -> 表示蕴涵逻辑运算符。

如何用与之对应的任何函数式语言（Haskell，最好）编写一些 lambda 表达式？

我有一些 "results" 但我真的不确定这样做是否正确：

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

如何将公式转换为 lambda 表达式？如果您知道一些 material 提到了这个问题，那将会非常有帮助。

谢谢

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

现在我们的目标是函数类型 returning A，但是我们有 z 是 A 所以我们不需要使用参数.我们将忽略它 return z.

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

好了！

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

Haskell lambda expressions and simple logic formulas

lambda

logic

haskell