2

Haskell で 4 つの De Morgan の法則のうち 3 つを実装しました。

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

ただし、最後の法律 (住民が 2 人いる) を実装することは可能ではないと思います。

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))

私の見方では、2つの可能な解決策があります。

  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))

    これはド・モルガンの法則よりも弱い法則であるため、良い解ではありません。

De Morgan の法則が正しいことはわかっていますが、最後の法則は Haskell でエンコードできないと仮定するのは正しいですか? これはカリー・ハワード同型について何を言っているのですか? すべての証明を同等のコンピューター プログラムに変換できない場合、それは実際には同型ではありませんよね?

4

2 に答える 2

6

第 4 法則は直観的ではありません。除外された中間の公理が必要になります。

lem :: Either a (a -> c)

またはピアスの法則:

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

それを証明するために。

于 2016-05-04T03:21:51.737 に答える
5

私が際立っていることの 1 つは、否定の定義やプロパティをどこでも使用していないように見えることです。

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 に答える