シン (Sîn) は、古代メソポタミアで信仰された月の神（男神）。シンはアッカド語の名前であり、シュメール語ではナンナ (Nanna)。「ナンナ」はアッカド語ではナンナルと呼ばれる[1]。
シュメール人の都市ウルの主神でもあり、アッカド時代になるとメソポタミア諸王の王女がウルのナンナ女祭司に任じられるようになり[2]、また人名の一部としても用いられることが多くなっていった[3]。またウルと並んで、メソポタミア北部のハランもシンの祭儀の中心であった[3]。
メソポタミアにおいてシンは月を司り[4]、大地と大気の神としても信仰されていた[5]。月の規則正しく満ちては欠ける性質から「暦を司る神」とされ[4][5]、同時に、月は欠けてもまた満ちることに由来し、豊穣神としての側面を持ち合わせていたと考えられる[1]。
また、「暦の神」としてのシンは「遠い日々の運命を決める」力を持っていたとされ、彼の練る計画を知った神はいないとされる[5]。
シンボルは三日月で、三日月に似た角を持つ雄牛と深い結びつきを持つとされた[3]。
TAPL の OCaml のサンプルにはないのですが Featherweight Java を Prolog で実装したものを今日は紹介します。
FJ の実装で難しいポイントは部分型付け規則がアルゴリズム的ではないので書き換える必要があるところです:
fj.pl
% 部分型付け規則 C <: D
[C|Cs] <: [D|Ds] :- C <: D,Cs <: Ds.
C <: C.
_ <: 'Object'.
C <: E :- class C <: D ={_},D <: E.
部分型付け規則は左再帰を除去して、class定義があった場合にのみ推移則を適用するように書き換えることでアルゴリズム的に書き換えが出来ます。
あとは class 定義は直接 Prolog の述語として定義してしまって参照する感じにすると環境を持たずにかけて良い感じでした。
FJ は OOP な言語を形式的に定義したもので、京都大学の五十嵐先生によって作られたものです。
レコードの代わりに norminal な型システムをつかい Java の継承が使えますが、 fullupdate 同様にオブジェクトのフィールドを書き換えることが出来ない単純な言語です。
fj.pl
:- op(999,fx,class),op(920,xfx,[=>,=>*]),op(910,xfx,[/-]).
:- op(501,xfx,<:),op(11,yfx,#).
% 部分型付け規則 C <: D
[C|Cs] <: [D|Ds] :- C <: D,Cs <: Ds.
C <: C.
_ <: 'Object'.
C <: E :- class C <: D ={_},D <: E.
% フィールドの探索 fields(C,[f:C])
fields('Object',[]).
fields(C,FCs_):- class C<:D={FCs,_,_},fields(D,GDs),append(GDs,FCs,FCs_).
% メソッドの型の探索 mtype(M,C,[C] -> C)
mtype(M,C,Bs->B):-class C<:_={_,_,Ms},member(def(M,As:B=_),Ms),split(As,_,Bs).
mtype(M,C,T):-class C<:D={_},mtype(M,D,T).
% 補助述語
split([],[],[]).
split([X:Y|Ls],[X|Xs],[Y|Ys]) :- split(Ls,Xs,Ys).
% メソッドの本体の探索 mbody(M,C,([X],T))
mbody(M,C,(Xs,T)):- class C<:_={_,_,Ms},member(def(M,As:_={T}),Ms),split(As,Xs,_).
mbody(M,C,T):- class C<:D={_},mbody(M,D,T).
% メソッドの正当なオーバーライド override(M,D,[C]->C0)
override(M,D,_->_) :- \+mtype(M,D,_).
override(M,D,Cs->C0):- mtype(M,D,Ds->D0),Cs=Ds,C0=D0.
% 項の型付け Γ /- T : C
Γ/-X:C :- atom(X),member(X:C,Γ),!. %(T-Var)
Γ/-T0#Fi:Ci :- Γ/-T0:C0,fields(C0,FCs),member(Fi:Ci,FCs),!. %(T-Field)
Γ/-T0#(M,Ts):C:- Γ/-T0:C0,mtype(M,C0,Ds->C),Γ/-Ts:Cs,Cs<:Ds,!. %(T-Invk)
Γ/-new(C,Ts):C:- fields(C,FDs),Γ/-Ts:Cs,split(FDs,_,Ds),Cs<:Ds,!. %(T-New)
Γ/-cast(C,T0):C:- Γ/-T0:D,D<:C,!. %(T-UCast)
Γ/-cast(C,T0):C:- Γ/-T0:D,C<:D,C\=D,!. %(T-DCast)
Γ/-cast(C,T0):C:- Γ/-T0:D,\+C<:D,\+C<:D, %(T-SCast)
format('警告 ~w と ~w はキャストできません\n',[C,D]),!.
_/-[]:[] :- !. %(T-List0)
Γ/-[T|Ts]:[C|Cs]:- Γ/-T : C,Γ/-Ts : Cs,!. %(T-List1)
% メソッドの型付け okas(C,M)
okas(C,def(M,Args:C0={T0})):- [this:C|Args] /- T0:E0,E0<:C0,class C<:D={_},
split(Args,_,Cs),override(M,D,Cs->C0).
% クラスの型付け ok(C)
thisffs(this#F=F).
ok(class C<:D={FCs,K,Ms}):- K=def(this,Args={super(Gs),ThisFFs}),
maplist(thisffs,ThisFFs),fields(D,GDs),
split(GDs,Gs,_),append(GDs,FCs,Args),
maplist(okas(C),Ms),!.
ok1(Class) :- ok(Class),!.
ok1(class C<:_=_) :- format('error class ~W\n',[C,[]]),fail.
okall :- findall(class C,class C,Cs),!,maplist(ok1,Cs),!.
% 置き換え
s([]->[],T->T).
s([S|Ss]->[D|Ds],T->T_) :- s(S->D,T->T1),s(Ss->Ds,T1->T_).
s(S->D,S->D) :- atom(S).
s(_->_,X->X) :- atom(X).
s(_->_,[]->[]).
s(S->D,[X|Xs]->[X_|Xs_]) :- s(S->D,X->X_),s(S->D,Xs->Xs_).
s(S->D,(T#(M,Ts))->(T_#(M,Ts_))) :- s(S->D,T->T_),s(S->D,Ts->Ts_).
s(S->D,(T#F)->(T_#F)) :- s(S->D,T->T_).
s(S->D,new(C,Ts)->new(C,Ts_)) :- s(S->D,Ts->Ts_).
s(S->D,cast(C,T)->cast(C,T_)) :- s(S->D,T->T_).
isVal(new(C,Vs)) :- atom(C),isVals(Vs).
isVals(Vs) :- maplist(isVal,Vs).
% 値と項を分離する
splitVals([],[],[]).
splitVals([V|Ts],[V|Vs],Ts_) :- isVal(V),splitVals(Ts,Vs,Ts_).
splitVals(Ts,[],Ts).
% 評価 T => T_
new(C,Vs)#Fi=>Vi:- isVals(Vs),atom(Fi),fields(C,FCs),
nth0(I,FCs,(Fi:_)),nth0(I,Vs,Vi),!. %(E-ProjNew)
new(C,Vs)#(M,Us)=>T0_:-isVals(Vs),atom(M),mbody(M,C,(Xs,T0)),
s([this|Xs]->[new(C,Vs)|Us],T0 -> T0_),!. %(E-InvkNew)
cast(D,new(C,Vs))=>new(C,Vs):-isVals(Vs),C<:D,!. %(E-CastNew)
T0#F=>T0_#F :- atom(F),T0=>T0_,!. %(E-Field)
T0#(M,Ts)=>T0_#(M,Ts) :- atom(M),T0=>T0_,!. %(E-Invk-Recv)
V0#(M,Args)=>V0#(M,Args_):- atom(M),splitVals(Args,Vs,[Ti|Ts]),
Ti=>Ti_,append(Vs,[Ti_|Ts],Args_),!. %(E-Invk-Arg)
new(C,Args)=>new(C,Args_):- atom(C),splitVals(Args,Vs,[Ti|Ts]),
Ti=>Ti_,append(Vs,[Ti_|Ts],Args_),!. %(E-New-Arg)
cast(C,T)=>cast(C,T_) :- atom(C),T=>T_,!. %(E-Cast)
E1 =>* E3 :- E1=>E2,!,E2 =>* E3.
E1 =>* E1.
% クラス定義
class 'B' <: 'Object' = {[],def(this,[]={super([]),[]}),[]}.
class 'C' <: 'Object' = {[],def(this,[]={super([]),[]}),[]}.
class 'A' <: 'B' = {[],def(this,[]={super([]),[]}),[]}.
class 'Pair' <: 'B' = {
[fst:'B',snd:'B'],
def(this,[fst:'B',snd:'B']={
super([]),[this#fst=fst,this#snd=snd]
}),
[ def(getFst,[]:'B' = {
this#fst
}),
def(setFst,[fst:'B']:'Pair' = {
new('Pair',[fst,this#snd])
}),
def(setSnd,[snd:'B']:'Pair' = {
new('Pair',[this#fst,snd])
})
]
}.
class 'Triple' <: 'Pair' = {
[thr:'B'],
def(this,[fst:'B',snd:'B',thr:'B']={
super([fst,snd]),[this#thr=thr]
}),
[ def(setFst,[fst:'B']:'Pair' = {
new('Triple',[fst,this#snd,this#thr])
})
]
}.
% test
test(E) :-
([]/-E:T->format('~W : ~W = ',[E,[],T,[]]);format('~W : type error\n',[E,[]]),fail),
(E=>*V,writeln(V),isVal(V); writeln('runtime error'));!.
:- (okall,writeln('all classes valid.'); writeln('invalid classess.'),halt),
test(new('Pair',[new('A',[]),new('B',[])])#fst),
test(new('Pair',[new('Pair',[new('A',[]),new('B',[])])#snd,new('B',[])])#fst),
test(new('Pair',[new('A',[]),new('B',[])])#(getFst,[])),
test(new('Pair',[new('A',[]),new('B',[])])#(setFst,[new('B',[])])),
test(new('Triple',[new('A',[]),new('B',[]),new('B',[])])#(getFst,[])),
test(new('Triple',[new('A',[]),new('B',[]),new('B',[])])#(setFst,[new('B',[])])),
test(new('Triple',[new('A',[]),new('B',[]),new('B',[])])#(setSnd,[new('A',[])])),
test(cast('Object',new('Object',[]))),
test(cast('Pair',new('Object',[]))#fst),
test(cast('C',new('C',[]))),
test(cast('A',new('B',[]))),
test(cast('B',new('A',[]))),
test(cast('C',new('B',[]))),% warning
test( new('Pair',[new('Pair',[new('A',[]),new('B',[])]),new('B',[])])#fst#fst),
test(cast('Pair',new('Pair',[new('Pair',[new('A',[]),new('B',[])]),new('B',[])])#fst)#fst),
halt.
