问题标签 [curry-howard]

在Propositions as Types中，它是这样写的：

1935 年，年仅 25 岁的根岑 15 引入了两种新的逻辑公式——自然演绎法和连续微积分——这两种方法被确立为制定逻辑的两个主要系统，并且一直保持到今天。他展示了如何规范化证明以确保它们不会“迂回”，从而产生希尔伯特系统一致性的新证明。而且，最重要的是，为了匹配 Peano 引入的存在量化符号 ∃ 的使用，Gentzen 引入了符号 ∀ 来表示全称量化。他将蕴涵写为 A ⊃ B（如果 A 成立，则 B 成立），合取为 A & B（A 和 B 都成立），析取为 A ∨ B（至少 A 或 B 中的一个成立）。

什么是迂回证明？你能举个简单的例子吗？为什么会出现问题？

如果我正确理解 Curry-Howard 的同构，那么每个依赖类型都对应一个定理，实现它的程序就是一个证明。这意味着任何数学问题，例如，a^n + b^n = c^n都可以以某种方式表示为一种类型。

现在，假设我想设计一个生成随机类型（定理）的游戏，并且游戏必须尝试实现这些类型（定理）的程序（证明）。是否有可能控制这些定理的难度？即，简单模式会产生微不足道的定理，而困难模式会产生更难的定理。

我在 Haskell 中实施了四个德摩根定律中的三个：

但是，我认为不可能实施最后一条法律（有两个居民）：

在我看来，有两种可能的解决方案：

1. undefined代替?. _ 这不是一个好的解决方案，因为它是作弊。

2. 使用单态类型或有界多态类型来编码默认值。

   这不是一个好的解决方案，因为它比德摩根定律更弱。

我们知道德摩根定律是正确的，但我假设最后一条定律不能用 Haskell 编码是否正确？这对 Curry-Howard 同构有什么看法？如果每个证明都不能转换成等效的计算机程序，那它就不是真正的同构，对吧？

编辑：Void我的意思是 Haskell 的Void类型，即不能有值但是的空类型undefined。

关于 Swift Evolution 是否将noreturn函数属性替换为实际Void类型的讨论正在进行中。为此，我们必须确保这将为平台带来真正的好处。使用Void作为返回类型是不够的。

所以我要求你提供非常实用的例子，其中的使用Void增加了代码的清晰度、简洁性和通用性。也许它会使用类（在 Haskell 意义上），也许是泛型，也许它会合并Void到 ADT 中。

但是，请不要对 HKT、Monads 和所有高级别的东西走得太远。标准库中的实用函数也是一个不好的例子。一个完美的例子是街机游戏或类似游戏的一部分。

我正在尝试weaken为有限的整数集编写一个函数。我正在使用该singletons软件包。我已经定义并推广了加法、减法和前驱函数，并证明了它们的一些方程以帮助类型检查器。但是我得到的错误与这一切完全无关。

我得到的错误是在weaken( SF (weaken n)) 的递归调用中，如下所示：Could not deduce (SingI n1)， wheren1被正确推断为 type 的类型级前身n。我可以添加一个SingI (Pred n)约束，但这只是将问题降低了一级（GHC 现在说它不能推断出 的等价物(SingI (Pred (Pred n)))）。

我怎样才能说服SingI (Pred n)遵循的GHC SingI n（以及为什么singletons软件包没有这样做）？

简而言之，Curry-Howard 对应表明类型是定理，返回该类型的程序是相应定理的证明。

对应是基于数学证明的形式化，在诸如谓词演算之类的语言中，受限于直觉逻辑。但是当数学证明用这些形式语言编写时，它们的错误可以被计算机检测到。例如，Mizar是一种相对高级的数学语言，加上一个编译器来检查它所写的证明。

因此，Curry-Howard 将程序与数学证明无误地关联起来。因此，Curry-Howard 如何在数学世界中翻译程序错误的概念？综上所述，这不是证明中的逻辑错误。

