抽象によるソフトウェア設計 第3章 論理系 その7

今日は関係演算子の定義域、値域の制限演算子説明からです。

    • s
  • :> - 値域の制限
    • r :> s は r から s の要素で終わるタプルのみ集めた集合を返す。
  • ++ - オーバーライド
    • 和集合と似ているが、 p ++ q は同じアトムで始まるタプルがあると q のタプルで上書きされる。タプルの最初の要素をキーとした時の Hash#merge みたいなもの

続いて 3.5 制約へ

  • 論理演算子 - 全て冗長形式と省略形式(記号での記法)がある
    • not, ! - 否定
    • and, && - 連言(論理積ではないんですね)
    • or, || - 選言(論理和では ry)
    • implies, => - 含意
      • implies には else を併用できる (F implies G else H)
    • iff, <=> - 両含意
  • 中括弧で複数の制約を括ると 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つだけ要素を持つとかの制約の指定もできる
  • 高階限量
    • 限量変数はスカラでなく集合や多項関係でもいい。こういうのを「高階」という
      • ただし解析できるとは限らない(直接解析してなくて「スコーレム化」で高階限量を取り除いているので、それができる時だけ)なので非推奨

関係演算子と限量子の使いかたを学びました。まだ let 式と多重度というのがあるようです。先はながい。