1

我一直盯着这张脸看了好几个小时不明白:(

我需要使用 coq 解决一些定义，我应该通过 Curry Howard 同构来解决。我已经阅读了，但仍然不知道我在做什么。我查看了其他示例并尝试以这些方式进行操作，但我总是遇到错误。

例如，在这里我需要定义这个：

Variables A B C : Set.

Definition c01 : (A -> B -> C) -> (B -> A -> C) :=

这是我的尝试：

fun g => fun p => g (snd p) (fst p).
end.

我也试过

fun f => fun b => fun a => f (b , a)
end.

最终它只是说它期待的类型与我给出的不同，有时它会说：“预期有类型“？9 * ？10”。”

在阅读了我能找到的所有内容后，我真的很难理解这一点。

请有人解释一下:(

4

1 回答 1

1

好吧，我猜您不知道如何正确读取类型。

c01的类型是(A -> B -> C) -> (B -> A -> C). 这意味着它是一个函数，它将一个函数作为参数并返回一个函数。

它采用 and 类型的“具有两个参数的函数”（我的意思是Haskell意义上的“具有两个参数的函数”，而不是 Scala 或 Java 意义上的），它返回一个 type 的值。ABC

它必须返回一个带有两个参数的函数，类型为A和B（但顺序相反），它返回一个类型的值C。

那么这个函数必须c01做什么呢？

它必须接受一个函数，并将其转换为相同的函数，但其​​参数的顺序颠倒了。

所以：

fun f => fun b => fun a => f a b

或等效地（只是添加一些括号使其更清晰）：

fun f => (fun b => fun a => f a b)
于 2013-11-12T20:45:58.633 回答