Tom*_*ett 93 formal-methods functional-programming curry-howard
我在编程生涯中相对较晚地遇到了Curry-Howard Isomorphism,也许这有助于我对它完全着迷.这意味着对于每个编程概念,在形式逻辑中存在精确的模拟,反之亦然.这是一个关于这种类比的"基本"列表,在我的头脑中:
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
RD1*_*RD1 32
既然你明确要求最有趣和最模糊的:
您可以将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 - 这是一个很好的起点,因为它从第一原则开始,其中大部分都是为了非逻辑学家/语言理论家可以使用.(我是第二作者,所以我有偏见.)
C. *_*ann 25
对于不确定的问题,你有点混乱.虚假是由无人居住的类型表示的,根据定义,它们不能是非终止的,因为首先要评估的是这种类型.
非终止代表矛盾 - 不一致的逻辑.然而,不一致的逻辑将允许您证明 任何事情,包括虚假.
忽略不一致性,类型系统通常对应于直觉主义逻辑,并且必然是建构主义者,这意味着某些经典逻辑片段不能直接表达,如果有的话.另一方面,这很有用,因为如果一个类型是一个有效的建设性证据,那么这个类型的术语就是构建你已经证明存在的任何东西的一种方法.
建构主义风格的一个主要特征是双重否定不等于非否定.事实上,否定在类型系统中很少是原始的,所以我们可以将其表示为暗示虚假,例如,not P成为P -> Falsity.因此,双重否定将是具有类型的函数(P -> Falsity) -> Falsity,其显然不等于仅仅类型的函数P.
然而,这有一个有趣的转折!在具有参数多态性的语言中,类型变量的范围涵盖所有可能的类型,包括无人类型,因此完全多态类型?a. a在某种意义上几乎是假的.那么如果我们通过使用多态来编写双重几乎否定呢？我们得到一个看起来像这样的类型:?a. (P -> a) -> a.这相当于什么类型P？实际上,它只是将其应用于身份功能.
但重点是什么？为什么写这样的类型？在编程术语中它是否意味着什么？好吧,你可以把它想象成一个已经有某种类型的函数P,并且需要你给它一个P作为参数的函数,整个事物在最终结果类型中是多态的.从某种意义上说,它代表一个暂停的计算,等待其余的提供.从这个意义上说,这些暂停的计算可以组合在一起,传递,调用,等等.对于一些语言的粉丝来说,这应该开始听起来很熟悉,比如Scheme或Ruby - 因为它意味着双重否定对应于延续传递风格,实际上我上面提到的类型正是Haskell中的延续monad.
Fra*_*sow 15
你的图表不太合适; 在许多情况下,您将类型与术语混淆.
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]图灵完备功能语言的逻辑是不一致的.递归在一致的理论中没有对应关系.在一个不一致的逻辑/不健全证明理论中,你可以称之为一个导致不一致/不健全的规则.
[2]同样,这是完整性的结果.如果逻辑是一致的,这将是反定理的证明 - 因此,它不可能存在.
[3]在函数式语言中不存在,因为它们忽略了一阶逻辑特征:所有量化和参数化都是在公式上完成的.如果你有一阶特性,会有比其他一类*,* -> *等等; 话语领域的那种元素.例如,在Father(X,Y) :- Parent(X,Y), Male(X),X和Y范围在话语的域(称之为Dom),和Male :: Dom -> *.
Ant*_*sky 13
我真的很喜欢这个问题.我不是很了解,但我确实有一些东西(在维基百科的文章的帮助下,它有一些整齐的表格本身):
我认为和类型/联合类型(例如 data Either a b = Left a | Right b)等同于包容性分离.而且,尽管我对库里 - 霍华德并不熟悉,但我认为这证明了这一点.考虑以下功能:
andImpliesOr :: (a,b) -> Either a b
andImpliesOr (a,_) = Left a
如果我理解正确的事情,类型说(一 ∧ b)→(一 ★ b)和定义说,这是真的,哪里★或者是包容还是排斥,或取其Either代表.你Either代表独家或,⊕; 然而,(一个 ∧ b)↛(一个 ⊕ b).例如,⊤∧⊤≡⊤,但是⊤⊕⊥≡⊥和⊤↛⊥.换句话说,如果a和b都是真的,那么假设是正确的,但结论是错误的,所以这个含义必定是假的.然而,很明显,(一个 ∧ b)→(一个 ∨ b),因为如果a和b都是真的,那么至少有一个是真的.因此,如果受歧视的工会是某种形式的分离,那么它们必须是包容性的种类.我认为这可以作为一个证据,但我觉得这个概念不仅仅是自由地消除了我.
同样,您对重言式和荒谬性的定义分别作为身份函数和非终止函数,有点过时.真正的公式由单元类型表示,单元类型只有一个元素(data ? = ?通常拼写()和/或Unit在函数式编程语言中).这是有道理的:因为这种类型保证有人居住,并且因为只有一个可能的居民,所以一定是真的.身份函数只代表a → a的特定重言式.
您对非终止功能的评论取决于您的意思,更多关闭.Curry-Howard在类型系统上起作用,但非终止不在那里编码.根据维基百科,处理不终止是一个问题,因为其添加产生不一致的逻辑(例如,我可以定义wrong :: a -> b通过wrong x = wrong x,并且因此"证明" 一 → b为任何一个和b).如果这就是你所说的"荒谬",那么你就完全正确了.如果你的意思是错误的陈述,那么你想要的是任何无人居住的类型,例如由...定义的东西data ? - 也就是说,没有任何方法来构造它的数据类型.这确保它根本没有值,因此它必须是无人居住的,这相当于false.我想你也可以使用a -> b,因为如果我们禁止非终止功能,那么这也是无人居住的,但我不是百分之百肯定.
维基百科说,公理是以两种不同的方式编码的,这取决于你如何解释库里 - 霍华德:无论是在组合者中还是在变量中.我认为组合子视图意味着我们给出的基本函数编码我们可以默认说的东西(类似于modus ponens是公理的方式,因为函数应用是原始的).而且我认为变量视图实际上可能意味着同样的事情 - 毕竟,组合器只是全局变量,它们是特定的函数.至于原始类型:如果我正确地考虑这个,那么我认为原始类型是实体 - 我们试图证明事物的原始对象.
按照我的逻辑和语义类,事实上,(一 ∧ b)→ c ^ ≡ 一 →(b → c ^)(也即b →(一 → C ^))被称为出口等价定律,至少在自然演绎证明.我当时没有注意到它只是在晃动 - 我希望我有,因为那很酷!
虽然我们现在有办法表示包容性分离,但我们没有办法代表独家品种.我们应该能够使用异或的定义来表示它:一个 ⊕ b ≡(一 ∨ b)∧¬(一 ∧ b).我不知道怎么写的否定,但我确实知道,¬ p ≡ p →⊥,都蕴涵和谎言很容易.因此,我们应该能够通过以下方式代表排他性分离:
data ?
data Xor a b = Xor (Either a b) ((a,b) -> ?)
这定义?为没有值的空类型,对应于虚假; Xor然后定义为包含两个(和)Either的一个或一个b(或)和一个函数(蕴涵从)(A,B) (和)至底部类型(假). 但是,我不知道这意味着什么. (编辑1:现在我做,看下一段!) 因为没有类型的值 (编辑1:是的,camccann.)(a,b) -> ?(有吗？),我无法理解这在程序中意味着什么.有没有人知道更好的方式来考虑这个定义或另一个定义？
编辑1:感谢camccann的回答(更具体地说,他留下的评论可以帮助我),我想我知道这里发生了什么.要构造类型的值Xor a b,您需要提供两件事.首先,证明存在任何一个元素a或b作为第一个参数; 也就是说,a Left a或a Right b.第二,一个证明,有没有这两种类型的元件a和b-换句话说,即证明(a,b)无人居住-作为第二个参数.既然你只能将能写从功能(a,b) -> ?,如果(a,b)是无人居住的,这是什么意思为要这样呢？这意味着类型对象的某些部分(a,b)无法建造; 换句话说,至少有一个,并且可能,既a和b无人居住的!在这种情况下,如果我们考虑模式匹配,你就不可能在这样的元组上进行模式匹配:假设它b是无人居住的,我们会写什么可以匹配该元组的第二部分？因此,我们无法对其进行模式匹配,这可能会帮助您了解为什么这会使其无人居住.现在,有一个不带参数的总函数的唯一方法(因为这个必须,因为(a,b)无人居住)是因为我们从模式匹配的角度考虑这个问题,结果也是无人居住的类型,这意味着即使函数没有任何情况,也没有可能的正文 它可以有,所以一切都好.
很多这是我在忙着大声思考/证明(希望)的东西,但我希望它是有用的.我真的推荐维基百科文章 ; 我没有仔细阅读它,但它的表格是一个非常好的总结,它非常彻底.
Tik*_*vis 12
这是一个有点模糊的,我很惊讶没有提到:"经典"功能反应式编程对应于时态逻辑.
当然,除非你是一位哲学家,数学家或强迫性的函数式程序员,否则这可能会带来更多问题.
那么,首先:什么是功能反应式编程？这是一种使用时变值的声明方式.这对于编写用户界面之类的东西很有用,因为来自用户的输入是随时间变化的值."经典"FRP有两种基本数据类型:事件和行为.
事件表示仅在离散时间存在的值.击键是一个很好的例子:您可以将键盘输入视为给定时间的角色.然后每个按键只是一对按键的字符和按下的时间.
行为是不断存在但可以不断变化的价值观.鼠标位置就是一个很好的例子:它只是x,y坐标的行为.毕竟,鼠标总是有一个位置,从概念上讲,当你移动鼠标时,这个位置会不断变化.毕竟,移动鼠标是一个单一的延长动作,而不是一堆不连续的步骤.
什么是时间逻辑？恰当地说,它是一套用于处理随时间量化的命题的逻辑规则.从本质上讲,它通过两个量词扩展了正常的一阶逻辑:□和◇.第一个意思是"总是":读□φ为"φ始终保持".第二个是"最终":◇φ表示"φ最终会保持".这是一种特殊的模态逻辑.以下两个定律涉及量词:
?? ? ¬?¬?
?? ? ¬?¬?
所以□和◇以∀和same相同的方式相互对立.
这两个量词对应于FRP中的两种类型.特别是,□对应于行为,◇对应于事件.如果我们考虑这些类型是如何居住的,这应该是有意义的:行为在每个可能的时间都有人居住,而事件只发生一次.
与延续和双重否定之间的关系有关,呼叫/ cc的类型是Peirce定律http://en.wikipedia.org/wiki/Call-with-current-continuation
CH通常被称为直觉主义逻辑和程序之间的对应关系.但是,如果我们添加call-with-current-continuation(callCC)运算符(其类型对应于Peirce定律),我们将使用callCC 获得经典逻辑和程序之间的对应关系.
虽然这不是一个简单的同构，但对构造性 LEM 的讨论是一个非常有趣的结果。特别是，在结论部分，Oleg Kiselyov 讨论了如何使用单子在构造性逻辑中实现双重否定消除，这类似于将计算可判定命题（LEM 在构造性设置中有效）与所有命题区分开来。单子捕获计算效果的概念是一个古老的概念，但库里-霍华德同构的这个例子有助于正确地看待它，并有助于理解双重否定的真正“含义”。
2-continuation | Sheffer stoke
n-continuation language | Existential graph
Recursion | Mathematical Induction
重要但尚未调查的一件事是 2-continuation（需要 2 个参数的延续）和Sheffer stroke 的关系。在经典逻辑中，谢弗笔画可以自己形成一个完整的逻辑系统（加上一些非算子的概念）。这意味着大家熟悉的and，or，not可以仅使用谢弗行程来实现，或者nand。
这是其编程类型对应的一个重要事实，因为它提示可以使用单个类型组合器来形成所有其他类型。
2-continuation 的类型签名是(a,b) -> Void。通过这个实现，我们可以将 1-continuation（正常延续）定义为(a,a)-> Void，乘积类型为((a,b)->Void,(a,b)->Void)->Void，和类型为((a,a)->Void,(b,b)->Void)->Void。这让我们对它的表现力印象深刻。
如果我们进一步挖掘，我们会发现 Piece 的存在图相当于一种唯一数据类型是 n-continuation 的语言，但我没有看到任何现有语言是这种形式。所以发明一个可能很有趣，我想。