如何用下一个类型实现 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 ?

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

1. I have verified 这个陈述在直觉逻辑中是可以证明的。
2. 试图建设性地理解：如果有function1将p的证明或q的证明转换为⊥，那么我们可以构造元组（function2将p的证明转换为⊥，function3将q的证明转换为到⊥）。执行(function1(p), function1(q))
3. 实施了类似的任务以更好地理解问题：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)

Answer 1

定义

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。