haskell-jp / beginners #20 at 2022-03-07 23:28:40 +0900

数学、論理学寄りの質問なのですが、今私はHaskellでproof checkをしてみたくて、Haskellの型で論理結合子を表現しようとしているのですが、全称量化子と存在量化子の表現方法がわからずに詰まっています。
”BHK解釈”のwikiで以下の画像のような記述を発見したのですが、xが証明ではなく、集合Sの要素であることを表現するにはどのようにすればよいか、教えていただきたいです。

import Data.Void (Void)

type Imply a b = a -> b
type And a b = (a, b)
type Or a b = Either a b
type False = Void
type Not a = a -> False

type Forall x a = x -> a -- xは個体変項 aは論理式
type Exists x a = (x, a)

各型 (And a bにおけるa,bなど) の値には何が格納されることを想定してますか？

証明を表すデータが格納されるということならば、データSの値をx∈Sの証明とみなして、`S -> A` 型の値として証明が書けると思います (∀x∈S.P(x)とは∀x.((x∈S)→P(x))のことなので)。

@yFkhr
すみません、ご指摘を踏まえて自分でいろいろ試してみたのですが、具体的に型を構成する方法がわかりませんでした。
参考として、のp22によると、AgdaではForallとExistsを以下のようにかけるようです。

data Forall (A : Set) (B : A -> Set) : Set where
  dfun : ((a : A) -> B a) -> Forall A B

data Exists (A : Set) (B : A -> Set) : Set where
  [_,_] : (a : A) -> B a -> Exists A B

これと等価な式はHaskellでも構成可能なのでしょうか？
PolyKinds拡張を有効にすると、それっぽくはかけるのですが、

type Forall (x :: s) a = s -> a x
type Exists (x :: s) a = (s, a x)

ForallとExistsがとる第一引数は集合であるsではなく、その要素であるxになってしまいます。（上のAgdaの例ではForallとExistsは、集合であるAと命題の述語記号Bを引数にとっている）

一応、例として、命題論理では以下のように証明しています。（長くてすみません）
・シンボルの定義

class Prop a

type Imply a b = a -> b
instance Prop (a -> b)

type And a b = (a, b)
instance Prop (a, b)

type Or a b = Either a b
instance Prop (Either a b)

-- 略記法と結合の強さの定義
type p /\ q = p `And` q
type p \/ q = p `Or` q　
type p --> q = p `Imply` q
infixl 3 /\
infixl 2 \/
infixr 1 -->

・（自然演繹の）推論規則と命題：(A\/C)->(B\/C)->~(A\/B)の証明

introAnd :: (Prop a, Prop b) => a -> b -> And a b
introAnd a b = (a, b)

contradict :: Prop a => a -> Not a -> False
contradict a na = na a

absurd :: Prop a => False -> a
absurd f = case f of

lemma :: (Prop a, Prop b, Prop c) => (a \/ c) --> (b \/ c) --> Not (a /\ b) --> c
lemma ac bc nab = case ac of
    Left a -> case bc of
        Left b -> absurd (contradict (introAnd a b) nab)
        Right c -> c
    Right c -> c

少し複雑なので分かりづらいかもしれませんが、このような感じで、述語論理に関しても、全称量化子と存在量化子を型で定義して、推論規則の組み合わせで命題を証明したいと考えています。

ちょっと無理がある気がしますね……。型が命題、その型を持つ項・プログラムが証明に対応するので、for all/ existsを表現しようとすれば項をパラメータに取る型が必要(dependent type theory)ですが、haskellのdependent type theoryのサポートってdatakindsくらいでかなり弱いので…

@gksato
なるほど。「依存型」と述語論理はそういう風に関連してくるのですか。少し理解が進みました。ありがとうございます。とりあえずHaskellでやるのは断念します。
ちなみに、一番近いのは

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}

type Forall s (a :: s -> *) = forall (x :: s). x -> a x
type Exists s (a :: s -> *) = forall (x :: s). (x, a x)

だったのですが、

Expected a type, but 'x' has kind 's'
• In the type 'forall (x :: s). x -> a x'
  In the type declaration for 'Forall'
  NB: Type 'Forall' was inferred to use visible dependent quantification.
Most types with visible dependent quantification are
  polymorphically recursive and need a standalone kind
  signature. Perhaps supply one, with StandaloneKindSignatures.

というエラーが出て駄目でした。エラーにならって、StandaloneKindSignatures拡張を入れましたが効きませんでした。

@ksrk

Perhaps supply one

とあるように、“one” つまり “a standalone kind signature”(スタンドアロンの種注釈) を与えてよるのがいいかもしれない、そのためには StandAloneKindSignatures 拡張が要るよ、という話な訳ですね．for all の定義として適切なように standalone kind signature をつけるなら

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}

type Forall :: forall k -> (k -> *) -> *
type Forall k (f :: k -> *) = forall (x :: k). f x

のような形になるでしょうか． existsをtype synonym で やりきるのは難しい気がします．data typeを使うなら：

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE ExistentialQuantification #-}

newtype Forall k (f :: k -> *) = ForallIntro (forall (x :: k). f x)
data Exists k (f :: k -> *) = forall (x :: k). ExistsIntro (f x)

のような形になるでしょうか．ただ，この場合のどちらにしても， k は型ではなく種であり，種として見做せるHaskellの型はあまり多くない，というのが(命題の表現力の意味で)ネックにはなってきますね…．