问题标签 [curry-howard]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
43 问题
0
投票
2
回答
152
浏览
types - 使用 Curry-Howard 对应来证明下一个命题逻辑陈述的正确方法是什么？
我正在研究库里-霍华德函授。
给定命题逻辑陈述：(¬p -> q) -> ((¬p -> ¬q) -> p).
我需要在 OCaml 中定义一个类型（作为命题）和一个函数（作为证明）。
我想出了下一个代码并卡住了：
错误：
0
投票
1
回答
47
浏览
types - 如何用下一个类型实现 OCaml 功能？
我正在研究库里-霍华德函授。
给定命题逻辑陈述：¬(p ∨ q) -> (¬p ∧ ¬q).
我需要在 OCaml 中定义一个类型（作为命题）和一个函数（作为证明）。
我已经定义了类型但不知道如何实现功能：
在发布问题之前我做了什么：
- 我已经验证了这个陈述在直觉逻辑中是可以证明的。
- 试图建设性地理解：如果存在
function1将 p 的证明或 q 的证明转换为⊥，那么我们可以构造元组（function2将 p 的证明转换为⊥，function3将 q 的证明转换为⊥）。执行(function1(p), function1(q)) - 实施了类似的任务以更好地理解问题：
p ∨ q -> ¬(¬p ∧ ¬q).
代码：
0
投票
1
回答
33
浏览
category-theory - 为什么 sum-type 在 Curry-Howard 对应关系中是析取的？
根据Curry-Howard 对应，sum-type aka tagged-union 相当于析取，逻辑 OR
为什么会这样？不是更接近异或吗？(a or b)意味着它可以是aorb或both，而Either a b必须是aorb但绝不是两者。