Kripke-Semantik

{-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs, TypeOperators,
    TypeFamilies,  UndecidableInstances, StandaloneDeriving #-}

import Data.Void


-- https://en.wikipedia.org/wiki/Kripke_semantics


-- Kripkes Welten sind nur eine Menge, ohne weitere Struktur
class World w
data W_Hask
data W_IO
data W_ahrheit
instance World W_Hask
instance World W_IO
instance World W_ahrheit
-- Anmerkung: Die Klasse World kann man auch weg lassen
-- wenn man will, kann man Welt-Datentypen auch durch so was wie
-- data World a
-- kennzeichnen

-- Weltrahmen, Liste aller Elemente der Weltrelation
data Frame w v where
    IO_R_Hask :: Frame W_IO W_Hask
    W_R_W :: World w => Frame w w

deriving instance Show (Frame w v)

-- Eigenschaften des Weltrahmens
type Reflexive frame = forall w. World w => frame w w
type Symmetric frame = forall w v. frame w v -> frame v w
type Transitive frame = forall w v z. frame w v -> frame v z -> frame w z
type Euclidean frame = forall w v z. frame w v -> frame w z -> frame v z

-- In unserem Beispiel
reflexive_Frame :: Reflexive Frame
reflexive_Frame = W_R_W

transitive_Frame :: Transitive Frame
transitive_Frame W_R_W wRv = wRv
transitive_Frame vRw W_R_W = vRw


-- Symbole Pos, Nec, Verneinung und Folgerung
data Pos a
data Nec a
data Not a
infixr 1 :->
data a :-> b

-- Die Axiome des Kripke-Modells als (geschlossene) type family
-- Dies erlaubt pattern matching auf Typebene
type family KripkeModel it w form  where
    KripkeModel it w (Not a) = KripkeModel it w a -> Void
    KripkeModel it w (a :-> b) = KripkeModel it w a -> KripkeModel it w b
    KripkeModel it w (Pos a) = PosTransform it w a
    KripkeModel it w (Nec a) = NecTransform it w a
    KripkeModel it w a = Interpretation it w a


type family Interpretation it world a
data I_Bsp
type instance Interpretation I_Bsp  W_IO   a = IO a
type instance Interpretation I_Bsp  W_Hask a = a

-- Die Transformierten sind als Wrapper zu sehen
newtype NecTransform it w a = Nec {
    nectransfrom :: forall v. Frame w v -> KripkeModel it v a }
data PosTransform it w a where
    Pos :: Frame w v -> KripkeModel it v a -> PosTransform it w a


-- Die modallogischen Schlußregeln als Typen
type Extract w = forall it a. KripkeModel it w (Nec a :-> a)
type Pure w    = forall it a. KripkeModel it w (a :-> Pos a)
type Duplicate = forall it w a. KripkeModel it w (Nec a :-> Nec (Nec a))
type Join      = forall it w a. KripkeModel it w (Pos (Pos a) :-> Pos a)
type Brouwer   = forall it w a. KripkeModel it w (a :-> Nec (Pos a))
type S5        = forall it w a. KripkeModel it w (Pos a :-> Nec (Pos a))

-- Nun zu den Äquivalenzen Schlußregel <=> Weltrahmenbedingung

-- Hilfsdefinitionen

-- Spezial-Variable () wird bei Spezialinterpretation I_CheckFrame w
-- in der Welt v interpretiert als: wRv
data I_CheckFrame w
type instance Interpretation (I_CheckFrame w) v () = Frame w v

-- Variable () wird bei Spezialinterpretation I_ConcludeFrame w z
-- in der Welt v interpretiert als: wRv bedingt wRz
data I_ConcludeFrame w z
type instance Interpretation (I_ConcludeFrame w z) v () = Frame w v -> Frame w z
-- conclusive_apply :: wRv , (wRv -> wRz) => wRz
-- ist modus ponens angewandt auf Pos
conclusive_apply :: PosTransform (I_ConcludeFrame w z) w () -> Frame w z
conclusive_apply (Pos wRv h) = h wRv


-- Hier die eigentlichen Äquivalenzen:

-- Pure ist äquivalent zu Reflexive Frame
reflexive_is_pure :: (World w) => Reflexive Frame -> Pure w
reflexive_is_pure = Pos

-- pure_is_reflexive :: (World w) => (Pure w) -> Reflexive Frame
-- Die Typsignatur müssen wir weglassen
pure_is_reflexive (axiom :: Pure w) = let
    p = axiom id
    in conclusive_apply p



-- Extract ist äquivalent zu Reflexive Frame
reflexive_is_extract :: (World w) => Reflexive Frame -> Extract w
reflexive_is_extract wrw (Nec necif) = necif wrw

--extract_is_reflexive' :: (World w) => Extract w -> Reflexive Frame
extract_is_reflexive (axiom :: Extract w) = let
    nt = Nec id :: NecTransform (I_CheckFrame w) w ()
    in axiom nt



transitive_is_duplicate :: Transitive Frame -> Duplicate
transitive_is_duplicate trans (Nec f_to_m) =
    Nec (\rel1 -> Nec (\rel2 -> f_to_m (trans rel1 rel2)))

duplicate_is_transitive :: Duplicate -> Transitive Frame
duplicate_is_transitive (duplicator :: Duplicate) = let
    nt = Nec id  :: forall w. NecTransform (I_CheckFrame w) w ()
    Nec f1 = duplicator nt
    in \rel1 -> let
        Nec f2 = f1 rel1
        in f2



transitive_is_join :: Transitive Frame -> Join
transitive_is_join trans (Pos wRv (Pos vRz a)) = Pos (trans wRv vRz) a

join_is_transitive :: Join -> Transitive Frame
join_is_transitive joinator (wRv :: Frame w v) (vRz :: Frame v z) = let
    p2 = joinator (Pos wRv (Pos vRz id))
    in conclusive_apply p2



symmetric_is_brouwer :: Symmetric Frame -> Brouwer
symmetric_is_brouwer sym form = let
    assertPos :: KripkeModel it w a -> Frame w v -> PosTransform it v a
    assertPos form wRv = Pos (sym wRv) form
    in Nec (assertPos form)

brouwer_is_symmetric :: Brouwer -> Symmetric Frame
brouwer_is_symmetric brouwerei wRv = let
    Nec f = brouwerei id
    in conclusive_apply (f wRv)



euclidean_is_s5 :: Euclidean Frame -> S5
euclidean_is_s5 euclid = let
    assertPos :: Frame w v -> KripkeModel it v a -> Frame w z -> PosTransform it z a
    assertPos wRv form wRz = Pos (euclid wRz wRv) form
    in \(Pos wRv form) -> Nec (assertPos wRv form)

s5_is_euclidean :: S5 -> Euclidean Frame
s5_is_euclidean s5 wRv wRz = let
    Nec f = s5 (Pos wRz id)
    in conclusive_apply (f wRv)