2

我在 Haskell 中实施了四个德摩根定律中的三个：

notAandNotB :: (a -> c, b -> c) -> Either a b -> c
notAandNotB (f, g) (Left x)  = f x
notAandNotB (f, g) (Right y) = g y

notAorB :: (Either a b -> c) -> (a -> c, b -> c)
notAorB f = (f . Left, f . Right)

notAorNotB :: Either (a -> c) (b -> c) -> (a, b) -> c
notAorNotB (Left f)  (x, y) = f x
notAorNotB (Right g) (x, y) = g y

但是，我认为不可能实施最后一条法律（有两个居民）：

notAandBLeft  :: ((a, b) -> c) -> Either (a -> c) (b -> c)
notAandBLeft  f = Left  (\a -> f (a, ?))

notAandBRight :: ((a, b) -> c) -> Either (a -> c) (b -> c)
notAandBRight f = Right (\b -> f (?, b))

在我看来，有两种可能的解决方案：

  1. undefined代替?. _ 这不是一个好的解决方案，因为它是作弊。

  2. 使用单态类型或有界多态类型来编码默认值。

    notAandBLeft  :: Monoid b => ((a, b) -> c) -> Either (a -> c) (b -> c)
notAandBLeft  f = Left  (\a -> f (a, mempty))

notAandBRight :: Monoid a => ((a, b) -> c) -> Either (a -> c) (b -> c)
notAandBRight f = Right (\b -> f (mempty, b))

    这不是一个好的解决方案，因为它比德摩根定律更弱。

我们知道德摩根定律是正确的，但我假设最后一条定律不能用 Haskell 编码是否正确？这对 Curry-Howard 同构有什么看法？如果每个证明都不能转换成等效的计算机程序，那它就不是真正的同构，对吧？

4

2 回答 2

6

第四定律不是直觉的。你需要排中公理：

lem :: Either a (a -> c)

或皮尔斯定律：

pierce :: ((a -> c) -> c) -> a

来证明它。

于 2016-05-04T03:21:51.737 回答
5

对我来说突出的一件事是，您似乎没有在任何地方使用否定的定义或任何属性。

在阅读了关于 CHI 的 Haskell Wikibooks 文章后，这里有一个证明，假设您有一个排中定律作为定理：

exc_middle :: Either a (a -> Void)

notAandB德摩根定律的证明如下：

notAandB' :: Either a (a -> Void) -> ((a,b) -> Void) -> Either (a -> Void) (b -> Void)
notAandB' (Right notA) _ = Left notA
notAandB' (Left a)     f = Right (\b -> f (a,b))

notAandB = notAandB' exc_middle
于 2016-05-04T03:21:40.613 回答