types - 如何用下一个类型实现 OCaml 功能？

Question

我正在研究库里-霍华德函授。

给定命题逻辑陈述：¬(p ∨ q) -> (¬p ∧ ¬q).

我需要在 OCaml 中定义一个类型（作为命题）和一个函数（作为证明）。

我已经定义了类型但不知道如何实现功能：

type empty = | 
type ('a , 'b) coprod = Left of 'a | Right of 'b
let ex513: (('p, 'q) coprod -> empty) -> ('p -> empty) * ('q -> empty) = fun ?

在发布问题之前我做了什么：

我已经验证了这个陈述在直觉逻辑中是可以证明的。
试图建设性地理解：如果存在function1将 p 的证明或 q 的证明转换为⊥，那么我们可以构造元组（function2将 p 的证明转换为⊥，function3将 q 的证明转换为⊥）。执行(function1(p), function1(q))
实施了类似的任务以更好地理解问题：p ∨ q -> ¬(¬p ∧ ¬q).

代码：

let func1: ('p, 'q) coprod -> ('p-> empty) * ('q-> empty) -> empty = fun x (f, g)->
    match x with 
    | Left x -> f(x)
    | Right x -> g(x)

score 2 · Accepted Answer

定义

type 'a not = 'a -> empty

为了简洁起见，写一个函数确实是个好主意

let left_branch: type p q. (p,q) coprod not -> p not = ...

和

let right_branch: type p q. (p,q) coprod not -> q not = ...

一旦定义了这两个函数（换句话说，证明了相应的引理），就可以通过应用两个引理来获得解决方案：

let de_morgan_law: type p q. (p,q) coprod not -> p not * q not =
  fun not_p_or_q -> left_branch not_p_or_q, right_branch not_p_or_q

如果您在编写（或正确的函数）时遇到问题left_branch，请记住

let left x = Left x

有类型'a -> ('a,'any) coprod。

1 回答 1