Blawxの動作原理メモ
Blawxブロックの定義
Blawxのブロックの実体はプログラミング言語Prolog(SWI Prolog)で定義されている
また、 S(CASP) ライブラリを使用している
SWISH -- SWI-Prolog for SHaring
:- use_module(library(scasp)).
swiplserver を使用してサーバーサイドでPrologを実行
Code Editorの右側のタブS(CASP) を選択すると、ブロックに対応するPrologソースコードが確認できる
前提:Prologの文法おさらい
Prologでは計算方法(手続き)の代わりに事実関係を記述する
(少し違うが)SQL的なイメージ
真偽判定
条件を満たす対象の検索
変数の代入が少し独特
変数を指定すると、条件に当てはまる何らかの値が代入(マッチ)される
例: son_of(X, Y): 「son of X is Y (YはXの子である)」
son_of(sazae, Y)→ Y = tarao
Prolog始めました - 'きぃの独話'
Prologおすすめ本(syuparn.iconの個人的趣味): 7つの言語 7つの世界
構文
%: コメント
_: 無名変数(パターンマッチのためだけに使われ中身は見ない)
大文字始まりの識別子(Hoge): 変数
小文字始まりの識別子(hoge): アトム
名前を表す定数のようなもの
Rubyでいうシンボル :hoge
乱暴だけど文字列リテラル "hoge" と思ってもいいかも
※大文字小文字の区別はBlawxのブロックでも同じ!
. : 文の終わり
他言語でいう ;
:-: 定義
A :- B は数学的に書くと B => A (BならばA)
mammal(X) :- human(X).
言い換えると human(X) ならば mammal(X)
左辺の foo(X) の部分(functor)は関数と似ているが、戻り値の構文は無い
代わりに、受け取りたい結果の引数に(まだマッチしていない)変数を指定する
例: count_blawx_list([a, b, c], Length) (変数 Length で計算結果である 3 を受け取る)
=: 単一化
通常のプログラミング言語のような「左辺を右辺に代入」という意味だけではない
数学的な等式に近い
左辺と右辺が等しくなるよう変数へ値が代入される
右辺の変数にマッチすることも可能
例:
2 = X. → X は 2 になる
[A, 2] = [1, B]. → A は 1、B は 2 になる
is 演算子: 右辺を計算した結果が左辺と等しい
= の場合は右辺の式そのものと左辺が等しいかどうかを検証(計算はしない)
参考: https://ist.ksc.kwansei.ac.jp/~kitamura/lecture/PROLOG/EXERSICES/r2.pdf
条件の組み合わせ方
OR: 定義を2つ併記する
foo(X) :- {条件1}. foo(X) :- {条件2}
AND: 定義を , で繋いで記載する
foo(X) :- {条件1}, {条件2}.
※Blawxのブロックで条件分岐を表わす方法も同じ!
[Head | Tail]: リストを先頭要素と2番目以降の要素のリスト(無い場合は空リスト)に分割
[1, 2, 3] = [Head | Tail]. → Head は 1、Tailは [2, 3]
(むしろリストの内部実装的に [1, 2, 3] が [1 | [2 | [3 | []]]] の糖衣構文と言ったほうが正確?→ 参考 )
先頭要素を取り出し、残りの処理を同じ述語の引数に渡す再帰的な定義によく使われる
s(CASP)の構文
#pred: s(CASP)の構文
Blawx作者の技術記事より引用: https://medium.com/computational-law-diary/how-rules-as-code-makes-laws-better-115ab62ab6c4
These #pred statements tell s(CASP) how to translate your code back into English once s(CASP) has turned your rules and your facts into an answer and an explanation.
述語に対する説明文を定義
テスト結果等の表示に使用可能
例:#pred blawx_comparison(X,eq,Y) :: '@(X) is equal to @(Y)'.
#pred の動作原理
あまりにも蛇足だったのでQiitaへ: https://qiita.com/Syuparn/items/9eeebf8f0e26d4a5cf03
演算子 #=, #<>, #<, #>, #=<, #>=, \=
# が付いているのがPrologの組み込み演算子との違い
https://github.com/SWI-Prolog/sCASP/blob/bae608edbed74ef3cdcbdd92ebeaeb27c300349d/prolog/scasp/load_compiled.pl#L11
これらもs(CASP)の組み込み演算子として定義されていそう
https://github.com/SWI-Prolog/sCASP/blob/bae608edbed74ef3cdcbdd92ebeaeb27c300349d/prolog/scasp/predicates.pl#L89
どう違う?
同じ
s(CASP)が当初実装されていたCiao Prolog形式の演算子はSWI-Prolog形式に置き換えられる
https://github.com/SWI-Prolog/sCASP/blob/bae608edbed74ef3cdcbdd92ebeaeb27c300349d/prolog/scasp/clp/clpq.pl#L72
Translate Ciao style clp(Q) constraints into an expression that can be handled by clp(Q) {Goal}.
code:prolog
:- op(700, fx, not, #).
:- op(700, xfx, (.\=.), (.=.)).
:- op(700, xfx, #=, #<>, #<, #>, #=<, #>=).
Prolog, s(CASP)上に表現されたBlawxの設計思想
全体的にProlog, s(CASP)の構文に沿ってブロックが作られている
変数:Prologの変数で表現
https://scrapbox.io/files/67dfd79d7aaf5bf60c777b61.png
A = 0.
オブジェクト:Prologのアトムで表現
属性は述語で表現
https://scrapbox.io/files/67e20b5ab960e0777bfe567e.png
person(foo).: foo (という名前)はpersonである
https://scrapbox.io/files/67e23b3a05e58aaa29096963.png
age(foo,20).: foo (という名前)のageは20である
foo そのものは変数ではなく値であることに注意!
fooという名前を表わす値なので、そこに何かを代入することはできない
※オブジェクトを宣言したとき、いわゆる「構造体」のようなデータ構造は生成されていない
データ構造としては名前しか存在しない
カテゴリもfunctorの名前として定義されているだけであり、クラスのようなものがあるわけではない
そのため、継承関係等の考慮は不要
(見た目上は、TypeScript等の構造的部分型を持つ言語とあまり使用感は変わらなそう)
自身が何のカテゴリであり、どんな属性を持つかは述語によって定義される
カテゴリ、属性の定義:#predで述語の宣言
person や age を定義
https://scrapbox.io/files/67e244775daabc6fec4ea1a4.png
述語の宣言: #pred person(X) :: '@(X) is a person'.
person という名前がカテゴリであることも別途定義: blawx_category(foo).
https://scrapbox.io/files/67e24558094abeac950ef169.png
blawx_attribute(person,age,number).
#pred age(X,Y) :: '@(X) \'s age is @(Y)'.
属性の型も blawx_attribute の述語で定義される
Prologに静的型の構文は無いため
型の誤りはブロック側で検知している?
型が合わないブロックははまらないようになっている
ブロックに表示されるメッセージの形式も#pred 右辺のメッセージを使用している?(自信なし)
ルール:Prologのルール:-で表現
https://scrapbox.io/files/67e21638900b4ad62bda1367.png
code:prolog
animal(X) :-
person(X).
順番が逆になることに注意!
A ならば B は B :- A. なので
(ここから先は詳しく知りたい方向けのメモ(長いです))
Pythonソースコード中のProlog定義を読む
blawx/aggregates.py
listsブロックに関連する処理
https://scrapbox.io/files/67dea6907619847b7b20eefa.png
count_blawx_list: リストの要素数
sum_blawx_list: 合計
average_blawx_list
max_blawx_list
min_blawx_list
blawx_list_not_between
blawx_not_between(List,Start,End): List の全要素が [Start, End] の範囲外にある(Start 以下 or End 以上)
どこで使っている?
blawx_list_not_before(List, End): List の全要素が End 以上
blawx_list_not_after(List, Start): Listの全要素が Start 以下
code:prolog
count_blawx_list([],0).
count_blawx_list([_|[]],1).
count_blawx_list(_|Rest,Count) :-
Rest \= [],
count_blawx_list(Rest,RestCount),
Count is RestCount + 1.
sum_blawx_list([],0).
sum_blawx_list([Any|[]],Any).
sum_blawx_list(First|Rest,Sum) :-
Rest \= [],
sum_blawx_list(Rest,RestSum),
Sum is First + RestSum.
average_blawx_list([Any|[]],Any).
average_blawx_list(List,Average) :-
count_blawx_list(List,Count),
sum_blawx_list(List,Sum),
Average is Sum / Count.
% If there is only one element, the maximum of that list is the element.
max_blawx_list([Any|[]],Any).
% If there are three elements, the maximum is either the first element, or the maximum of the remainder
max_blawx_list(First|Rest,First) :-
max_blawx_list(Rest,RestMax),
First #>= RestMax.
max_blawx_list(First|Rest,RestMax) :-
max_blawx_list(Rest,RestMax),
First #< RestMax.
min_blawx_list([Any|[]],Any).
min_blawx_list(First|Rest,First) :-
min_blawx_list(Rest,RestMin),
First #=< RestMin.
min_blawx_list(First|Rest,RestMin) :-
min_blawx_list(Rest,RestMin),
First #> RestMin.
blawx_list_not_between(Head|Tail,Start,End) :-
blawx_not_between(Head,Start,End),
blawx_list_not_between(Tail,Start,End).
blawx_list_not_between([],_,_).
blawx_not_between(X,Y,Z) :- X =< Y.
blawx_not_between(X,Y,Z) :- X >= Z.
blawx_list_not_before(Head|Tail,End) :-
Head >= End,
blawx_list_not_before(Tail,End).
blawx_list_not_before([],_).
blawx_list_not_after(Head|Tail,Start) :-
Head =< Start,
blawx_list_not_after(Tail,Start).
blawx_list_not_after([],_).
blawx/dates.py
以下は時刻や日付を表わす組み込みの述語?
微妙に引数が違うのが気になる
https://www.swi-prolog.org/pldoc/man?section=timedate
date: 日付
time: 時刻
datetime:
duration:
date_add: duration 後の時刻
duration_compare, date_compare: 時刻の大小比較
第二引数のアトムで演算切り替え(eq, lt 等)
code:prolog
% ※コメントアウトされている行は省略
#pred date_add(X,Y,Z) :: 'adding @(Y) to @(X) gives @(Z)'.
#pred date_compare(X,eq,Y) :: '@(X) is the same as @(Y)'.
#pred date_compare(X,lt,Y) :: '@(X) is before @(Y)'.
#pred date_compare(X,lte,Y) :: '@(X) is on or before @(Y)'.
#pred date_compare(X,gt,Y) :: '@(X) is after @(Y)'.
#pred date_compare(X,gte,Y) :: '@(X) is on or after @(Y)'.
#pred date_compare(X,ne,Y) :: '@(X) is not the same as @(Y)'.
#pred duration_compare(X,eq,Y) :: '@(X) is the same as @(Y)'.
#pred duration_compare(X,lt,Y) :: '@(X) is larger than @(Y)'.
#pred duration_compare(X,lte,Y) :: '@(X) is larger than or the same as @(Y)'.
#pred duration_compare(X,gt,Y) :: '@(X) is less than @(Y)'.
#pred duration_compare(X,gte,Y) :: '@(X) is less than or the same as @(Y)'.
#pred duration_compare(X,ne,Y) :: '@(X) is not the same as @(Y)'.
date_add(date(X),duration(Y),datetime(Z)) :- Z #= X + Y.
date_add(datetime(X),duration(Y),datetime(Z)) :- Z #= X + Y.
date_add(date(X),time(Y),datetime(Z)) :- Z #= X + Y.
date_compare(time(X),eq,time(X)).
date_compare(time(X),lt,time(Y)) :- X #< Y.
date_compare(time(X),gt,time(Y)) :- X #> Y.
date_compare(time(X),lte,time(Y)) :- X #=< Y.
date_compare(time(X),gte,time(Y)) :- X #>= Y.
date_compare(time(X),ne,time(Y)) :- X \= Y.
date_compare(datetime(X),eq,datetime(X)).
date_compare(datetime(X),lt,datetime(Y)) :- X #< Y.
date_compare(datetime(X),gt,datetime(Y)) :- X #> Y.
date_compare(datetime(X),lte,datetime(Y)) :- X #=< Y.
date_compare(datetime(X),gte,datetime(Y)) :- X #>= Y.
date_compare(datetime(X),ne,datetime(Y)) :- X \= Y.
date_compare(date(X),eq,datetime(X)).
date_compare(date(X),lt,datetime(Y)) :- X #< Y.
date_compare(date(X),gt,datetime(Y)) :- X #> Y.
date_compare(date(X),lte,datetime(Y)) :- X #=< Y.
date_compare(date(X),gte,datetime(Y)) :- X #>= Y.
date_compare(date(X),ne,datetime(Y)) :- X \= Y.
date_compare(datetime(X),eq,date(X)).
date_compare(datetime(X),lt,date(Y)) :- X #< Y.
date_compare(datetime(X),gt,date(Y)) :- X #> Y.
date_compare(datetime(X),lte,date(Y)) :- X #=< Y.
date_compare(datetime(X),gte,date(Y)) :- X #>= Y.
date_compare(datetime(X),ne,date(Y)) :- X \= Y.
date_compare(date(X),eq,date(X)).
date_compare(date(X),lt,date(Y)) :- X #< Y.
date_compare(date(X),gt,date(Y)) :- X #> Y.
date_compare(date(X),lte,date(Y)) :- X #=< Y.
date_compare(date(X),gte,date(Y)) :- X #>= Y.
date_compare(date(X),ne,date(Y)) :- X \= Y.
duration_compare(duration(X),eq,duration(X)).
duration_compare(duration(X),lt,duration(Y)) :- X #< Y.
duration_compare(duration(X),gt,duration(Y)) :- X #> Y.
duration_compare(duration(X),lte,duration(Y)) :- X #=< Y.
duration_compare(duration(X),gte,duration(Y)) :- X #>= Y.
duration_compare(duration(X),ne,duration(Y)) :- X \= Y.
blawx/events.py
dateとdatetimeの相互変換
code:prolog
blawx_as_of(X,datetime(Y)) :- blawx_as_of(X,date(Y)).
blawx_during(datetime(X),Y,datetime(Z)) :- blawx_during(date(X),Y,date(Z)).
blawx_during(datetime(X),Y,datetime(Z)) :- blawx_during(date(X),Y,datetime(Z)).
blawx_during(datetime(X),Y,datetime(Z)) :- blawx_during(datetime(X),Y,date(Z)).
blawx_becomes(X,datetime(Y)) :- blawx_becomes(X,date(Y)).
blawx/ldap.py
(LDAP認証とは関係ない)
#pred で宣言だけされていて実装が無い
code:prolog
% We need language for the applies predicate that is not related to any other predicate.
#pred blawx_applies(Y,X) :: '@(Y) applies to @(X)'.
#pred holds(user,blawx_applies,Y,Z) :: 'it is provided as a fact that @(Y) applies to @(Z)'.
#pred holds(user,-blawx_applies,Y,Z) :: 'it is provided as a fact that it is not the case that @(Y) applies to @(Z)'.
#pred holds(X,blawx_applies,Y,Z) :: 'the conclusion in @(X) that @(Y) applies to @(Z) holds'.
#pred holds(X,-blawx_applies,Y,Z) :: 'the conclusion in @(X) that it is not the case that @(Y) applies to @(Z) holds'.
#pred according_to(X,blawx_applies,Y,Z) :: 'according to @(X) @(Y) applies to @(Z)'.
#pred according_to(X,-blawx_applies,Y,Z) :: 'according to @(X) it is not the case that @(Y) applies to @(Z)'.
#pred defeated(X,blawx_applies,Y,Z) :: 'the conclusion in @(X) that @(Y) applies to @(Z) is defeated'.
#pred defeated(X,-blawx_applies,Y,Z) :: 'the conclusion in @(X) that it is not the case that @(Y) applies to @(Z) is defeated'.
blawx/passthrough.py
比較演算子を定義
blawx_diseq: XとYが等しいかどうか
blawx_comparison: 比較演算子
code:prolog
#pred blawx_diseq(X,Y) :: '@(X) is not the same object as @(Y)'.
blawx_diseq(X,Y) :- X \= Y.
#pred blawx_comparison(X,eq,Y) :: '@(X) is equal to @(Y)'.
#pred blawx_comparison(X,neq,Y) :: '@(X) is not equal to @(Y)'.
#pred blawx_comparison(X,gt,Y) :: '@(X) is greater than @(Y)'.
#pred blawx_comparison(X,gte,Y) :: '@(X) is greater than or equal to @(Y)'.
#pred blawx_comparison(X,lt,Y) :: '@(X) is less than @(Y)'.
#pred blawx_comparison(X,lte,Y) :: '@(X) is less than or equal to @(Y)'.
blawx_comparison(X,eq,Y) :- X #= Y.
blawx_comparison(X,neq,Y) :- X \= Y.
blawx_comparison(X,gt,Y) :- X #> Y.
blawx_comparison(X,gte,Y) :- X #>= Y.
blawx_comparison(X,lt,Y) :- X #< Y.
blawx_comparison(X,lte,Y) :- X #=< Y.
Blawxブロックにより生成されるProlog実装を読む
Primary
We Know
何も生成されない
When we know [ ] we also know [ ]
:-でつなぐ
https://scrapbox.io/files/67e21638900b4ad62bda1367.png
code:prolog
animal(X) :-
person(X).
Exceptions
Known Sections
Categories
[ ] is a Category Appearing as: "[ ] object [ ]"
blawx_category: カテゴリ名をアトムを使って定義
blawx_category_nlg: ブロックを説明するメッセージの定義
ブロックに表示されるテキストはここから拾っている?
#pred foo(X) :: '@(X) is a foo'.: カテゴリを宣言するための述語
#pred blawx_as_of(foo(X),T)
こんな風に使われている
blawx_as_of(age(X,Y),datetime(Time)) :- blawx_initially(age(X,Y)), BeforeT #< Time,blawx_not_interrupted(datetime(bot),age(X,Y),datetime(BeforeT)).
初期状態でXのageがY、Timeよりも前の状態で中断されていなければblawx_as_ofも成り立つ(どういうこと?)
OpenFiscaのように、ある時に制度改正され条件が変わることを表現するために使用する?
#pred blawx_becomes(foo(X),T)
https://scrapbox.io/files/67dfd531f9001433787da59f.png
code:prolog
blawx_category(foo).
blawx_category_nlg(foo,"","is a foo").
:- dynamic foo/1.
#pred foo(X) :: '@(X) is a foo'.
#pred holds(user,foo,X) :: 'it is provided as a fact that @(X) is a foo'.
#pred holds(user,-foo,X) :: 'it is provided as a fact that it is not the case that @(X) is a foo'.
#pred holds(Z,foo,X) :: 'the conclusion in @(Z) that @(X) is a foo holds'.
#pred holds(Z,-foo,X) :: 'the conclusion in @(Z) that it is not the case that @(X) is a foo holds'.
#pred according_to(Z,foo,X) :: 'according to @(Z), @(X) is a foo'.
#pred according_to(Z,-foo,X) :: 'according to @(Z), it is not the case that @(X) is a foo'.
#pred blawx_defeated(Z,foo,X) :: 'the conclusion in @(Z) that @(X) is a foo is defeated'.
#pred blawx_defeated(Z,-foo,X) :: 'the conclusion in @(Z) that it is not the case that @(X) is a foo is defeated'.
#pred blawx_initially(foo(X)) :: 'that @(X) is a foo holds initially'.
#pred blawx_initially(-foo(X)) :: 'that it is not the case that @(X) is a foo holds initially'.
#pred blawx_ultimately(foo(X)) :: 'that @(X) is a foo holds ultimately'.
#pred blawx_ultimately(-foo(X)) :: 'that it is not the case that @(X) is a foo holds ultimately'.
#pred blawx_as_of(foo(X),T) :: 'that @(X) is a foo holds at @(T)'.
#pred blawx_as_of(-foo(X),T) :: 'that it is not the case that @(X) is a foo holds at @(T)'.
#pred blawx_during(T1,foo(X),T2) :: 'that @(X) is a foo held between @(T1) and @(T2)'.
#pred blawx_during(T1,-foo(X),T2) :: 'that it is not the case that @(X) is a foo held between @(T1) and @(T2)'.
#pred blawx_becomes(foo(X),T) :: 'that @(X) is a foo became true at @(T)'.
#pred blawx_becomes(-foo(X),T) :: 'that it is not the case that @(X) is a foo became true at @(T)'.
#pred blawx_not_interrupted(Start,foo(X),End) :: '@(X) is a foo remained the case between @(Start) and @(End)'.
#pred blawx_not_interrupted(Start,-foo(X),End) :: 'it is not the case that @(X) is a foo remained the case between @(Start) and @(End)'.
blawx_not_interrupted(datetime(Start),foo(X),datetime(End)) :- Start \= bot, End \= eot, findall(Time,blawx_becomes(-foo(X),datetime(Time)),Times),blawx_list_not_between(Times,Start,End).
blawx_not_interrupted(datetime(Start),-foo(X),datetime(End)) :- Start \= bot, End \= eot, findall(Time,blawx_becomes(foo(X),datetime(Time)),Times),blawx_list_not_between(Times,Start,End).
blawx_not_interrupted(datetime(bot),foo(X),datetime(End)) :- End \= eot, findall(Time,blawx_becomes(-foo(X),datetime(Time)),Times),blawx_list_not_before(Times,End).
blawx_not_interrupted(datetime(bot),-foo(X),datetime(End)) :- End \= eot, findall(Time,blawx_becomes(foo(X),datetime(Time)),Times),blawx_list_not_before(Times,End).
blawx_not_interrupted(datetime(Start),foo(X),datetime(eot)) :- Start \= bot, findall(Time,blawx_becomes(-foo(X),datetime(Time)),Times),blawx_list_not_after(Times,Start).
blawx_not_interrupted(datetime(Start),-foo(X),datetime(eot)) :- Start \= bot, findall(Time,blawx_becomes(foo(X),datetime(Time)),Times),blawx_list_not_after(Times,Start).
blawx_not_interrupted(datetime(bot),foo(X),datetime(eot)) :- blawx_initially(foo(X)), blawx_ultimately(foo(X)), findall(Time,blawx_becomes(-foo(X),datetime(Time)),[]).
blawx_not_interrupted(datetime(bot),-foo(X),datetime(eot)) :- blawx_initially(-foo(X)), blawx_ultimately(-foo(X)), findall(Time,blawx_becomes(foo(X),datetime(Time)),[]).
blawx_as_of(foo(X),datetime(Time)) :- blawx_initially(foo(X)), BeforeT #< Time,blawx_not_interrupted(datetime(bot),foo(X),datetime(BeforeT)).
blawx_as_of(foo(X),datetime(Time)) :- blawx_becomes(foo(X),datetime(BeforeT)),BeforeT #< Time,blawx_not_interrupted(datetime(BeforeT),foo(X),datetime(Time)).
blawx_as_of(-foo(X),datetime(Time)) :- blawx_initially(-foo(X)), BeforeT #< Time,blawx_not_interrupted(datetime(bot),-foo(X),datetime(BeforeT)).
blawx_as_of(-foo(X),datetime(Time)) :- blawx_becomes(-foo(X),datetime(BeforeT)),BeforeT #< Time,blawx_not_interrupted(datetime(BeforeT),-foo(X),datetime(Time)).
blawx_during(datetime(Start),foo(X),datetime(End)) :- blawx_becomes(foo(X),datetime(Start)), blawx_becomes(-foo(X),datetime(End)), Start #< End, blawx_not_interrupted(datetime(Start),foo(X),datetime(End)).
blawx_during(datetime(bot),foo(X),datetime(End)) :- blawx_initially(foo(X)), blawx_becomes(-foo(X),datetime(End)), blawx_not_interrupted(datetime(bot),foo(X),datetime(End)).
blawx_during(datetime(Start),foo(X),datetime(eot)) :- blawx_ultimately(foo(X)), blawx_becomes(-foo(X),datetime(Start)), blawx_not_interrupted(datetime(Start),foo(X),datetime(eot)).
blawx_during(datetime(bot),foo(X),datetime(eot)) :- blawx_initially(foo(X)), blawx_ultimately(foo(X)), blawx_becomes(-foo(X),datetime(Start)), blawx_not_interrupted(datetime(bot),foo(X),datetime(eot)).
blawx_during(datetime(Start),-foo(X),datetime(End)) :- blawx_becomes(-foo(X),datetime(Start)), blawx_becomes(foo(X),datetime(End)), Start #< End, blawx_not_interrupted(datetime(Start),-foo(X),datetime(End)).
blawx_during(datetime(bot),-foo(X),datetime(End)) :- blawx_initially(-foo(X)), blawx_becomes(foo(X),datetime(End)), blawx_not_interrupted(datetime(bot),-foo(X),datetime(End)).
blawx_during(datetime(Start),-foo(X),datetime(eot)) :- blawx_ultimately(-foo(X)), blawx_becomes(foo(X),datetime(Start)), blawx_not_interrupted(datetime(Start),-foo(X),datetime(eot)).
blawx_during(datetime(bot),-foo(X),datetime(eot)) :- blawx_initially(-foo(X)), blawx_ultimately(-foo(X)), blawx_becomes(-foo(X),datetime(Start)), blawx_not_interrupted(datetime(bot),-foo(X),datetime(eot)).
The category [ ] has an attribute [ ]
blawx_attribute(person,age,number): attirbuteを定義
age(X,Y) ageを定義する述語の宣言
https://scrapbox.io/files/67e2125c3940db3abc76e0c5.png
code:prolog
blawx_attribute(person,age,number).
blawx_attribute_nlg(age,ov,"","'s age is","").
:- dynamic age/2.
#pred age(X,Y) :: '@(X) \'s age is @(Y)'.
#pred holds(user,age,X,Y) :: 'it is provided as a fact that @(X) \'s age is @(Y)'.
#pred holds(user,-age,X,Y) :: 'it is provided as a fact that it is not the case that @(X) \'s age is @(Y)'.
#pred holds(Z,age,X,Y) :: 'the conclusion in @(Z) that @(X) \'s age is @(Y) holds'.
#pred holds(Z,-age,X,Y) :: 'the conclusion in @(Z) that it is not the case that @(X) \'s age is @(Y) holds'.
#pred according_to(Z,age,X,Y) :: 'according to @(Z), @(X) \'s age is @(Y)'.
#pred according_to(Z,-age,X,Y) :: 'according to @(Z), it is not the case that @(X) \'s age is @(Y)'.
#pred blawx_defeated(Z,age,X,Y) :: 'the conclusion in @(Z) that @(X) \'s age is @(Y) is defeated'.
#pred blawx_defeated(Z,-age,X,Y) :: 'the conclusion in @(Z) that @(X) \'s age is @(Y) is defeated'.
#pred blawx_initially(age(X,Y)) :: 'that @(X) \'s age is @(Y) holds initially'.
#pred blawx_initially(-age(X,Y)) :: 'that it is not the case that @(X) \'s age is @(Y) holds initially'.
#pred blawx_ultimately(age(X,Y)) :: 'that @(X) \'s age is @(Y) holds ultimately'.
#pred blawx_ultimately(-age(X,Y)) :: 'that it is not the case that @(X) \'s age is @(Y) holds ultimately'.
#pred blawx_as_of(age(X,Y),T) :: 'that @(X) \'s age is @(Y) holds at @(T)'.
#pred blawx_as_of(-age(X,Y),T) :: 'that it is not the case that @(X) \'s age is @(Y) holds at @(T)'.
#pred blawx_during(T1,age(X,Y),T2) :: 'that @(X) \'s age is @(Y) held between @(T1) and @(T2)'.
#pred blawx_during(T1,-age(X,Y),T2) :: 'that it is not the case that @(X) \'s age is @(Y) held between @(T1) and @(T2)'.
#pred blawx_becomes(age(X,Y),T) :: 'that @(X) \'s age is @(Y) became true at @(T)'.
#pred blawx_becomes(-age(X,Y),T) :: 'that it is not the case that @(X) \'s age is @(Y) became true at @(T)'.
#pred blawx_not_interrupted(Start,age(X,Y),End) :: '@(X) \'s age is @(Y) remained the case between @(Start) and @(End)'.
#pred blawx_not_interrupted(Start,-age(X,Y),End) :: 'it is not the case that @(X) \'s age is @(Y) remained the case between @(Start) and @(End)'.
blawx_not_interrupted(datetime(Start),age(X,Y),datetime(End)) :- Start \= bot, End \= eot, findall(Time,blawx_becomes(-age(X,Y),datetime(Time)),Times),blawx_list_not_between(Times,Start,End).
blawx_not_interrupted(datetime(Start),-age(X,Y),datetime(End)) :- Start \= bot, End \= eot, findall(Time,blawx_becomes(age(X,Y),datetime(Time)),Times),blawx_list_not_between(Times,Start,End).
blawx_not_interrupted(datetime(bot),age(X,Y),datetime(End)) :- End \= eot, findall(Time,blawx_becomes(-age(X,Y),datetime(Time)),Times),blawx_list_not_before(Times,End).
blawx_not_interrupted(datetime(bot),-age(X,Y),datetime(End)) :- End \= eot, findall(Time,blawx_becomes(age(X,Y),datetime(Time)),Times),blawx_list_not_before(Times,End).
blawx_not_interrupted(datetime(Start),age(X,Y),datetime(eot)) :- Start \= bot, findall(Time,blawx_becomes(-age(X,Y),datetime(Time)),Times),blawx_list_not_after(Times,Start).
blawx_not_interrupted(datetime(Start),-age(X,Y),datetime(eot)) :- Start \= bot, findall(Time,blawx_becomes(age(X,Y),datetime(Time)),Times),blawx_list_not_after(Times,Start).
blawx_not_interrupted(datetime(bot),age(X,Y),datetime(eot)) :- blawx_initially(age(X,Y)), blawx_ultimately(age(X,Y)), findall(Time,blawx_becomes(-age(X,Y),datetime(Time)),[]).
blawx_not_interrupted(datetime(bot),-age(X,Y),datetime(eot)) :- blawx_initially(-age(X,Y)), blawx_ultimately(-age(X,Y)), findall(Time,blawx_becomes(age(X,Y),datetime(Time)),[]).
blawx_as_of(age(X,Y),datetime(Time)) :- blawx_initially(age(X,Y)), BeforeT #< Time,blawx_not_interrupted(datetime(bot),age(X,Y),datetime(BeforeT)).
blawx_as_of(age(X,Y),datetime(Time)) :- blawx_becomes(age(X,Y),datetime(BeforeT)),BeforeT #< Time,blawx_not_interrupted(datetime(BeforeT),age(X,Y),datetime(Time)).
blawx_as_of(-age(X,Y),datetime(Time)) :- blawx_initially(-age(X,Y)), BeforeT #< Time,blawx_not_interrupted(datetime(bot),-age(X,Y),datetime(BeforeT)).
blawx_as_of(-age(X,Y),datetime(Time)) :- blawx_becomes(-age(X,Y),datetime(BeforeT)),BeforeT #< Time,blawx_not_interrupted(datetime(BeforeT),-age(X,Y),datetime(Time)).
blawx_during(datetime(Start),age(X,Y),datetime(End)) :- blawx_becomes(age(X,Y),datetime(Start)), blawx_becomes(-age(X,Y),datetime(End)), Start #< End, blawx_not_interrupted(datetime(Start),age(X,Y),datetime(End)).
blawx_during(datetime(bot),age(X,Y),datetime(End)) :- blawx_initially(age(X,Y)), blawx_becomes(-age(X,Y),datetime(End)), blawx_not_interrupted(datetime(bot),age(X,Y),datetime(End)).
blawx_during(datetime(Start),age(X,Y),datetime(eot)) :- blawx_ultimately(age(X,Y)), blawx_becomes(-age(X,Y),datetime(Start)), blawx_not_interrupted(datetime(Start),age(X,Y),datetime(eot)).
blawx_during(datetime(bot),age(X,Y),datetime(eot)) :- blawx_initially(age(X,Y)), blawx_ultimately(age(X,Y)), blawx_becomes(-age(X,Y),datetime(Start)), blawx_not_interrupted(datetime(bot),age(X,Y),datetime(eot)).
blawx_during(datetime(Start),-age(X,Y),datetime(End)) :- blawx_becomes(-age(X,Y),datetime(Start)), blawx_becomes(age(X,Y),datetime(End)), Start #< End, blawx_not_interrupted(datetime(Start),-age(X,Y),datetime(End)).
blawx_during(datetime(bot),-age(X,Y),datetime(End)) :- blawx_initially(-age(X,Y)), blawx_becomes(age(X,Y),datetime(End)), blawx_not_interrupted(datetime(bot),-age(X,Y),datetime(End)).
blawx_during(datetime(Start),-age(X,Y),datetime(eot)) :- blawx_ultimately(-age(X,Y)), blawx_becomes(age(X,Y),datetime(Start)), blawx_not_interrupted(datetime(Start),-age(X,Y),datetime(eot)).
blawx_during(datetime(bot),-age(X,Y),datetime(eot)) :- blawx_initially(-age(X,Y)), blawx_ultimately(-age(X,Y)), blawx_becomes(-age(X,Y),datetime(Start)), blawx_not_interrupted(datetime(bot),-age(X,Y),datetime(eot)).
[ ] is a relationship between ...
blawx_relationship で複数オブジェクトの関係性を定義
https://scrapbox.io/files/67e2136ad34d049dd3154b87.png
code:prolog
blawx_relationship(relationship_name,number,number,number).
blawx_relationship_nlg(relationship_name,"","","","").
:- dynamic relationship_name/3.
#pred relationship_name(A,B,C) :: '@(A) @(B) @(C)'.
#pred holds(user,relationship_name,A,B,C) :: 'it is provided as a fact that @(A) @(B) @(C)'.
#pred holds(user,-relationship_name,A,B,C) :: 'it is provided as a fact that it is not the case that @(A) @(B) @(C)'.
#pred holds(Z,relationship_name,A,B,C) :: 'the conclusion in @(Z) that @(A) @(B) @(C) holds'.
#pred holds(Z,-relationship_name,A,B,C) :: 'the conclusion in @(Z) that it is not the case that @(A) @(B) @(C) holds'.
#pred according_to(Z,relationship_name,A,B,C) :: 'according to @(Z), @(A) @(B) @(C)'.
#pred according_to(Z,-relationship_name,A,B,C) :: 'according to @(Z), it is not the case that @(A) @(B) @(C)'.
#pred blawx_defeated(Z,relationship_name,A,B,C) :: 'the conclusion in @(Z) that @(A) @(B) @(C) is defeated'.
#pred blawx_defeated(Z,-relationship_name,A,B,C) :: 'the conclusion in @(Z) that @(A) @(B) @(C) is defeated'.
#pred blawx_initially(relationship_name(A,B,C)) :: 'that @(A) @(B) @(C) holds initially'.
#pred blawx_initially(-relationship_name(A,B,C)) :: 'that it is not the case that @(A) @(B) @(C) holds initially'.
#pred blawx_ultimately(relationship_name(A,B,C)) :: 'that @(A) @(B) @(C) holds ultimately'.
#pred blawx_ultimately(-relationship_name(A,B,C)) :: 'that it is not the case that @(A) @(B) @(C) holds ultimately'.
#pred blawx_as_of(relationship_name(A,B,C),T) :: 'that @(A) @(B) @(C) holds at @(T)'.
#pred blawx_as_of(-relationship_name(A,B,C),T) :: 'that it is not the case that @(A) @(B) @(C) holds at @(T)'.
#pred blawx_during(T1,relationship_name(A,B,C),T2) :: 'that @(A) @(B) @(C) held between @(T1) and @(T2)'.
#pred blawx_during(T1,-relationship_name(A,B,C),T2) :: 'that it is not the case that @(A) @(B) @(C) held between @(T1) and @(T2)'.
#pred blawx_becomes(relationship_name(A,B,C),T) :: 'that @(A) @(B) @(C) became true at @(T)'.
#pred blawx_becomes(-relationship_name(A,B,C),T) :: 'that it is not the case that @(A) @(B) @(C) became true at @(T)'.
#pred blawx_not_interrupted(Start,relationship_name(A,B,C),End) :: '@(A) @(B) @(C) remained the case between @(Start) and @(End)'.
#pred blawx_not_interrupted(Start,-relationship_name(A,B,C),End) :: 'it is not the case that @(A) @(B) @(C) remained the case between @(Start) and @(End)'.
blawx_not_interrupted(datetime(Start),relationship_name(A,B,C),datetime(End)) :- Start \= bot, End \= eot, findall(Time,blawx_becomes(-relationship_name(A,B,C),datetime(Time)),Times),blawx_list_not_between(Times,Start,End).
blawx_not_interrupted(datetime(Start),-relationship_name(A,B,C),datetime(End)) :- Start \= bot, End \= eot, findall(Time,blawx_becomes(relationship_name(A,B,C),datetime(Time)),Times),blawx_list_not_between(Times,Start,End).
blawx_not_interrupted(datetime(bot),relationship_name(A,B,C),datetime(End)) :- End \= eot, findall(Time,blawx_becomes(-relationship_name(A,B,C),datetime(Time)),Times),blawx_list_not_before(Times,End).
blawx_not_interrupted(datetime(bot),-relationship_name(A,B,C),datetime(End)) :- End \= eot, findall(Time,blawx_becomes(relationship_name(A,B,C),datetime(Time)),Times),blawx_list_not_before(Times,End).
blawx_not_interrupted(datetime(Start),relationship_name(A,B,C),datetime(eot)) :- Start \= bot, findall(Time,blawx_becomes(-relationship_name(A,B,C),datetime(Time)),Times),blawx_list_not_after(Times,Start).
blawx_not_interrupted(datetime(Start),-relationship_name(A,B,C),datetime(eot)) :- Start \= bot, findall(Time,blawx_becomes(relationship_name(A,B,C),datetime(Time)),Times),blawx_list_not_after(Times,Start).
blawx_not_interrupted(datetime(bot),relationship_name(A,B,C),datetime(eot)) :- blawx_initially(relationship_name(A,B,C)), blawx_ultimately(relationship_name(A,B,C)), findall(Time,blawx_becomes(-relationship_name(A,B,C),datetime(Time)),[]).
blawx_not_interrupted(datetime(bot),-relationship_name(A,B,C),datetime(eot)) :- blawx_initially(-relationship_name(A,B,C)), blawx_ultimately(-relationship_name(A,B,C)), findall(Time,blawx_becomes(relationship_name(A,B,C),datetime(Time)),[]).
blawx_as_of(relationship_name(A,B,C),datetime(Time)) :- blawx_initially(relationship_name(A,B,C)), BeforeT #< Time,blawx_not_interrupted(datetime(bot),relationship_name(A,B,C),datetime(BeforeT)).
blawx_as_of(relationship_name(A,B,C),datetime(Time)) :- blawx_becomes(relationship_name(A,B,C),datetime(BeforeT)),BeforeT #< Time,blawx_not_interrupted(datetime(BeforeT),relationship_name(A,B,C),datetime(Time)).
blawx_as_of(-relationship_name(A,B,C),datetime(Time)) :- blawx_initially(-relationship_name(A,B,C)), BeforeT #< Time,blawx_not_interrupted(datetime(bot),-relationship_name(A,B,C),datetime(BeforeT)).
blawx_as_of(-relationship_name(A,B,C),datetime(Time)) :- blawx_becomes(-relationship_name(A,B,C),datetime(BeforeT)),BeforeT #< Time,blawx_not_interrupted(datetime(BeforeT),-relationship_name(A,B,C),datetime(Time)).
blawx_during(datetime(Start),relationship_name(A,B,C),datetime(End)) :- blawx_becomes(relationship_name(A,B,C),datetime(Start)), blawx_becomes(-relationship_name(A,B,C),datetime(End)), Start #< End, blawx_not_interrupted(datetime(Start),relationship_name(A,B,C),datetime(End)).
blawx_during(datetime(bot),relationship_name(A,B,C),datetime(End)) :- blawx_initially(relationship_name(A,B,C)), blawx_becomes(-relationship_name(A,B,C),datetime(End)), blawx_not_interrupted(datetime(bot),relationship_name(A,B,C),datetime(End)).
blawx_during(datetime(Start),relationship_name(A,B,C),datetime(eot)) :- blawx_ultimately(relationship_name(A,B,C)), blawx_becomes(-relationship_name(A,B,C),datetime(Start)), blawx_not_interrupted(datetime(Start),relationship_name(A,B,C),datetime(eot)).
blawx_during(datetime(bot),relationship_name(A,B,C),datetime(eot)) :- blawx_initially(relationship_name(A,B,C)), blawx_ultimately(relationship_name(A,B,C)), blawx_becomes(-relationship_name(A,B,C),datetime(Start)), blawx_not_interrupted(datetime(bot),relationship_name(A,B,C),datetime(eot)).
blawx_during(datetime(Start),-relationship_name(A,B,C),datetime(End)) :- blawx_becomes(-relationship_name(A,B,C),datetime(Start)), blawx_becomes(relationship_name(A,B,C),datetime(End)), Start #< End, blawx_not_interrupted(datetime(Start),-relationship_name(A,B,C),datetime(End)).
blawx_during(datetime(bot),-relationship_name(A,B,C),datetime(End)) :- blawx_initially(-relationship_name(A,B,C)), blawx_becomes(relationship_name(A,B,C),datetime(End)), blawx_not_interrupted(datetime(bot),-relationship_name(A,B,C),datetime(End)).
blawx_during(datetime(Start),-relationship_name(A,B,C),datetime(eot)) :- blawx_ultimately(-relationship_name(A,B,C)), blawx_becomes(relationship_name(A,B,C),datetime(Start)), blawx_not_interrupted(datetime(Start),-relationship_name(A,B,C),datetime(eot)).
blawx_during(datetime(bot),-relationship_name(A,B,C),datetime(eot)) :- blawx_initially(-relationship_name(A,B,C)), blawx_ultimately(-relationship_name(A,B,C)), blawx_becomes(-relationship_name(A,B,C),datetime(Start)), blawx_not_interrupted(datetime(bot),-relationship_name(A,B,C),datetime(eot)).
Events
Numbers
数値
https://scrapbox.io/files/67e0a79c5cd89c8a288f5568.png
0
加減乗除
https://scrapbox.io/files/67e0a0193cdbea49dff7e891.png
(*, / が +, - より先に計算されないように)かっこでくくる
( 0 + 0 )
比較演算子
https://scrapbox.io/files/67e0a768ad74b68e886a4e47.png
blawx_comparison(0,lt,0)
Dates
dateには3種類の「型」がある
カレンダーのアイコン:date
時計のアイコン:time
カレンダーと時計のアイコン:datetime
動的型付け言語のPrologでどうやって型を実現?
時刻操作の述語の定義で引数に時刻の型を表わす述語を使用することで、誤った型を使用した場合に未定義になるようにしている
例: date_add(datetime(946652400),duration(600),X)
[ ] is set to the current date
https://scrapbox.io/files/67e0a922b07af5f5b04ee312.png
blawx_today(X)
[ ] is set to the current datetime
https://scrapbox.io/files/67e0aa061e3bcbb3136e4c95.png
blawx_now(X)
日付、時刻
https://scrapbox.io/files/67e0aa1fc5b6873a37ee3a70.png
date(946652400)
unixtimeで表現される?
https://scrapbox.io/files/67e0aa31ba11ce8f057fbf4c.png
datetime(946652400)
https://scrapbox.io/files/67e0aa6111962569da789193.png
time(0)
duration
https://scrapbox.io/files/67e0ab5fdf2dc29439dbdb19.png
duration(0)
加算に使用
時刻の比較
加算
https://scrapbox.io/files/67e0ab5fdf2dc29439dbdb19.png
date_add(datetime(946652400),duration(600),X)
時刻の変換?
https://scrapbox.io/files/67e207663ad10b058547ec49.png
time(A)
Lists
Empty List
https://scrapbox.io/files/67dfdf4c040d318c0241f5df.png
[]
[X], [Y]
[X | Y]
(構文)[Head | Tail]: リストを先頭要素と2番目以降の要素のリスト(無い場合は空リスト)に分割
例:
https://scrapbox.io/files/67dfe1a4a5f3bd94cf698f63.png
[0 | []] (= [0])
https://scrapbox.io/files/67dfe2324f7535bc50c689c9.png
[0 | [1 | []]]. (= [0, 1])
[ ] is the count of the elements of [ ]
count_blawx_list
例:
https://scrapbox.io/files/67dfe0fbec706aeffa95b118.png
count_blawx_list([0 | 1] , X)
[値] is a list of all the values of [値] returns for {文}
findall
https://www.swi-prolog.org/pldoc/man?predicate=findall/3
https://scrapbox.io/files/67dfe45251fe17884b52b595.png
findall(Age , name(Person,Age) , Ages).
Objects
[ ] is a {category名}
変数のカテゴリを指定
person(foo).
https://scrapbox.io/files/67e20b5ab960e0777bfe567e.png
[ ] and [ ] are the same object
[ ] and [ ] are not the same object
https://scrapbox.io/files/67e20dded776e07bbbac703e.png
blawx_diseq(A,B)
[ ] is in the category {category名}
オブジェクトがカテゴリに属する
https://scrapbox.io/files/67e20ae7bc80f16a7c354c63.png
person(A)
[ ] is a person との使い分けは?
こちらは主に [ ] is a {category名}によって生成された新規オブジェクトをはめるために使う
=あるcategoryのオブジェクトが別のcateogryにも属することを宣言したい場合
[ ] is a person はオブジェクト(アトム)の新規作成のため
Known Objects
オブジェクトを表わすアトム
[ ] is a {category名} を宣言すると使用可能になる
アトムなので変数ブロックと違い、代入はできない(foo という名前を表わすオブジェクト)
この名前を別の述語(ブロック)に渡すことでオブジェクトの属性を定義する
https://scrapbox.io/files/67e20ef989a9c25f9a0f7f32.png
foo
Known Attributes
属性
https://scrapbox.io/files/67e23b3a05e58aaa29096963.png
age(foo,20)
Known Relationships
Logic
it is false that
- (否定の単項演算子)
例:https://scrapbox.io/files/67dfd828f8872b07a0368ad9.png
-blawx_comparison(0,gt,1).
there is no evidence that
not (否定の単項演算子)
- が「誤りである」ことを示すのに対し、こちらは「正しいとは言えない」(誤りであるかどうかも分からない)ことを表わす
s(CASP) の推論で出てくるメッセージも there is no evidence that...
https://swish.swi-prolog.org/example/scasp.swinb
例: https://scrapbox.io/files/67dfd8ee2956d9a50f826a5e.png
not blawx_comparison(0,gt,1).
[X] is [the same value as] [Y]
X {比較演算子} Y
例:
https://scrapbox.io/files/67dfdaa27eb54adc74a0cc1c.png
0 = 0.
Variables
{変数名}
変数
例:https://scrapbox.io/files/67dfd5e0612e036c798cadc4.png
A
any
_ 無名変数(パターンマッチのためだけに使われ中身は見ない)
例:https://scrapbox.io/files/67dfd7c3e56485525b9e22ec.png
_
[ ] is set to [ ]
{左辺} = {右辺}.
例:
https://scrapbox.io/files/67dfd79d7aaf5bf60c777b61.png
A = 0.
#blawx