Mercurial > hg > Papers > 2017 > atton-master
changeset 127:7903c02fe686
Update
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 16 Feb 2017 13:49:07 +0900 |
| parents | 18f872806bc0 |
| children | 9ef69d114781 |
| files | paper/agda.tex paper/atton-master.pdf |
| diffstat | 2 files changed, 6 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/agda.tex Thu Feb 16 13:39:49 2017 +0900 +++ b/paper/agda.tex Thu Feb 16 13:49:07 2017 +0900 @@ -457,7 +457,12 @@ $ \Rightarrow \mathcal{I}$ に対応するのは関数適用である。 よってこの証明は「一つの変数から \verb/fst/ と \verb/snd/ を使って関数を二つ取り出し、それぞれを関数適用する」という形になる。 これをラムダ式で書くとリスト~\ref{src:agda-modus-ponens}のようになる。 -仮定 A $ \times $ B と仮定 A から A $ \rightarrow $ C を導いている。 +仮定 $ (\text{A} \rightarrow \text{B}) \times (\text{B} \rightarrow \text{C}) $ と仮定 A から A $ \rightarrow $ C を導いている。 + +仮定に相当する変数 p の型は$ (\text{A} \rightarrow \text{B}) \times (\text{B} \rightarrow \text{C}) $ であり、p からそれぞれの命題を取り出す操作が \verb/fst/ と \verb/snd/ に相当する。 +\verb/fst p/ の型は $ (\text{A} \rightarrow \text{B}) $ であり、\verb/snd p/ の型は $ (\text{B} \rightarrow \text{C}) $ である。 +もう一つの仮定xの型は A なので、\verb/fst p/ を関数適用することで B が導ける。 +得られた B を \verb/snd p/ に適用することで最終的に C が導ける。 \lstinputlisting[label=src:agda-modus-ponens, caption=Agda における三段論法の証明] {src/AgdaModusPonens.agda.replaced}