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

今日は制約の続き、let 式からです。

• let 式、let 制約
  • let x = e | A
    • A の中の x を e で置きかえる。つまりx に e を代入(束縛)して A の中で利用するという感じ
  • 再帰的な定義はできない
• 内包表記
  • { x1 : e1, x2 : e2, ... | F }
  • e1, e2, ... の各要素からなるタプルのうち制約 F を見たすものからなる多項関係を作る記法
• 宣言
  • name : expression
  • 本文の説明がわかりにくいのですが、宣言も制約の一種で集合に名前をつけるもの
  • シグネチャのフィールドの束縛変数を宣言するのによく使う
  • 集合多重度 - 宣言の expression には多重度キーワード(set, one, lone, some)を付けられる。限量子とかぶってるキーワードがあるので注意
  • 関係多重度 - 矢印演算子の前後に多重度キーワードを入れることができる
    • A -> one B、 A some -> B, A some -> one B みたいに
• 宣言式
  • expression in expression
  • 関係や式にその場で制約を加えるのに使う。見た目は宣言とはかなり違う

関係多重度の読みかたは慣れないと難しいですね。第3章はおそらくあと1日です。