在维基百科中，底部类型被简单地定义为“没有值的类型”。但是，如果b是这个空类型，那么产品类型(b,b)也没有值，但看起来与b. 我同意底部是无人居住的，但我认为这个属性不足以定义它。

通过Curry-Howard 对应关系，底部与数学错误相关联。现在有一个逻辑原则表明从 False 遵循任何命题。对于Curry-Howard，这意味着该类型forall a. bottom -> a是有人居住的，即存在一个函数族f :: forall a. bottom -> a。

那些功能是f什么？它们是否有助于定义底部，也许是所有类型的无限产物forall a. a？

自从我开始阅读交互式精益教程以来，一个问题一直困扰着我：Prop内部分离层次结构的目的是什么Type？

据我现在了解，我们有以下 Universe 层次结构：

1. 边缘是否?真的有标记，或者我只是弥补它们（可能）？
2. 快速查看 Agda 和 Idris 似乎他们没有区分Sort n和Type n。为什么精益区分它们？

令人感到奇怪的Prop是，一方面它就像一个归纳类型（例如，它是封闭的事实意味着p ∧ nat没有意义），但另一方面却像一种类型一样使用（例如，通过构造一个证明值来显示类型 ）。我怀疑这与区别有关，但我无法表达清楚。有一些基本的论文可以阅读吗？p : Propp

如何在 Scala 中显示没有构造函数的类型的值有任何结果？我想对值进行模式匹配，让 Scala 告诉我没有模式可以匹配，但我愿意接受其他建议。这是一个简短的例子，说明它为什么有用。

证明否定

在 Scala 中，可以在类型级别定义自然数，例如使用 Peano 编码。

由此我们可以定义一个数字是偶数的含义。零是偶数，任何比偶数多二的数也是偶数。

由此我们可以证明例如二是偶数：

但是我无法证明一个不是偶数，即使编译器可以告诉我既不Base也Step不能存在于该类型中。

编译器会很高兴地告诉我，我给出的任何情况都不可能出现 error pattern type is incompatible with expected type，但是将match块留空将是一个编译错误。

有什么方法可以建设性地证明这一点？如果空模式匹配是要走的路 - 我会接受任何版本的 Scala 甚至是宏或插件，只要在类型被占用时我仍然会收到空模式匹配的错误。也许我在叫错树，模式是否匹配错误的想法 - EFQ 可以以其他方式显示吗？

注意：证明一个是奇数可以用另一个（但等效的）均匀度定义来完成——但这不是重点。一个简短的例子说明为什么需要 EFQ：

假设我已经在 Isabelle/HOL 中证明了直觉命题逻辑的一些基本命题：

我从 Curry-Howard 对应关系中知道，命题对应于某种类型(a -> b) -> ((b -> c) -> (a -> c))，而证明对应于某个术语，都在某种类型理论中（例如，在简单类型的 λ 演算中）。从证明的结构，我知道对应的简单类型 λ-项是λf:a→b. λg:b→c. λx:a. f(g(x))。

有没有办法让伊莎贝尔为我建造这个？

我在 Isabelle 中查找了程序提取，据我所知，它主要指的是其他东西：你在 Isabelle 中编写函数式程序，证明关于它们的事情，然后它提供某种对 Haskell 或 ML 的翻译。

我也知道 HOL 与依赖类型理论不同，我理解它具有更强的 Curry-Howard 风格。我知道 HOL 本身在概念上有点像多态 λ-演算，并且我发现了一些关于 HOL 如何是类型论中逻辑的浅层编码的简要说明，但如果能提供更多上下文将不胜感激。我几乎无法将所有这些不同的证明助手及其相关基础如何联系在一起，也许更多的历史背景也会有所帮助。不幸的是，围绕 Isabelle、Coq 等的文档似乎有点乱。特别是对于伊莎贝尔，我似乎经常发现已经过时 20 年的信息。