局所定義
局所的な定義をする式let式(局所定義) |
let パターン:型=式,...,パターン:型=式 in 式 :型 は省略可 |
let x:nat = 1 in x + 1
let x = 1 in x + 1
let x:nat = 1, y:nat = 2 in x + y
let f:nat -> nat1 f(x) == x + 1 in f(2)
|
let be式(条件マッチ局所定義) |
let 多重束縛 be st 条件式 in 式 |
let x in set {1,2,3,4} be st x mod 2 = 0 in x
let b1, b2:bool be st b1 => b2 in mk_(b1, b2)
|
場合分け
場合分けをする式if式(真偽値による場合分け) |
if 条件式 then 式 else 式 if 条件式 then 式 elseif 条件式 then 式 ... else 式 |
if 3 mod 2 = 0 then <偶数> else <奇数>
if 10 mod 15 = 0 then <フィズバズ> elseif 10 mod 5 = 0 then <バズ> elseif 10 mod 3 = 0 then <フィズ> else 10
|
cases式(パターンマッチによる場合分け) |
cases 式: パターン,..,パターン -> 式,...,パターン,...,パターン -> 式, others -> 式 end デフォルト定義 , others -> 式 は省略可 |
cases mk_('+', 1, 2):
cases "03-123-4567":
|
比較
等号や非等号の左右の値の型が合っていなければならないことに注意。等値 | = |
? * ? -> bool |
1 = 1
1 = 2
1 = '1'
'1' = '1'
1 = 1.0
|
非等値 | <> |
? * ? -> bool |
1 <> 1
1 <> 2
1 <> '1'
'1' <> '2'
1 <> 1.0
|
> | > |
real * real -> bool |
1 > 1
2 > 1
|
≧ | >= |
real * real -> bool |
1 >= 1
1 >= 2
|
< | < |
real * real -> bool |
1 < 1
1 < 2
|
≦ | <= |
real * real -> bool |
1 <= 1
2 <= 1
|
数式
加算 | + |
real * real -> real |
1 + 2
|
減算 | - |
real * real -> real |
1 - 2
|
乗算 | * |
real * real -> real |
1 * 2
|
除算 | / |
real * real -> real |
1 / 2
1 / 0
|
累乗 | ** |
real * real -> real |
2 ** 3
|
商 | + |
int * int -> int |
1 div 2
1 div 0
|
剰余1 | mod |
int * int -> int |
1 mod 2
-1 mod 2
1 mod -2
1 mod 0
|
剰余2 | rem |
int * int -> int |
1 rem 2
-1 rem 2
1 rem -2
1 rem 0
|
絶対値 | abs |
real -> real |
abs 2
abs -1
|
符号反転 | - |
real -> real |
- 3.14
-(2 + 3)
|
底 | floor |
real -> int |
floor 3.14
floor -3.14
|
論理式
否定 | not |
bool -> bool |
not true
not false
|
論理積 | and |
bool * bool -> bool |
true and true
true and false
true and undefined
false and undefined
undefined and false
|
論理和 | or |
bool * bool -> bool |
false or false
true or false
true or undefined
false or undefined
undefined or true
|
含意 | => |
bool * bool -> bool |
true => true
true => false
false => false
false => undefined
undefined => true
|
同値 | <=> |
bool * bool -> bool |
true <=> true
false <=> false
true <=> false
|
非等値(排他論理和) | <> |
bool * bool -> bool |
true <> true
true <> false
|
要素の取り出し
組 | 組.#自然数リテラル |
mk_(1, 'a', 3).#1
mk_(1, 'a', 3).#2
mk_(1, 'a', 3).#3
|
レコード | レコード.フィールド名 |
mk_Point(1,2).x
mk_Point(1,2).y
|
適用
列(リスト) | 列式(自然数式) |
[0,2,4](2)
[0,2,4](10)
|
写像(連想配列、マップ) | 写像式(式) |
{0 |-> false, 1 |-> true}(0)
|
関数(ラムダ式を含む) | 関数式(式,式,...,式) |
(lambda x:nat & x + 1)(2)
|
操作 |
操作() 操作(式,式,...,式) |
inc()
add(2)
|
コンストラクタ
組 | mk_(式,式,...,式) |
mk_(1,2,3)
mk_("abc", nil, 1)
|
トークン | mk_token(式) |
mk_token(1)
mk_token("abc")
mk_token(nil)
|
レコード | mk_コンストラクタ(式,式,...,式) |
mk_Point(1, 2.3)
|
外延表記(列挙)
集合 |
{} {式,式,...,式}
|
{}
{1,2,3}
{1,2,{'3', nil}}
{1,...,10}
|
列(リスト) |
[] [式,式,...,式] "文字列" |
[]
[1,2,3]
[1,2,['3', nil]]
"文字列"
"文字列" = ['文', '字', '列']
|
写像(連想配列、マップ) |
{|->} {式 |->式 ,式 |-> 式,...,式 |-> 式}
|
{|->}
{<りんご> |-> 100, <レタス> |-> 200, <大根> |-> 150}
|
内包表記
集合 |
{x * 2 | x in set {1, ... ,5}}
{x * 2 | x in set {1, ... ,5} & x mod 2 = 0}
{mk_(b1, b2, b1 and b2) | b1,b2 : bool}
|
列(リスト) |
[x * 2 | x in set {1, ... ,5}]
[x * 2 | x in set {1, ... ,5} & x mod 2 = 0]
|
写像(連想配列、マップ) |
{"0123456789"(i+1) |-> i | i in set {0,...,9}}
{"0123456789"(i+1) |-> i | i in set {0,...,9} & i mod 2 = 0}
|
集合演算
要素 | in set |
T * set of T -> bool |
1 in set {1,2,3}
0 in set {1,2,3}
{1,2} in set {0, {1, 2}, 3}
|
非要素 | not in set |
T * set of T -> bool |
1 not in set {1,2,3}
0 not in set {1,2,3}
{1,2} not in set {0, {1, 2}, 3}
|
部分集合 | subset |
set of T * set of T -> bool |
{1,2} subset {1,2,3}
{1,2,3} subset {1,2,3}
{1,2,3} subset {1,2}
|
真部分集合 | psubset |
set of T * set of T -> bool |
{1,2} psubset {1,2,3}
{1,2,3} psubset {1,2,3}
{1,2,3} psubset {1,2}
|
和集合 | union |
set of T * set of T -> set of T |
{1,2} union {2,3}
|
共通部分 | inter |
set of T * set of T -> set of T |
{1,2} inter {2,3}
|
差集合 | \ |
set of T * set of T -> set of T |
{1,2} \ {2,3}
|
濃度(要素の数) | card |
set of T -> nat |
card {1,...,10}
card {1, 2, nil}
card {}
|
分配和集合 | dunion |
set of set of T -> set of T |
dunion {{1,2}, {2,3}}
dunion {{{1},2}, {2,3}}
|
分配共通部分 | dinter |
set of set of T -> set of T |
dinter {{1,2}, {2,3}}
dinter {{1,2, {3}}, {2,3}}
|
べき集合 | power |
set of T -> set of set of T |
power {1,2,3}
power {}
|
列(リスト)
スライス | ( ,..., ) |
seq of T * nat1 * nat1 -> T |
"任意の文字列"(4,...,5)]
"任意の文字列"(5,...,4)]
"任意の文字列"(4,...,10)]
|
先頭要素 | hd |
seq1 of T -> T |
hd [1,2,3]
hd "文字列"
|
続き | tl |
seq1 of T -> seq of T |
tl [1,2,3]
tl "文字列"
|
長さ | len |
seq of T -> nat |
len [1,2,3,4,5]
len "文字列"
|
要素集合 | elems |
seq of T -> set of T |
elems [1,2,3,4,5]
elems "文字列"
|
添字集合 | inds |
seq of T -> set of nat1 |
inds [0,2,4]
inds "文字列"
|
逆順 | reverse |
seq of T -> seq of T |
reverse [0,2,4]
reverse "文字列"
|
連結 | ^ |
seq of T * seq of T -> seq of T |
[0,2,4]^[1,3,5]
"文字"^"列"
|
分配連結 | conc |
seq of seq of T -> seq of T |
conc [[0,2,4],[1,3,5]]
conc ["文字","列"]
|
上書き | ++ |
seq of T * map nat1 to T -> seq of T |
[0,2,4]++{2|->10}
"文字列"++{1|->'数'}]
|
写像(連想配列、マップ)
定義域 | dom |
map T1 to T2 -> set of T1 |
dom {0 |-> false, 1 |-> true}
|
値域 | rng |
map T1 to T2 -> set of T2 |
rng {0 |-> false, 1 |-> true}
|
併合 | munion |
map T1 to T2 * map T1 to T2 -> map T1 to T2 |
{0 |-> false, 1 |-> true} munion {2 |-> false, 3 |-> true}
{0 |-> false, 1 |-> true} munion {1 |-> true, 2 |-> false}
{0 |-> false, 1 |-> true} munion {1 |-> false, 2 |-> false}
|
上書き | ++ |
map T1 to T2 * map T1 to T2 -> map T1 to T2 |
{0 |-> false, 1 |-> true} ++ {2 |-> false, 3 |-> true}
{0 |-> false, 1 |-> true} ++ {1 |-> false, 2 |-> false}
|
分配併合 | merge |
set of map T1 to T2 -> map T1 to T2 |
merge {{0 |-> false, 1 |-> true}, {2 |-> false, 3 |-> true}}
merge {{0 |-> false, 1 |-> true}, {1 |-> false, 2 |-> false}}
|
定義域制限 | <: |
set of T1 * map T1 to T2 -> map T1 to T2 |
{2,3} <: {0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true}
|
定義域除外 | <-: |
set of T1 * map T1 to T2 -> map T1 to T2 |
{2,3} <-: {0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true}
|
値域制限 | :> |
map T1 to T2 * set of T2 -> map T1 to T2 |
{0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true} :> {true, nil}
|
値域除外 | :-> |
map T1 to T2 * set of T2 -> map T1 to T2 |
{0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true} :-> {true, nil}
|
合成 | comp |
map T2 to T3 * map T1 to T2 -> map T1 to T3 |
{true|-><奇数>, false|-><偶数>} comp {0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true}
|
繰り返し | ** |
map T1 to T1 * nat -> map T1 to T1 |
{0 |-> 1, 1 |-> 2, 2 |-> 3, 3 |-> 3} ** 1
{0 |-> 1, 1 |-> 2, 2 |-> 3, 3 |-> 3} ** 2
{0 |-> 1, 1 |-> 2, 2 |-> 3, 3 |-> 3} ** 3
|
逆写像 | inverse |
inmap T1 to T2 -> inmap T2 to T1 |
inverse {0 |-> '0', 1 |-> '1', 2 |-> '2'}
|
量化
多くの組み合わせに関する特性を書く式全称式(あらゆる) | forall 多重束縛,...,多重束縛 & 式 |
forall i in set {1,2,3} & i mod 4 <> 0
forall i in set {1,2,3} & i mod 2 <> 0
forall b1,b2:bool & b1 or b2
|
存在式(少なくとも1つ) | exists 多重束縛,...,多重束縛 & 式 |
exists i in set {1,2,3} & i mod 4 = 0
exists i in set {1,2,3} & i mod 2 = 0
exists b1,b2:bool & b1 and b2
|
ユニーク存在式(1つだけ) | exists1 束縛 & 式 |
exists1 i in set {1,2,3} & i mod 2 = 0
exists1 i in set {1,2,3} & i mod 2 <> 0
exists1 mk_(b1,b2):bool*bool & b1 and b2
|
イオタ式
集合や型から、条件に合致する唯一の値を取り出す式。 ユニーク存在式と関係が深い。イオタ式 | iota 束縛 & 式 |
iota i in set {1,2,3} & i mod 2 = 0
iota i in set {1,2,3} & i mod 4 = 0
iota i in set {1,2,3} & i mod 2 = 1
|
関数
関数を表す式ラムダ式 | lambda 引数:型,...,引数:型 & 式 |
(lambda x:real, y:real & x + y)(1,2)
(lambda x:real & lambda y:real & x + y)(1)(2)
|
型判別
値の型を判別する式一般is式 | is_(式, 型) |
is_(10, nat1)
is_(3.14, nat1)
is_(10, real)
is_({1,...,10}, set of nat1)
|
基本型is式 | is_型(式) |
is_nat1(10+20)
is_nat1(3.14)
is_real(10)
is_token(mk_token("abc"^"xyz"))
|
未定義
未定義値を表す未定義式 | undefined |
undefined
nil = undefined
{1,2,undefined}
{1,2} union undefined
|