Mercurial > hg > Members > kono > Proof > automaton

comparison a02/lecture.ind @ 406:a60132983557

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 08 Nov 2023 21:35:54 +0900
parents 407684f806e4
children
comparison
equal deleted inserted replaced
405:af8f630b7e60 406:a60132983557
20 20
21 型つきλ計算と論理が対応するように、データ構造と論理演算子(∧とか∨)を対応させることにより 21 型つきλ計算と論理が対応するように、データ構造と論理演算子(∧とか∨)を対応させることにより
22 22
23 論理式を型として表し、推論を型つきλ計算の項とすると、この二つは似ていることがわかる。 23 論理式を型として表し、推論を型つきλ計算の項とすると、この二つは似ていることがわかる。
24 24
25 この章の内容は基本的には Girad 先生の Proofs and Typesに書いてある内容です。
25 26
26 --あらすじ 27 --あらすじ
27 28
28 1) 論理式を変数とそれを結ぶ演算子(connectives)で定義する 29 1) 論理式を変数とそれを結ぶ演算子(connectives)で定義する
29 これは構文定義、あるいは、論理式の作り方に相当する 30 これは構文定義、あるいは、論理式の作り方に相当する
160 161
161 162
162 163
163 record によって 164 record によって
164 165
165 record _∧_ A B : Set 166 record _∧_ A B : Set where
166 field 167 field
167 π1 : A 168 π1 : A
168 π2 : B 169 π2 : B
169 170
170 _∧_　は中置演算子を表す。 171 _∧_　は中置演算子を表す。
175 176
176 A ∧ B 177 A ∧ B
177 178
178 とかける。(Haskell では (∧) を使う) 179 とかける。(Haskell では (∧) を使う)
179 180
180 は、型Aと型Bから作るデ0ータ構造である。オブジェクトあるいは構造体だと思って良い。 181 は、型Aと型Bから作るデータ構造である。オブジェクトあるいは構造体だと思って良い。
181 182
182 record { π1 = x ; π2 = y } 183 record { π1 = x ; π2 = y }
183 184
184 185
185 ---例題 186 ---例題