Alloy本いただいた
Alloy本を献本でいただいた。けど、「はじめに」しか読んでない。
昨日、他もチラチラ眺めたが、チラチラではどうも分からないな。疑問を感じたところをメモしておこう。ちゃんと読めばたぶん分かるだろうから、後で読むときに「気をつける」ポイントだな。
- 仕様と述語はどう違うの？
- 仕様とアサーションはどう違うの？
- アトムのリテラルは説明専用？
- タプルと一元（sigleton）関係はほんとに同じ？
- 部分集合と単項（unary）関係はほんとに同じ？
- フィールドってなに？
- sigってなに？（インスティチューションのsigと関係するのか）
- インスタンスってなに？（アトムとは全然違うが、語感がアトムっぽい）
- なんで、集合の直積に '->' を使う？ そのココロは？
- なんで型システムがあるんだ？ 関係計算だけじゃダメ？
- 整数ってなに？ なんで整数だけ付け足しっぽい？
- 入れ子タプルは認めてないようだが、強調してないな。直積もフラットな直積になるよな。
- 一階の対象（タプルの集合）までしか認めてないのに高階論理風の論理式が出てくるけど、あれはなに？
- 「+」は和集合か、直和はないの？ 直和である条件を制約として書く？ メンドイ。
- univとnoneの扱いが不明。
- サイズと基数って同じじゃないの？
- アリティだけで、関係のプロファイルのようなものはないのか。
- 関係の定義がこれはどうなのかな。単純すぎない？
- 転置や推移的閉包が2項関係にしか定義できない。入れ子タプルを認めないと、一般の関係を2項に落とすこともできないし。フラットタプル型をペアにしたプロファイルが認められるなら、たいていのことは出来そうだが。
- “実行”で検索する検索空間がイマイチはっきりしない。
- 代数や余代数で定式化できないの？
- loneをなんて発音する？ エルワン、ローン？
- 一階の論理式でも、対象物が関係なら、アトムから数えて二階にいると思うが。
