記号論理学IIレポート

.gitignore

*.aux
*.log
*~

PropositionalLogic.hs

-{
このコードは岡本先生の記号論理学IIの授業のレポートのために書いたコードです。 

東京大学教養学部理科一類一年和賀正樹
}-
dpair :: Integer -> Integer -> Integer
dpair m n = ( m + n )*( m + n + 1) + 2 * m

undpair :: Integer -> ( Integer , Integer )
undpair phi = ( half - a sigma , sigma + (a sigma) - half )
  where 
    half = quot phi 2
    sigma = una half 0
    una x t | a t <= x = una x $ t+1
            | otherwise = t-1
    a :: Integer ->  Integer
    a 0 = 0
    a x = (a (x-1)) + x

o :: t ->  Integer
o _ = 1

v :: Integer ->  Integer
v m =  (2*m + 3)

s ::  Integer ->  Integer
s t = dpair 0 t

plus ::  Integer ->  Integer ->  Integer
plus t u = dpair 1 $ dpair t u

times ::  Integer ->  Integer ->  Integer
times t u = dpair 2 $ dpair t u

equal ::  Integer ->  Integer ->  Integer
equal t u = dpair 3 $ dpair t u

lesser ::  Integer ->  Integer ->  Integer
lesser t u = dpair 4 $ dpair t u

not ::  Integer ->  Integer
not phi = dpair 5 phi

_or ::  Integer ->  Integer ->  Integer
_or phi psy = dpair 6 $ dpair phi psy

_and :: Integer -> Integer ->  Integer
_and phi psy = dpair 7 $ dpair phi psy

implies ::  Integer ->  Integer ->  Integer
implies phi psy = dpair 8 $ dpair phi psy

iff ::  Integer ->  Integer ->  Integer
iff phi psy = dpair 9 $ dpair phi psy

forall ::  Integer ->  Integer ->  Integer
forall x phi = dpair 10 $ dpair x phi

exist :: Integer -> Integer ->  Integer
exist x phi = dpair 11 $ dpair x phi

introAnd :: Integer -> Integer -> Integer
introAnd phi psy = dpair 12 $ dpair phi psy
-- phi , psy |- phi /\ psy

elimAnd :: Integer -> Integer
elimAnd phi = dpair 13 $ dpair phi $ fst $ undpair $ snd $ undpair phi
-- phi /\ psy |- phi

introOr :: Integer -> Integer -> Integer
introOr phi psy = dpair 14 $ dpair phi psy
-- phi |- phi \/ psy

elimOr :: Integer -> Integer -> Integer -> Integer -> Integer
elimOr phi psy xi upsilon = dpair 15 $ dpair ( dpair phi  psy ) $ dpair xi upsilon
-- phi|psy|xi |- upsilon

introImplies :: Integer -> Integer -> Integer
introImplies psy x = dpair 16 $ dpair psy x
-- psy |- x -> psy

elimImplies :: Integer -> Integer -> Integer -> Integer
elimImplies x phi psy = dpair 17 $ dpair x $ dpair  phi psy
-- x , phi |- psy ( phi == x -> psy)

botRule :: Integer -> Integer -> Integer -> Integer
botRule phi psy xi = dpair 18 $ dpair  phi $ dpair psy xi
-- phi , psy |- bot |- xi

introAll :: Integer -> Integer
introAll phi = dpair 19 phi
-- phi |- \-/ phi

elimAll :: Integer -> Integer
elimAll phi = dpair 20 phi

introExist :: Integer -> Integer
introExist phi = dpair 21 phi

elimExist :: Integer -> Integer
elimExist phi = dpair 22 phi

decode :: Integer -> [Integer]
decode x | odd x = [x]
         | matchAny x [1,2,3,4,6,7,8,9,10,11,12,13,14,16] = [typeOfSyntax,
                                                             fst $ undpair $ snd $ undpair $ x, 
                                                             snd $ undpair $ snd $ undpair $ x]
         | matchAny x [5,19,20,21,22] = [typeOfSyntax,
                                         snd $ undpair x]
         | matchAny x [15] = [typeOfSyntax,
                              fst $ undpair $ fst $ undpair $ snd $ undpair x,
                              snd $ undpair $ fst $ undpair $ snd $ undpair x,
                              fst $ undpair $ snd $ undpair $ snd $ undpair x,
                              snd $ undpair $ snd $ undpair $ snd $ undpair x]
         | matchAny x [17,18] = [typeOfSyntax,
                                 fst $ undpair $ snd $ undpair x,
                                 snd $ undpair $ fst $ undpair $ snd $ undpair x,
                                 fst $ undpair $ snd $ undpair $ snd $ undpair x,
                                 snd $ undpair $ snd $ undpair $ snd $ undpair x]
  where
    matchAny :: Integer -> [Integer] -> Bool
    matchAny x list = or $ map (==typeOfSyntax) list
    typeOfSyntax = fst $ undpair x

report.dvi

report.pdf

report.tex

\documentclass[a4j]{jsarticle}
\title{記号論理学レポート(岡本先生)}
\author{東京大学教養学部理科一類一年 和賀正樹 240938H}
\date{}
\usepackage{latexsym}
\usepackage{proof}
\usepackage{ascmac}
\usepackage{txfonts} \usepackage{listings, jlisting} \renewcommand{\lstlistingname}{リスト} 
\lstset{language=haskell, basicstyle=\ttfamily\scriptsize,
commentstyle=\textit, 
classoffset=1, 
keywordstyle=\bfseries, 
frame=tRBl, 
framesep=5pt, 
showstringspaces=false, 
numbers=left, 
stepnumber=1, 
numberstyle=\tiny, 
tabsize=2 }
\begin{document}
\maketitle
授業中に説明された証明のエン・デコーディングに興味を持ったのでNJの証明図
のエン・デコーディングを実装してみました。言語は僕の知っている限り、一番容易
に(事実上)無限長の整数を扱えるHaskellで書きました。
\section*{方針}
鹿島先生のテキストにあった、Russel-Hilbelt系でのエン・デコーディング法を
NJの推論規則を書けるように拡張しました。例えば、
\[\infer{v_1 \wedge v_2}
 {v_1 &
 v_2}
\]
をエンコードするときには
\begin{verbatim}
introAnd (v 1) (v 2)
\end{verbatim}
の様に関数を使えばよいものとしました。\par
また、デコードはまず、dpairの結果から元の引数を求めるundpairを作り、証明
図を一段階だけデコードして結果を返す関数decodeを作りました。
例えば、先の証明図をエンコードすると31886となるが、
\begin{verbatim}
decode 31886
\end{verbatim}
を実行すると
\begin{verbatim}
[12,5,7]
\end{verbatim}
が返ってきます。これは、12がintroAndに対応し、5,7が$v_1$,$v_2$に対応するこ
とと合致しています。\par
また、不条理則、否定除去則についてはひとかたまりにして
\[\infer{\infer{\Xi}
{\bot}}
 {\Phi & \Psi}
\]
の$\Phi , \Psi,\Xi$を埋める形で実装しています。つまり、
\begin{verbatim}
botRule phi psy xi
\end{verbatim}
を実行することで両者に対応しています。\par
課題としては、試作したundpairには大きな数を処理するときにかなり時間がかかると
いうことがあります。これは実装したアルゴリズムに問題があると思われます。
\lstinputlisting[caption=実装例] {./PropositionalLogic.hs}

\end{document}