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

Question

在将简单的逻辑公式转换为lambda表达式时,我有一个误解(证明了该公式).

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

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

我有一些"结果",但我真的不确定这是否正确:

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

如何将公式转换为lambda表达式？如果您知道某些材料涉及此问题,将会非常有帮助.

谢谢

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)))

你去吧!