Last active
December 11, 2015 03:18
-
-
Save MasWag/4536267 to your computer and use it in GitHub Desktop.
記号論理学IIレポート
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
*.aux | |
*.log | |
*~ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-{ | |
このコードは岡本先生の記号論理学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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
\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} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment