抽象によるソフトウェア設計 第3章 論理系 その7
-
- s
- :> - 値域の制限
- r :> s は r から s の要素で終わるタプルのみ集めた集合を返す。
- ++ - オーバーライド
- 和集合と似ているが、 p ++ q は同じアトムで始まるタプルがあると q のタプルで上書きされる。タプルの最初の要素をキーとした時の Hash#merge みたいなもの
続いて 3.5 制約へ
- 論理演算子 - 全て冗長形式と省略形式(記号での記法)がある
- 中括弧で複数の制約を括ると and で結合するのと同じ - { A B C } = A and B and C
- 限量
- Q x: e | F
- Q が限量子。e が x の範囲(集合)、F が制約
- all - 全ての x で成立する
- some - ある x について成立する
- no - 全ての x について成立しない
- lone - たかだか1つの(0 または 1) x で成立する
- one - 1つの x で成立する
- 限量子は式に直接使って、集合が空でないとか 1つだけ要素を持つとかの制約の指定もできる
- Q x: e | F
- 高階限量
- 限量変数はスカラでなく集合や多項関係でもいい。こういうのを「高階」という
- ただし解析できるとは限らない(直接解析してなくて「スコーレム化」で高階限量を取り除いているので、それができる時だけ)なので非推奨
- 限量変数はスカラでなく集合や多項関係でもいい。こういうのを「高階」という
関係演算子と限量子の使いかたを学びました。まだ let 式と多重度というのがあるようです。先はながい。