库里-霍华德同构中最有趣的等价物是什么?

您可以将C-H扩展到许多有趣的逻辑和逻辑公式,以获得真正广泛的对应关系。在这里,我试着把重点放在一些更有趣的问题上,而不是那些晦涩难懂的问题,再加上一些基本的问题,这些问题还没有出现。

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

编辑:我建议有兴趣了解C-H扩展的人参考:

http://www.cs.cmu.edu/~fp/papers/mscs00.pdf -这是一个很好的起点,因为它是从第一原理开始的,而且它的大部分目标是让非逻辑学家/语言理论家能够接触到(我是第二作者,所以我有偏见。)

无人居住类型

不终止代表 矛盾 --前后矛盾的逻辑。不一致的逻辑当然会 allow you to prove anything 但也包括谎言。

忽略不一致性,类型系统通常对应于 intuitionistic logic constructivist ,这意味着某些经典逻辑无法直接表达。另一方面,这是有用的,因为如果一个类型是一个有效的构造性证明,那么这个类型的项就是一个有效的构造性证明 构造任何你已经证明存在的东西的方法 .

建构主义风格的一个主要特点是 双重否定 not P 变成 P -> Falsity . 因此,双重否定将是一个类型为 (P -> Falsity) -> Falsity ,这显然不等同于某种类型的东西 P

∀a. a 在某种意义上,几乎是假的。所以如果我们用多态性写双几乎否定呢?我们得到的类型如下所示: ∀a. (P -> a) -> a . 这等同于某种类型的东西吗 P 确实如此 ,仅将其应用于标识函数。

但重点是什么?为什么要写这样的字?是吗 有什么编程术语吗?好吧,你可以把它看作是一个已经有某种类型的函数 P 暂停计算 ,等待提供其余的。从这个意义上说,这些挂起的计算可以组合在一起,传递,调用,等等。对于某些语言的爱好者来说,这应该是很熟悉的,比如Scheme或Ruby,因为它的意思是 双重否定对应于 continuation-passing style 事实上,我上面给出的类型正是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

[2] 同样,这是完整性的结果。如果逻辑是一致的,这将是一个反定理的证明——因此,它不可能存在。

* , * -> * 等。;话语领域的要素类型。例如,在 Father(X,Y) :- Parent(X,Y), Male(X) , X 和 Y Dom ),和 Male :: Dom -> * .

function composition      | syllogism

我很喜欢这个问题。我知道的不多,但我确实有一些事情要做 the Wikipedia article ,它有一些整洁的桌子等):

1. 我认为和类型/并集类型( 例如 data Either a b = Left a | Right b )相当于 包容的 分离。而且,虽然我对库里·霍华德不是很熟悉,但我认为这证明了这一点。考虑以下功能:

   andImpliesOr :: (a,b) -> Either a b
   andImpliesOr (a,_) = Left a
   

   如果我理解正确的话,类型是这样的( § b )( 一 b )这个定义说,这是真的,其中要么是包容的,要么是排他性的,或者,无论哪个 Either 代表。你有 或者 代表排他或;但是( 一 § b 一 b 一 和 一 )( 一 ¨ ),因为如果两者都 一 和 如果是真的,那么至少有一个是真的。因此,如果歧视性结合是某种形式的分离,那么它们一定是包容的变体。我认为这可以作为一个证据,但我可以更自由地驳斥我的观点。

