咖喱 - 霍达同构产生的最有趣的等效是什么？
https://stackoverflow.com/questions/2969140
-
24-10-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
Russian题
我遇到了 咖喱 - 霍达同构 在我的编程生活中相对较晚，也许这有助于我对此完全着迷。这意味着对于每个编程概念，都存在正式逻辑中的精确类似物，反之亦然。这是我头顶上的类比的“基本”列表：
program/definition | proof
type/declaration | proposition
inhabited type | theorem/lemma
function | implication
function argument | hypothesis/antecedent
function result | conclusion/consequent
function application | modus ponens
recursion | induction
identity function | tautology
non-terminating function | absurdity/contradiction
tuple | conjunction (and)
disjoint union | disjunction (or) -- corrected by Antal S-Z
parametric polymorphism | universal quantification
所以，我的问题： 这种同构的更有趣/晦涩的含义是什么？ 我不是逻辑学家，所以我敢肯定我只用这个列表划过表面。
例如，以下是一些编程概念，我不知道逻辑中的精确名称：
currying | "((a & b) => c) iff (a => (b => c))"
scope | "known theory + hypotheses"
这是一些逻辑概念，我还没有完全固定在编程术语中：
primitive type? | axiom
set of valid programs? | theory
编辑：
以下是从回答中收集的更多等价：
function composition | syllogism -- from Apocalisp
continuation-passing | double negation -- from camccann
解决方案
由于您明确要求最有趣，最晦涩的人：
您可以将CH扩展到许多有趣的逻辑和逻辑表述，以获得各种各样的对应关系。在这里，我试图专注于一些更有趣的东西，而不是晦涩难懂，还有几个尚未出现的基本。
evaluation | proof normalisation/cut-elimination
variable | assumption
S K combinators | axiomatic formulation of logic
pattern matching | left-sequent rules
subtyping | implicit entailment (not reflected in expressions)
intersection types | implicit conjunction
union types | implicit disjunction
open code | temporal next
closed code | necessity
effects | possibility
reachable state | possible world
monadic metalanguage | lax logic
non-termination | truth in an unobservable possible world
distributed programs | modal logic S5/Hybrid logic
meta variables | modal assumptions
explicit substitutions | contextual modal necessity
pi-calculus | linear logic
编辑：我建议任何有兴趣了解有关CH的扩展的人的参考：
“模态逻辑的判断重建” http://www.cs.cmu.edu/~fp/papers/mscs00.pdf - 这是一个开始的好地方，因为它始于第一原则，其中大部分旨在可供非逻辑学家/语言理论家使用。 （虽然我是第二作者，所以我有偏见。）
其他提示
关于非终止的事情，您正在弄乱一些事情。虚假是由 无人类型, ，从定义上讲，这不是没有终止的，因为首先没有这种类型的评估。
非终止代表 矛盾- 不一致的逻辑。当然是不一致的逻辑意志 允许您证明 任何事物, ，包括虚假。
忽略不一致之处，类型系统通常对应于 直觉逻辑, ，并且有必要 建构主义者, ，这意味着某些古典逻辑无法直接表达，如果有的话。另一方面，这很有用，因为如果一种类型是有效的建设性证明，那么该类型的术语为一个 构建您证明存在的任何东西的手段.
建构主义风味的主要特征是 双重否定 不等于非束缚。实际上，否定很少是类型系统中的原始性，因此我们可以表示它是暗示虚假的，例如，例如 not P 变成 P -> Falsity. 。因此，双重否定将是类型的函数 (P -> Falsity) -> Falsity, ，显然不等于仅类型的东西 P.
但是，这有一个有趣的转折！在具有参数多态性的语言中，类型变量在所有可能的类型（包括无人居住的类型）中范围范围，因此完全多态类型 ∀a. a 从某种意义上说，几乎是false。那么，如果我们通过使用多态性写两次几乎几乎束缚怎么办？我们得到了这样的类型： ∀a. (P -> a) -> a. 。这等同于类型 P? 它的确是, ，仅将其应用于身份函数。
但是重点是什么？为什么写这样的类型？可以 意思是 编程术语中有什么吗？好吧，您可以将其视为已经具有类型的功能 P 在某个地方，需要您给它一个功能 P 作为一个论点，整个过程在最终结果类型中是多态的。从某种意义上说，它代表 暂停计算, ，等待其余的提供。从这个意义上讲，这些悬浮的计算可以合并在一起，通过，调用，无论如何。某些语言的粉丝（例如方案或红宝石）应该开始熟悉这听起来 - 因为这是什么意思是 双重接种对应 延续通过的风格, ，实际上，我上面给的类型正是Haskell中的延续单元。
您的图表不太正确；在许多情况下，您将类型与术语混淆。
function type implication
function proof of implication
function argument proof of hypothesis
function result proof of conclusion
function application RULE modus ponens
recursion n/a [1]
structural induction fold (foldr for lists)
mathematical induction fold for naturals (data N = Z | S N)
identity function proof of A -> A, for all A
non-terminating function n/a [2]
tuple normal proof of conjunction
sum disjunction
n/a [3] first-order universal quantification
parametric polymorphism second-order universal quantification
currying (A,B) -> C -||- A -> (B -> C), for all A,B,C
primitive type axiom
types of typeable terms theory
function composition syllogism
substitution cut rule
value normal proof
1] Turing-Complete功能语言的逻辑是不一致的。递归在一致的理论中没有对应关系。在不一致的逻辑/不健全的证据理论中，您可以称其为导致不一致/不恢复性的规则。
2]再次，这是完整性的结果。如果逻辑是一致的，这将是反理论的证明 - 因此，它不存在。
3]在功能语言中不存在，因为它们具有一阶逻辑特征：所有量化和参数化均在公式上完成。如果您有一阶功能，那么有一种 *, * -> *, ， ETC。;话语领域的元素。例如，在 Father(X,Y) :- Parent(X,Y), Male(X), X 和 Y 在话语领域范围（称之为） Dom）， 和 Male :: Dom -> *.
function composition | syllogism
我真的很喜欢这个问题。我不知道很多，但是我确实有几件事（协助 Wikipedia文章, ，有一些整洁的桌子等）：
我认为总类型/工会类型（例如
data Either a b = Left a | Right b）等同于 包括的 析取。而且，尽管我不太了解咖喱 - 咖喱，但我认为这证明了这一点。考虑以下功能：andImpliesOr :: (a,b) -> Either a b andImpliesOr (a,_) = Left a如果我正确理解事情，类型说（一个 ∧ b) → (一个 ★ b）和定义说这是正确的，其中★是包容性或独家
Either代表。你有Either代表独家或⊕;然而， （一个 ∧ b) ↛ (一个 ⊕ b）。例如，⊤∧⊤⊤⊤⊤⊤，但是⊤⊕⊥⊥⊥⊥⊥⊥⊥⊥⊥⊥⊥⊥⊥⊥。换句话说，如果两者都 一个 和 b 是正确的，那么假设是正确的，但结论是错误的，因此这种含义必须是错误的。但是，很明显（（一个 ∧ b) → (一个 ∨ b），因为如果两者都 一个 和 b 是真的，那么至少一个是真实的。因此，如果歧视工会是某种形式的脱节形式，则必须是包容性的品种。我认为这是一个证明，但感觉不仅可以自由地解除我的这个概念。同样，您对重言式和荒谬的定义分别是身份函数和非终止功能的定义有些关闭。真正的公式由 单位类型, ，这是只有一个元素的类型（
data ⊤ = ⊤;经常拼写()和/或Unit在功能编程语言中）。这是有道理的：因为那种类型是 保证 要居住，由于只有一个可能的居民，这一定是正确的。身份函数仅表示特定的重言术 一个 → 一个.您对非终止功能的评论是，取决于您的含义，更多。咖喱 - 霍华德在类型系统上的功能，但在那里没有编码非终止。根据 维基百科, ，处理非终止是一个问题，因为添加它会产生不一致的逻辑（例如, ，我可以定义
wrong :: a -> b经过wrong x = wrong x, ，因此“证明” 一个 → b 任何 一个 和 b）。如果这是您所说的“荒谬”，那么您是完全正确的。相反，如果您的意思是错误的陈述，那么您想要的是任何无人类型的类型， 例如 定义的东西data ⊥- 也就是说，一个数据类型，无需任何构建它。这确保了它根本没有价值观，因此必须无人居住，这等同于虚假。我认为你也可能会使用a -> b, ，由于如果我们禁止非终止功能，那么这也是无人居住的，但我不是100％确定的。维基百科 说公理是通过两种不同的方式编码的，具体取决于您如何解释咖喱豆：在组合者或变量中。我认为组合仪视图意味着我们给出的原始函数默认情况下可以说的话（类似于Modus Ponens是公理的方式，因为功能应用程序是原始的）。和我 思考 变量视图实际上可能意味着同一件事 - 毕竟，combinator只是特定函数的全局变量。至于原始类型：如果我正确考虑这一点，那么我认为原始类型是实体，即我们试图证明事物的原始对象。
根据我的逻辑和语义课，这一事实（一个 ∧ b) → C ≡ 一个 → (b → C）（还有 b → (一个 → C））称为出口等效法，至少在自然推论证明中。当时我没有注意到它只是在咖喱 - 我希望我有，因为那很酷！
虽然我们现在有办法代表 包括的 脱节，我们没有办法代表独家品种。我们应该能够使用独家脱节的定义来表示： 一个 ⊕ b ≡ (一个 ∨ b) ∧ ¬(一个 ∧ b）。我不知道如何写否定，但是我确实知道p ≡ p→⊥，含义和虚假都很容易。因此，我们应该能够通过以下方式代表独家脱节。
data ⊥ data Xor a b = Xor (Either a b) ((a,b) -> ⊥)这是定义的
⊥是没有值的空类型，与虚假相对应；Xor然后定义为包含两个（和)Either一个 一个 或a b (或者）和一个函数（含义） 从 （a，b） (和）到底部类型（错误的).但是，我不知道这是什么 方法.(编辑1： 现在我这样做了，请参阅下一段！）由于没有类型的值(编辑1： 是的， 马车.)(a,b) -> ⊥（有吗？），我无法理解这个程序的含义。有人知道一种更好的方法来考虑这个定义还是另一个定义？编辑1： 谢谢 卡甘的答案 （尤其是，他留下的评论以帮助我），我想我看到这里发生了什么。构建类型的值
Xor a b, ，您需要提供两件事。首先，见证了一个元素的存在a或者b作为第一个论点；这是一个Left a或aRight b. 。其次，证明两种类型都没有元素a和b换句话说，证明了(a,b)是无人居住的 - 第二个论点。因为您只能从中写一个函数(a,b) -> ⊥如果(a,b)是无人居住的，这是什么意思？这意味着类型对象的某些部分(a,b)无法构建；换句话说，至少一个，甚至可能是a和b也无人居住！在这种情况下，如果我们正在考虑模式匹配，那么您不可能在这样的元组上进行模式匹配：假设b是无人居住的，我们写的是什么可以匹配该元组的第二部分？因此，我们无法与之匹配，这可能会帮助您了解为什么这使它无人居住。现在，拥有不采用参数的总函数的唯一方法（因为这是必须的，因为(a,b)是无人居住的）结果也是一个无人类型的类型 - 如果我们从模式匹配的角度考虑这一点，这意味着即使功能没有案例，也没有可能 身体 它可能有，所以一切都很好。
很多都是我大声/示意（希望）即时的事情，但我希望它很有用。我真的推荐 Wikipedia文章;我没有任何细节阅读它，但是它的表格是一个非常不错的摘要，而且非常详尽。
这是一个有点晦涩的人，我感到惊讶的是没有早些时候提出：“古典”功能反应性编程对应于时间逻辑。
当然，除非您是哲学家，数学家或强迫症的程序员，否则这可能会提出更多问题。
因此，首先关闭：什么是功能性反应性编程？这是一种声明的方式 时变值. 。这对于编写用户界面之类的内容很有用，因为用户的输入是随时间变化的值。 “古典” FRP有两种基本数据类型：事件和行为。
事件表示仅在离散时间存在的值。击键是一个很好的例子：您可以在给定时间将键盘的输入视为角色。然后，每个按键只是一对与钥匙的字符和按下的时间。
行为是不断存在但可以不断变化的价值观。鼠标位置是一个很好的例子：它只是x，y坐标的行为。毕竟，鼠标 总是 在概念上有一个位置，并且这个位置改变了 不断 当您移动鼠标时。毕竟，移动鼠标是一个持久的动作，而不是一堆离散的步骤。
什么是时间逻辑？足够适当地，这是一组逻辑规则，用于处理随着时间的推移量化的命题。从本质上讲，它通过两个量词扩展了正常的一阶逻辑：□和◇。第一个表示“始终”：读取□φ为“φ总是保持”。第二个是“最终”：◇φ是指“最终将保持”。这是一种特殊的 模态逻辑. 。以下两个法律与量化符有关：
□φ ⇔ ¬◇¬φ
◇φ ⇔ ¬□¬φ
因此，□和◇彼此双重与∀和∃相同。
这两个量词对应于FRP中的两种类型。特别是，□对应于行为，◇对应于事件。如果我们考虑这些类型的居住方式，这应该是有道理的：行为是居住在的 每一个 可能的时间，而事件只发生一次。
与连续性与双重否定之间的关系有关，通话/CC的类型是Peirce定律 http://en.wikipedia.org/wiki/call-with-current-continature
CH通常称为直觉逻辑和程序之间的对应关系。但是，如果我们添加呼叫 - 电流通信（CallCC）操作员（其类型与Peirce定律相对应），我们会在 古典逻辑 和CallCC的程序。
虽然这不是一个简单的同构，但 关于建设性LEM的讨论 是一个非常有趣的结果。特别是，在“结论”部分中，Oleg Kiselyov讨论了如何在建设性逻辑中使用单调消除双重否定的方法类似于区分计算可决定的命题（在建设性环境中为LEM有效）与所有命题。单调捕获计算效应的概念是一个古老的效果，但是咖喱的实例 - 霍华德同构有助于将其视为视角，并有助于获得双重否定的真正“意思”。
一流的连续支持使您可以表达$ p lor neg p $。诀窍是基于以下事实：不称呼延续并以某种表达方式退出等同于以相同的表达方式调用延续。
有关更多详细视图，请参阅： http://www.cs.cmu.edu/~rwh/courses/logic/www old/handouts/callcc.pdf
2-continuation | Sheffer stoke
n-continuation language | Existential graph
Recursion | Mathematical Induction
重要的一件事，但尚未进行调查是2次接触的关系（连续2个参数）和 谢弗中风. 。在经典逻辑中，Sheffer Stroke可以自己形成一个完整的逻辑系统（加上一些非操作员概念）。这意味着熟悉的 and, or, not 只能使用Sheffer Stoke或 nand.
这是其编程类型对应关系的重要事实，因为它提示可以使用单一类型组合器来形成所有其他类型。
2次接触的类型签名是 (a,b) -> Void. 。通过此实施，我们可以将1个登机（正常连续性）定义为 (a,a) - > void，产品类型为 ((a,b)->Void,(a,b)->Void)->Void, ，总和类型为 ((a,a)->Void,(b,b)->Void)->Void. 。这给我们带来了令人印象深刻的表现力。
如果我们进一步挖掘，我们会发现那件作品 存在图 等同于唯一数据类型的语言是n-contination，但是我没有看到任何现有语言以这种形式。因此，我认为发明一个可能很有趣。
