1 -----------------------------------------------------------------------------
    2 -- |
    3 -- Module      :  Translation
    4 -- Copyright   :  (c) Masahiro Sakai 2007-2009
    5 -- License     :  BSD3-style (see LICENSE)
    6 -- 
    7 -- Maintainer:    masahiro.sakai@gmail.com
    8 -- Stability   :  experimental
    9 -- Portability :  non-portable
   10 
   11 {-# LANGUAGE TypeOperators, GADTs, TypeSynonymInstances, ScopedTypeVariables #-}
   12 
   13 module Translation (translate, catToType) where
   14 
   15 import IL
   16 import P
   17 
   18 -----------------------------------------------------------------------------
   19 
   20 {-
   21 -- 範疇から型への対応
   22 type family Translate x
   23 type instance Translate Sen = Prop
   24 type instance Translate IV = E -> Prop
   25 type instance Translate CN = E -> Prop
   26 type instance Translate Adj = E -> Prop
   27 type instance Translate (a :/ b) = ((S -> Translate b) -> Translate a)
   28 type instance Translate (a :// b) = ((S -> Translate b) -> Translate a)
   29 -}
   30 
   31 catToType :: Cat c ->  Type
   32 catToType Sen = Prop
   33 catToType IV = E :-> Prop
   34 catToType CN = E :-> Prop
   35 catToType Adj = E :-> Prop -- これで本当にあっている?
   36 catToType (a :/ b) = (S (catToType b)) :-> catToType a
   37 catToType (a :// b) = (S (catToType b)) :-> catToType a
   38 
   39 -----------------------------------------------------------------------------
   40 
   41 translate :: forall c. P c -> Expr
   42 --- 1. αがgの定義域にあれば，α は，g(α) に翻訳される．
   43 -- 最後に
   44 --- 2. be → λp.λx. p{f^λy.[x = y]}.
   45 ---    ここで，変数pのタイプは<s, <<s, <e, t>>, t>>.
   46 translate (B (IV :/ (Sen :/ IV)){- TV -} "be") =
   47   lambda p $ lambda x $ 
   48     FVar p <@> int (lambda y $ Op2 Id (FVar x) (FVar y))
   49   where
   50     p = ("p", S (S (E :-> Prop) :-> Prop))
   51     x = ("x", E)
   52     y = ("y", E)
   53 --- 3. necessarily → λp[□ext p]. ここで，p のタイプは<s, t>とする．
   54 translate (B (Sen :/ Sen) "necessarily") = lambda p $ Op1 Box (ext (FVar p))
   55   where
   56     p = ("p", S Prop)
   57 --- 4. j, m, b はタイプがe の定数記号，変数P のタイプは<s, <e, t>>とする．
   58 translate (B (Sen :/ IV){- T -} x) = lambda p $ FVar p <@> Const (x, E)
   59   where
   60     p = ("p", S (catToType IV))
   61 --- 5. he_n → λP. P {x_n}．x_ はタイプe の変数．
   62 translate (He n) = lambda p $ FVar p <@> FVar (xn n)
   63   where
   64     p = ("p", S (E :-> Prop))
   65 translate (F2 delta zeta) = trApp delta zeta -- T2
   66 translate (F3 n zeta phi) = -- T3
   67     lambda (xn n) $ Op2 And (translate zeta :@ FVar (xn n)) (translate phi)
   68 translate (F4 alpha delta) = trApp alpha delta -- T4
   69 translate (F5 delta beta)  = trApp delta beta  -- T5
   70 -- T6 (T5と同じなので省略)
   71 translate (F16 delta phi)  = trApp delta phi   -- T7
   72 translate (F17 delta beta) = trApp' delta beta -- T8
   73 translate (F6 delta beta)  = trApp delta beta  -- T9
   74 translate (F7 delta beta)  = trApp delta beta  -- T10
   75 translate (F8 phi psi) =
   76   case cat :: Cat c of
   77     Sen -> Op2 And (translate phi) (translate psi) -- T11a
   78     IV -> lambda x $ Op2 And (translate phi :@ FVar x) (translate psi :@ FVar x) -- T12a
   79   where
   80     x = ("x", E)
   81 translate (F9 phi psi) =
   82   case cat :: Cat c of
   83     Sen -> Op2 Or (translate phi) (translate psi) -- T11b
   84     IV -> lambda x $ Op2 Or (translate phi :@ FVar x) (translate psi :@ FVar x) -- T12b
   85       where x = ("x", E)
   86     Sen :/ IV -> lambda p $ Op2 Or (translate phi :@ FVar p) (translate psi :@ FVar p) -- T13
   87       where p = ("P", S (E :-> Prop))
   88 -- T14 (講義資料はx_nになるべきところがxになっている)
   89 translate (F10 n alpha phi) =
   90   case cat :: Cat c of
   91     Sen -> translate alpha :@ (int $ lambda (xn n) (translate phi)) -- T14
   92     CN -> lambda y $ translate alpha :@ int (lambda (xn n) (translate phi :@ FVar y)) -- T15
   93     IV -> lambda y $ translate alpha :@ int (lambda (xn n) (translate phi :@ FVar y)) -- T16
   94   where
   95     y = ("y", E)
   96 -- T17
   97 translate (F11 alpha delta) = Op1 Not         $ trApp alpha delta
   98 translate (F12 alpha delta) =           Op1 F $ trApp alpha delta
   99 translate (F13 alpha delta) = Op1 Not $ Op1 F $ trApp alpha delta
  100 translate (F14 alpha delta) =           Op1 H $ trApp alpha delta
  101 translate (F15 alpha delta) = Op1 Not $ Op1 H $ trApp alpha delta
  102 -- T18 (beの扱い以外はT9と同じ)
  103 translate (B (IV :/ Adj) "be") = lambda p $ lambda x $ FVar p <@> FVar x
  104   where
  105     p = ("P", S (E :-> Prop))
  106     x = ("x", E)
  107 -- T19
  108 translate (F19 delta) =
  109   lambda x $ exists y $
  110     translate delta :@ int (lambda p (FVar p <@> FVar y)) :@ FVar x
  111   where
  112     x = ("x", E)
  113     p = ("P", S (E :-> Prop))
  114     y = ("y", E)
  115 translate (F20 delta beta) = trApp delta beta -- T20
  116 translate (F21 delta beta) = trApp delta beta -- T21 (講義資料ではF20を誤って使っている)
  117 -- T22
  118 translate (F22 delta) =
  119   lambda p $ lambda q $ lambda x $
  120     translate delta :@ FVar q :@ FVar p :@ FVar x
  121   where
  122     p = ("P", S (catToType (cat :: Cat T)))
  123     q = ("Q", S (catToType (cat :: Cat T)))
  124     x = ("x", E)
  125 translate (F23 alpha delta) = trApp alpha delta -- T23
  126 translate (F24 alpha beta)  = trApp alpha beta  -- T24
  127 -- 講義資料のByの解釈は誤り? (型が一致しない)
  128 translate (B (IV :/ (IV :/ (Sen :/ IV)) :/ (Sen :/ IV)){- PP/T -} "by") = 
  129   lambda p $ lambda r $ lambda x $
  130     FVar p <@>
  131       (int $ lambda y $ FVar r <@> int (lambda q $ FVar q <@> FVar x) :@ FVar y)
  132   where
  133     p = ("P", S (catToType (Sen :/ IV)))
  134     r = ("R", S (catToType (IV :/ (Sen :/ IV))))
  135     x = ("x", E)
  136     y = ("y", E)
  137     q = ("Q", S (catToType IV))
  138 -- T25
  139 translate (F25 delta) =
  140   lambda x $ exists y $ Op1 H $
  141     translate delta :@
  142       int (lambda p $ FVar p <@> FVar x) :@
  143       (FVar y)
  144   where
  145     x = ("x", E)
  146     y = ("y", E)
  147     p = ("P", S (catToType IV))
  148 
  149 -- Det
  150 translate (B (Sen :/ IV :/ CN) s) =
  151   case s of
  152     "a"   ->
  153       lambda p $ lambda q $ exists x $
  154         Op2 And (FVar p <@> FVar x) (FVar q <@> FVar x)
  155     "the" ->
  156       lambda p $ lambda q $ exists y $ 
  157         Op2 And
  158           (forall x $ Op2 Equiv (FVar p <@> FVar x) (Op2 Id (FVar x) (FVar y)))
  159           (FVar q <@> FVar y)
  160     "every" ->
  161       lambda p $ lambda q $ forall x $
  162         Op2 Imply (FVar p <@> FVar x) (FVar q <@> FVar x)
  163     "no" ->
  164       lambda p $ lambda q $ forall x $
  165         Op1 Not (Op2 And (FVar p <@> FVar x) (FVar q <@> FVar x))
  166     _ -> Const (s, catToType (cat :: Cat Det))
  167   where
  168     p = ("p", S (E :-> Prop))
  169     q = ("q", S (E :-> Prop))
  170     x = ("x", E)
  171     y = ("y", E)
  172 
  173 -- それ以外
  174 translate (B c x) = Const (x, catToType c)
  175 
  176 -- ユーティリティ
  177 trApp :: P (b :/ a) -> P a -> Expr
  178 trApp  f a = translate f :@ (int (translate a))
  179 trApp' :: P (b :// a) -> P a -> Expr
  180 trApp' f a = translate f :@ (int (translate a))
  181 
  182 xn :: Int -> Name
  183 xn n = ("he_"++show n, E)
  184