importing from PTQ 0.0.5

msakai · Dec 19, 2010 · 94e38fb · 94e38fb
commit 94e38fb
Show file tree

Hide file tree

Showing 24 changed files with 2,977 additions and 0 deletions.
diff --git a/COPYING b/COPYING
diff --git a/PTQ.cabal b/PTQ.cabal
@@ -0,0 +1,71 @@
+Name:            PTQ
+Version:         0.0.5
+License:         LGPL
+License-File:    COPYING
+Author:          Masahiro Sakai
+Maintainer:      Masahiro Sakai <masahiro.sakai AT gmail.com>
+Homepage:        http://www.tom.sfc.keio.ac.jp/~sakai/hiki/?hsPTQ
+Category:        Natural Language Processing
+Build-Type:      Simple
+Synopsis:        An implementation of Montague's PTQ.
+Description:     An implementation of Montague's PTQ (Proper Treatment of Quantification). It translates simple plain English sentences into formulas of intentional logic.
+Cabal-Version:   >= 1.2.3
+Stability:       experimental
+Extra-Source-Files:
+   README, COPYING
+   src/Context.hs, src/MP.hs, src/PDict.hs, src/ParserTest.hs,
+   misc/Test.hs, misc/Test2.agda, misc/Test3.hs
+Data-Files: cgi/index.html, cgi/main.html
+
+Flag UTF8Terminal
+  Description: Use UTF-8 for terminal I/O
+  Default: False
+
+Flag UTF8CGI
+  Description: Use UTF-8 for HTTP contents
+  Default: True
+
+Executable ptq
+  Main-Is: Main.hs
+  Hs-Source-Dirs: src
+  Other-Modules:
+     IL
+     P
+     Translation
+     Parser
+     Report
+     Version
+  Extensions:
+     EmptyDataDecls
+     GADTs
+     MultiParamTypeClasses
+     TypeOperators
+     TypeSynonymInstances
+  Build-Depends: base >=4 && <5, haskell98, mtl, containers
+  if flag(UTF8Terminal)
+    CPP-Options: "-DUSE_UTF8"
+    Build-Depends: utf8-string
+
+Executable ptq.cgi
+  Main-Is: CGIMain.hs
+  Hs-Source-Dirs: src
+  Other-Modules:
+     IL
+     P
+     Translation
+     Parser
+     Version
+     ReportHTML
+     CGI
+     URLEncoding
+  Extensions:
+     EmptyDataDecls
+     GADTs
+     MultiParamTypeClasses
+     TypeOperators
+     TypeSynonymInstances
+     CPP
+  Build-Depends: base >=4 && <5, haskell98, mtl, containers, network, xml
+  if flag(UTF8CGI)
+    CPP-Options: "-DUSE_UTF8"
+    Build-Depends: utf8-string
diff --git a/README b/README
@@ -0,0 +1,41 @@
+= An implementation of Montague's PTQ in Haskell
+
+== Build and Install
+
+You'll need GHC 6.7 or later.
+
+  % runhaskell Setup.lhs configure
+  % runhaskell Setup.lhs build
+  % runhaskell Setup.lhs install
+
+== Usage of interactive shell ptq
+
+  % ptq
+  PTQ> John seeks a unicorn.
+  Parsed:
+    F4 john (F5 seek (F2 a unicorn))
+
+  Translation:
+    (\x0. x0 {john}) (Int (seek (Int ((\x0. \x1. exists x2. x0 {x2} && x1 {x2}) (Int unicorn)))))
+
+  Translation (simplified):
+    seek (Int (\x0. exists x1. unicorn x1 && x0 {x1})) john
+
+  ------------------------------------------------------
+
+  Parsed:
+    F10 0 (F2 a unicorn) (F4 john (F5 seek (He 0)))
+
+  Translation:
+    (\x0. \x1. exists x2. x0 {x2} && x1 {x2}) (Int unicorn) (Int (\x0. (\x1. x1 {john}) (Int (seek (Int (\x1. x1 {x0}))))))
+
+  Translation (simplified):
+    exists x0. unicorn x0 && seek (Int (\x1. x1 {x0})) john
+  PTQ> quit
+  %
+
+== CGI interface
+
+By locating ptq.cgi, cgi/index.html and cgi/main.html to the place
+where CGI is executable, you can try it on the web.
+Demo site runs at <http://www.tom.sfc.keio.ac.jp/~sakai/hsPTQ/>.
diff --git a/Setup.lhs b/Setup.lhs
@@ -0,0 +1,4 @@
+#! /usr/bin/env runhaskell
+
+> import Distribution.Simple
+> main = defaultMain
diff --git a/cgi/index.html b/cgi/index.html
@@ -0,0 +1,14 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Frameset//EN">
+<html>
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
+<title>Demo page of PTQ</title>
+</head>
+<frameset rows="30%,*">
+<frame src="main.html">
+<frame name="result">
+<noframes>
+<a href="main.html">No frame version</a>
+</noframes>
+</frameset>
+</html>
diff --git a/cgi/main.html b/cgi/main.html
@@ -0,0 +1,49 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+<html>
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
+<title>Demo page of PTQ</title>
+</head>
+
+<body>
+<h1>Demo page of <a href="http://www.tom.sfc.keio.ac.jp/~sakai/hiki/?hsPTQ" target="_top">PTQ</a></h1>
+
+<p>
+<form method="get" action="ptq.cgi" accept-charset="utf-8 us-ascii" target="result">
+<input type="text" name="s" value="" size="100" />
+<input type="submit" value="Translate!" />
+</form>
+</p>
+
+<p>
+<form method="get" action="ptq.cgi" accept-charset="utf-8 us-ascii" target="result">
+Sample: <select name="s">
+<option>John seeks a unicorn.</option>
+<option>John finds a unicorn.</option>
+<option>Necessarily John walks.</option>
+<option>John is Bill.</option>
+<option>John is a unicorn.</option>
+<option>John believes that a unicorn talks.</option>
+<option>Every woman loves a unicorn.</option>
+<option>Every woman loves John.</option>
+<option>A unicorn walks and it talks.</option>
+<option>Every unicorn such that it walks talks.</option>
+<option>John walks slowly.</option>
+<option>John walks in a park.</option>
+<option>John wishes to find a unicorn and eat it.</optoin>
+<option>A man or a woman is asleep.</option>
+<option>A man is asleep or a woman is asleep.</option>
+<option>A man or a woman loves every unicorn.</option>
+<option>A man loves every unicorn or a woman loves every unicorn.</option>
+<option>Every unicorn walks or talks.</option>
+<!-- ここまでは講義資料に載っていたもの -->
+<option>John has sought a unicorn.</option>
+<option>John will seek a unicorn.</option>
+<option>A unicorn is eaten by John.</option>
+<option>Every unicorn is not a man.</option>
+<option>Every man loves a woman such that she loves him.</option>
+</select> <input type="submit" value="Translate!" />
+</form>
+</p>
+
+</body> </html>
diff --git a/misc/Test.hs b/misc/Test.hs
@@ -0,0 +1,50 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
+
+{-# OPTIONS_GHC -fallow-undecidable-instances #-}
+-- coverage condition を満たしていないインスタンス宣言があるため
+
+-----------------------------------------------------------------------------
+-- Expr.hs 
+
+-- Benetteの意味タイプ
+data E       -- 個体
+data Prop    -- 本来はtと書かれるけど、小文字が使えないので
+data S a
+-- 関数型はHaskellの -> をそのまま使う
+
+infixl 9 :@
+
+-- 意味タイプがtである式
+data Expr t where
+    FVar :: Name -> Expr t
+    BVar :: !Int -> Expr t
+    Lam  :: Name -> Scope b -> Expr (a -> b)
+    Forall :: Name -> Scope Prop -> Expr Prop
+    Exists :: Name -> Scope Prop -> Expr Prop
+    (:@) :: Expr (a -> b) -> Expr a -> Expr b
+    C :: C t -> Expr t
+
+type Name = String
+newtype Scope t = Sc (Expr t)
+
+data C t where
+    John' :: C E
+    Mary' :: C E
+    Bill' :: C E
+    Int   :: C (a -> S a)
+
+abstract :: Name -> Expr t -> Scope t
+abstract name expr = Sc (h 0 expr)
+  where
+    h outer (FVar name') | name==name' = BVar 0
+			 | otherwise   = FVar name'
+    h outer (BVar index) = BVar index
+
+-- instantiate :: Expr u -> Scope t -> Expr t
+
+-----------------------------------------------------------------------------
+
+-- import Expr.hs
+
+
+-----------------------------------------------------------------------------
diff --git a/misc/Test2.agda b/misc/Test2.agda
@@ -0,0 +1,99 @@
+postulate s :: Set
+postulate e :: Set
+postulate t :: Set
+postulate ext :: (a::Set) |-> (s -> a) -> a
+postulate int :: (a::Set) |-> a -> (s -> a)
+postulate box :: t -> t
+postulate id :: e -> e -> t
+postulate and :: t -> t -> t
+postulate or :: t -> t -> t
+postulate imply :: t -> t -> t
+postulate equiv :: t -> t -> t
+postulate not :: t -> t
+postulate forall :: (e -> t) -> t
+postulate exists :: (e -> t) -> t
+postulate H :: t -> t
+postulate F :: t -> t
+
+CN :: Set
+CN = e -> t
+
+IV :: Set
+IV = e -> t
+
+(/) :: Set -> Set -> Set
+a / b = (s -> b) -> a
+
+(//) :: Set -> Set -> Set
+a // b = (s -> b) -> a
+
+T   = t / IV
+TV  = IV / T
+IAV = IV / IV
+
+Det = T / CN
+DTV = TV / T
+TTV = TV / T
+PP  = IV / TV
+Adj :: Set
+Adj = e -> t
+
+be :: TV
+be p x = ext p (int (\(y::e) -> id x y))
+
+necessarily :: t / t
+necessarily p = box (ext p)
+
+postulate j :: e
+postulate m :: e
+postulate b :: e
+postulate n :: e
+
+John :: T
+John P = ext P j
+
+Mary :: T
+Mary P = ext P m
+
+Bill :: T
+Bill P = ext P b
+
+ninty :: T
+ninty P = ext P n
+
+a :: Det
+a p q = exists (\(x::e) -> and (ext p x) (ext q x))
+
+the :: Det
+the p q = exists (\(y::e) ->
+                  forall (\(x::e) -> and (equiv (ext p x) (id x y)) (ext q x)))
+
+every :: Det
+every p q = forall (\(x::e) -> imply (ext p x) (ext q x))
+
+no :: Det
+no p q = forall (\(x::e) -> not (and (ext p x) (ext q x)))
+
+be' :: IV / Adj
+be' P x = ext P x
+
+by :: PP / T
+by P R x = ext P (int (\(y::e) -> ext R (int (\(Q::s -> e -> t) -> ext Q x)) y))
+
+-- NG
+by' :: PP / T
+by' P R x = ext P (int (\(y::e) -> int R {! !} {! !} {! !} {! !}))
+-- λP λR λx P{^ (λy [^R(y, ^(λP P{x}))])}
+
+bar :: ((R::{! !}) -> (h::{! !}) -> {! !}) / T
+bar = \(P::s->T) -> \(R::{! !}) -> \(x::e) ->
+      ext P (int (\(y::e) -> {! !}))
+
+{-
+Q : s -> e -> x
+
+int (\Q -> ext Q x)
+-}
+
+F25 :: TV -> Adj
+F25 delta x = exists (\(y::e) -> H (delta (int (\(P::s->e->t) -> ext P x)) y))
diff --git a/misc/Test3.hs b/misc/Test3.hs
@@ -0,0 +1,53 @@
+{-# OPTIONS_GHC -fallow-undecidable-instances #-}
+-- coverage condition を満たしていないインスタンス宣言があるため
+
+-----------------------------------------------------------------------------
+
+data Prop
+data S
+data E
+
+infixl 9 :@
+
+data Expr t where
+    BVar :: Int -> Expr t
+    FVar :: String -> Expr t
+    (:@) :: Expr (a->b) -> Expr a -> Expr b
+    Lam  :: Expr b -> Expr (a->b)
+    Int  :: Expr a -> Expr (S->a)
+    Ext  :: Expr (S->a) -> Expr a
+
+-----------------------------------------------------------------------------
+
+infixl 1 :/
+
+data Sen
+data IV
+data CN
+data (:/) a b
+
+type T   = Sen :/ IV
+type TV  = IV :/ T
+type IAV = IV :/ IV
+
+data P c where
+    F :: CatToType b u => P (a :/ b) -> P b -> P a
+
+class CatToType c t | c -> t
+instance CatToType Sen Prop
+instance CatToType IV (E->Prop)
+instance CatToType CN (E->Prop)
+instance (CatToType a t, CatToType b u) => CatToType (a :/ b) ((S->u)->t)
+
+translate :: CatToType c t => P c -> Expr t
+translate (F fun arg) = translate fun :@ Int (translate arg)
+
+-----------------------------------------------------------------------------
+
+{-
+class Assoc a b | a -> b
+instance Assoc Int Int
+
+f :: Assoc Int b => Int -> b
+f x = x
+-}