2. 类似地,你将重言式和荒谬性分别定义为同一函数和非终止函数,这有点不对劲。真正的公式由 单位类型 ,即只有一个元素的类型( data ⊤ = ⊤ ; 经常拼写 () Unit 在函数式编程语言中)。这是有道理的:因为这种类型是 有人居住,既然只有一个可能的居民,那一定是真的。恒等式函数只是表示 一 一 .

   Wikipedia ,处理不终止是一个问题,因为添加它会产生不一致的逻辑( 例如 wrong :: a -> b 通过 wrong x = wrong x ,从而证明 一 b 对于任何 和 b 由…定义的东西 data ⊥ 也就是说,一个没有任何方法来构造它的数据类型。这确保了它没有任何值,因此它必须是无居民的,这相当于false。我想你也可以 a -> b ,因为如果我们禁止非终止函数,那么这也是无人居住的,但我不是100%确定。

3. 说公理是以两种不同的方式编码的,这取决于你如何解释Curry-Howard:要么在组合词中,要么在变量中。我认为combinator的观点意味着我们得到的原始函数编码了我们默认可以说的东西(类似于modus ponens是一个公理的方式,因为函数应用程序是原始的)。我呢 变量视图实际上可能意味着相同的东西,毕竟,组合子只是全局变量,是特定的函数。至于基本类型:如果我想的没错,那么我认为基本类型就是我们试图证明的基本对象的实体。

4. 一 § b c 一 ( b )(还有 b ( c ))被称为出口等值法,至少在自然演绎证明中是这样。我当时没注意到那只是一种咖喱我希望我有,因为那很酷!

5. 我们现在有办法 包容的 析取,我们没有一种方法来表示排他性的变化。我们应该能够使用排他析取的定义来表示它: ( 一 ¨ b 一 § b ). 我不知道怎么写否定,但我知道 p p

   data ⊥
   data Xor a b = Xor (Either a b) ((a,b) -> ⊥)
   

   这定义了 ⊥ 是没有值的空类型,对应于falsity; Xor 然后定义为同时包含( 和 ) 一 b ( )和一个函数( 含义 )从 (甲、乙) ( 和 假 ). 然而,我不知道这是什么 . 编辑1: 现在我知道了,看下一段!) 因为没有类型的值 (a,b) -> ⊥ (有吗?),我无法理解这在程序中意味着什么。有人知道更好的方法来思考这个定义还是另一个定义吗? ( camccann .)

   感谢 camccann's answer (更具体地说,他在上面留下的帮助我的评论),我想我明白这里发生了什么。构造类型的值 Xor a b a 或 b Left a Right b 一 和 b (a,b) 作为第二个论点。因为你只能从 (a,b)—> 如果 (甲、乙) (甲、乙) 无法构建;换言之,至少有一个,而且可能两者都有 一 和 b (甲、乙) 也可以,所以一切都好。

很多这是我在思考/证明(希望)事情的时候,但我希望这是有用的。我真的很推荐你 ; 我没有读过任何细节,但它的表格是一个非常好的总结,它是非常彻底的。

这里有一个稍微晦涩的问题,我很惊讶它没有被提前提到:“经典的”函数式反应式编程对应于时态逻辑。

当然,除非你是哲学家、数学家或痴迷于函数编程,否则这可能会带来更多的问题。

那么,首先:什么是函数式反应式编程?这是一种声明式的工作方式 时变值 . 这对于编写用户界面之类的东西很有用,因为来自用户的输入是随时间变化的值。”经典的“FRP”有两种基本数据类型:事件和行为。

事件表示仅在离散时间存在的值。击键就是一个很好的例子:你可以把键盘的输入想象成一个给定时间的字符。然后,每个按键都只是一对,带有按键的字符和按键的时间。

行为是不断存在的价值观,但可以不断变化。鼠标位置就是一个很好的例子:它只是x,y坐标的一种行为。毕竟,老鼠 不断地 当你移动鼠标的时候。毕竟,移动鼠标是一个长期的动作,而不是一堆离散的步骤。

什么是时间逻辑?恰当地说,这是一套逻辑规则,用于处理随时间而量化的命题。本质上,它用两个量词扩展了正常的一阶逻辑:和。第一个意思是“始终”:读作“始终保持”。第二个是“最终”:意思是“最终会保持”。这是一种特殊的 modal logic . 以下两条定律与量词有关:

□φ ⇔ ¬◇¬φ
◇φ ⇔ ¬□¬φ

所以和是双重的,就像和一样。

每一个 可能的时间,而事件只发生一次。

关于连续体和双重否定的关系,call/cc的类型是皮尔士定律 http://en.wikipedia.org/wiki/Call-with-current-continuation

C-H通常表示为直觉逻辑与程序之间的对应关系。然而,如果我们添加带有当前延续(callCC)运算符的调用(其类型对应于皮尔士定律),我们得到 古典逻辑

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 (a,a) -&燃气轮机;无效,产品类型为 ((a,b)->Void,(a,b)->Void)->Void ,总和类型为 ((a,a)->Void,(b,b)->Void)->Void

如果我们再进一步挖掘,就会发现那块是 existential graph 相当于一种语言的唯一数据类型是n-延续,但我没有看到任何现有的语言是这种形式。所以发明一个可能会很有趣,我想。

虽然这不是简单的同构, this discussion of constructive LEM

头等舱续航支持允许您表达$P\lor\neg P$。 诀窍是基于这样一个事实:不调用continuation并用某个表达式退出就等于用同一个表达式调用continuation。

有关详细视图,请参见: http://www.cs.cmu.edu/~rwh/courses/logic/www-old/handouts/callcc.pdf