今日もちょっとAlloyで遊んでみます。
ある目的から、自然数の区間 {0, 1, 2, ..., n} の性質の一部を抽象した構造が欲しくなりました。その構造とは次のものです。
- サクセッサ（後者関数）に基づく全順序（線形順序）
- 2点間の距離
2点間の距離とは、x, y∈{0, 1, 2, ..., n} として、次のように定義されます。
- δ(x, y) = |x - y|
ここでは便宜上引き算と絶対値で表現してますが、事前に引き算や絶対値を要求しているわけではありません。
とりあえず、サクセッサ（名前はnextにします）と順序＜（名前はlt）、それと定数ゼロ（zero）、最後の数（last）を定義してみます。
-- 自然数の区間 {0, 1, 2, ..., n}
module interval
sig Interv {
-- 後者
next: lone Interv,
-- 順序 ＜
lt: set Interv
}
-- ゼロと最後の数
one sig zero, last extends Interv {}
-- nextに関する公理
fact next {
-- lastのnextは存在しない
no last.next
and
-- last以外ではnextが定義されている
all x: (Interv - last) |
one x.next
and
-- ゼロからの可達性
zero.*next = Interv
}
-- ltに関する公理
fact lt {
lt = ^next
}不等号「＜」に相当する関係ltを上では定義してますが、nextの推移的閉包に過ぎないし、^next と書いても同じなんで、下に出てくるコードでは特にltを定義はしてません。
さて、δ(x, y) = |x - y| に相当する関係が x.delta[y] = z となるように定義します。基本的に、δ(x, x) = 0 からはじまる再帰的な定義です。x ≦ y のときだけを考えた補助関数δ0を先に定義して、それの対称化としてδを定義しました。もっとうまいやり方／Alloyらしい書き方があるかも知れませんが、とりあえず最初に思いついた方法です。
-- 自然数の区間 {0, 1, 2, ..., n}
module interval
sig Interv {
-- 後者
next: lone Interv,
-- 距離
private delta0: Interv ->one Interv,
delta: Interv ->one Interv
}
-- ゼロと最後の数
one sig zero, last extends Interv {}
-- nextに関する公理
fact next {
-- lastのnextは存在しない
no last.next
and
-- last以外ではnextが一意に定義されている
all x: (Interv - last) |
one x.next
and
-- ゼロからの可達性
zero.*next = Interv
}
-- delta0に関する公理
fact delta0 {
all x, y: Interv |
{
x.delta0[x] = zero
-- x ≦ y ならば、定義されている範囲内で
-- δ0(x, y.next) = δ0(x, y).next
y in x.*next implies
(x.delta0[y.next] in (x.delta[y]).next)
}
}
-- deltaに関する公理
fact delta {
all x, y: Interv |
-- x ≦ y ならば、δ = δ0
y in x.*next implies (delta = delta0)
-- それ以外では、δ(x, y) = δ(y, x)
else x.delta[y] = y.delta0[x]
}このくらいの定義（Alloyコード）でも、未定義部分を考慮してなかったり、「＜」と「≦」を取り違えたりと、何度も何度もAlloyアナライザーに事例（モデルインスタンス）を作らせないと正しく書けません。これ(↑)で正しい自信もありませんが、基数が2, 3の台集合上の構造としては意図どおりになっているみたいです。
