定理証明手習い (65) J-Bob/リスト操作
筆者らのJ-Bob実装で最初に定義しているのはリスト操作です。
list0
要素が0個のリストを作る
list0?
要素が0個のリストかどうか
list1
要素が1個のリストを作る
list1?
要素が1個のリストかどうか
elem1
リストの1個目の要素
list2
要素が2個のリストを作る
list2?
要素が2個のリストかどうか
elem2
リストの2個目の要素
list3
要素が3個のリストを作る
list3?
要素が3個のリストかどうか
elem3
リストの3個目の要素
3個で終わり
3個までしか登場しないということだろうな
リストのn個目の要素を取る関数は要素がn個より少ないときは'()
を返します
全域性のためかな
例外処理のために使われることもあるんだろうか
リストの要素は何でも受け付けるので要素がリストでもいいし'()
でもいいので
'()
が返ってきたときは曖昧さが発生しそう
まず要素の数を確認してから、ってやるのかな
(tag sym x)
x
にsym
というタグを付ける
(tag? sym x)
x
にsym
というタグがついているかどうか
(untag x)
x
からタグを取って値を取り出す
(member x ys)
x
がys
の要素かどうか
ところでテスト項目
(my/test "tag?/yes" (tag? 'a (tag 'a 1)) 't)
(my/test "tag?/no" (tag? 'b (tag 'a 1)) 'nil)
(my/test "untag" (untag (tag 'a 1)) '1)
こういうテストと
(my/test "tag" (tag 'a 1) '(a . 1))
こういうテスト
上のテストは外部仕様的なところ
証明を書くとしたらこういう感じの定理を証明するんだろうな
下のテストは内部の実装が見えてる形
本来は不要なはずだけど、コード見ながらだとこういうテストも書きたくなるな
上のテストだけで十分、って言える?