gpt4 book ai didi

haskell - 通过库里-霍华德通信了解 haskell 的德摩根定律

转载 作者:行者123 更新时间:2023-12-02 10:00:03 25 4
gpt4 key购买 nike

我在 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. 使用未定义代替。这不是一个好的解决方案,因为它是作弊行为。
  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 编码是否正确?这对库里-霍华德同构有何说明?如果每个证明都不能转换成等价的计算机程序,那么它就不是真正的同构,对吧?

最佳答案

第四定律是not intuitionistic 。您需要排除中间公理:

lem :: Either a (a -> c)

或 PIL 斯定律:

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

证明这一点。

关于haskell - 通过库里-霍华德通信了解 haskell 的德摩根定律,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/37016673/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com