next up previous contents
Next: E Dynamic-Signatures Dialog Up: RELFUN Guide: Programming with Previous: C Builtin-Sorts Dialog

D User-Defined Sorts Dialog

 

rfi-p> exec pet.bat

relfun
rfi-p> sp
rfi-p> inter
rfi-p> sortstyle static
rfi-p> destroy
rfi-p> destroy-sortbase
rfi-p> 
rfi-p> % Demo of sorts in Interpreter and Compiler  
rfi-p> % ----------------------------------------------------------------------
rfi-p> % New Relfun commands:  sortbase - for looking at the module sortbase
rfi-p> %                       consult-sortbase - to load the module sortbase
rfi-p> %                       destroy-sortbase - to delete the module sortbase
rfi-p> %                       compile-sortbase - to precompile the module sortbase
rfi-p> %                       complete-taxonomy - to check if the
rfi-p> %                                           taxonomy is complete,
rfi-p> %                                           i.e. intensional glb
rfi-p> %                                              = extensional glb
rfi-p> %                       unique-glb - to check if the taxonomy is
rfi-p> %                                    unambiguous, i.e. there is at most
rfi-p> %                                    one glb for two sorts.
rfi-p> %                       unsubsumes - subsumes(a,b) -> a(X) :- b(X)
rfi-p> %
rfi-p> %                       sortstyle - to alternate between sort models
rfi-p> %                                   (dynamic and static), or (without
rfi-p> %                                   argument) to indicate the chosen 
rfi-p> %                                   model
rfi-p> % compile-sortbase, complete-taxonomy, unique-glb can only be executed
rfi-p> % in the static model.
rfi-p> %
rfi-p> % In the dynamic model it is necessary to make sure that a glb-calculation
rfi-p> % was loaded in the current database module. Depending on the implementation of
rfi-p> % these calculations the "sort knowledge" can be chosen in the subsumes 
rfi-p> % notation or Horn logic notation. In this dialog the subsumes notation is used,
rfi-p> % therefore the command unsubsumes is not needed.
rfi-p> 
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> 
rfi-p> sortstyle
static
rfi-p> % preset static
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> %                     STATIC MODEL
rfi-p> 
rfi-p> % Loading an incomplete taxonomy
rfi-p> consult-sortbase "exa1"
Reading file "/home/rfm/RELFUN/RFM/demo/types/sorts/exa1.rfp"
rfi-p> %        *a*
rfi-p> %       {1-6}
rfi-p> %     /     \
rfi-p> %    b      g
rfi-p> %  {1-5}  {1,3,6}
rfi-p> %    |      |
rfi-p> %    c      |
rfi-p> %  {1-4}    |
rfi-p> %    |      |
rfi-p> %    d      |
rfi-p> %  {1-3}    |
rfi-p> %    |      |
rfi-p> %   *e*     |
rfi-p> %  {1,2}    |
rfi-p> %      \    |
rfi-p> %       \   f
rfi-p> %          {1}
rfi-p> 
rfi-p> 
rfi-p> sortbase
subsumes(a,b).
subsumes(b,c).
subsumes(c,d).
subsumes(d,e).
subsumes(e,f).
subsumes(a,g).
subsumes(g,f).
g(6).
g(3).
b(5).
c(4).
d(3).
e(2).
f(1).
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> 
rfi-p> compile-sortbase
rfi-p> 
rfi-p> complete-taxonomy
Taxonomy is not complete: B G 
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> destroy-sortbase
rfi-p> % Loading an ambiguous taxonomy 
rfi-p> 
rfi-p> consult-sortbase "exa4"
Reading file "/home/rfm/RELFUN/RFM/demo/types/sorts/exa4.rfp"
rfi-p> 
rfi-p> 
rfi-p> %  a        b
rfi-p> %  \ \    / /
rfi-p> %   \  \/  /  
rfi-p> %    \/  \/
rfi-p> %     c   d
rfi-p> %      \ /
rfi-p> %       e
rfi-p> 
rfi-p> 
rfi-p> 
rfi-p> sortbase
subsumes(a,d).
subsumes(a,c).
subsumes(b,c).
subsumes(b,d).
subsumes(c,e).
subsumes(d,e).
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> 
rfi-p> compile-sortbase
rfi-p> 
rfi-p> complete-taxonomy
rfi-p> 
rfi-p> 
rfi-p> unique-glb
Taxonomy is not well defined: A B 
rfi-p> 
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> destroy-sortbase
rfi-p> 
rfi-p> % Loading the "pet sortbase"
rfi-p> 
rfi-p> consult-sortbase "pet-base-sub"
Reading file "/home/rfm/RELFUN/RFM/demo/types/sorts/pet-base-sub.rfp"
rfi-p> 
rfi-p> compile-sortbase
rfi-p> 
rfi-p> sortbase
subsumes(pet,mammal).
subsumes(mammal,dog).
subsumes(mammal,horse).
subsumes(mammal,cat).
subsumes(pet,fish).
subsumes(fish,goldfish).
subsumes(pet,bird).
subsumes(bird,canary).
dog(lassy).
dog(fido).
horse(fury).
cat(tom).
cat(garfield).
goldfish(goldy).
canary(tweety).
rfi-p> 
rfi-p> browse-sortbase
rfi-p> 
rfi-p> complete-taxonomy
rfi-p> 
rfi-p> unique-glb
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> %
rfi-p> % UNIFICATION OF SORTS
rfi-p> %
rfi-p> 
rfi-p> X is $pet, X is $dog
bnd[X,$dog]
X=$dog
rfi-p> 
rfi-p> X is $dog, X is $pet
bnd[X,$dog]
X=$dog
rfi-p> 
rfi-p> X is $dog, X is $cat
unknown
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> X is $dog, X is lassy
lassy
X=lassy
rfi-p> 
rfi-p> X is lassy, X is $dog
lassy
X=lassy
rfi-p> 
rfi-p> X is $dog, X is fury
unknown
rfi-p> 
rfi-p> X is fury, X is $dog
unknown
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> X is $dog, X is dom[lassy,fido]
bnd[X,dom[lassy,fido]]
X=dom[lassy,fido]
rfi-p> 
rfi-p> X is $dog, X is dom[lassy,fido, fifi]
bnd[X,dom[lassy,fido]]
X=dom[lassy,fido]
rfi-p> 
rfi-p> X is $dog, X is dom[lassy,fido, goldy]
bnd[X,dom[lassy,fido]]
X=dom[lassy,fido]
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> 
rfi-p> %
rfi-p> % USE OF SORTS
rfi-p> %
rfi-p> 
rfi-p> % Anonymous sorts
rfi-p> 
rfi-p> az eats($cat, $fish).
rfi-p> 
rfi-p> eats(tom, goldy)
true
rfi-p> 
rfi-p> 
rfi-p> eats(X, Y)
true
X=bnd[Anon213*1,$cat]
Y=bnd[Anon214*1,$fish]
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> 
rfi-p> % Named sorts
rfi-p> 
rfi-p> az young(tom).
rfi-p> az eats(X : $cat, $bird) :- young(X).
rfi-p> 
rfi-p> 
rfi-p> l eats
eats($cat,$fish).
eats(X:$cat,$bird) :- young(X).
rfi-p> 
rfi-p> eats(X,Y)
true
X=bnd[Anon219*1,$cat]
Y=bnd[Anon220*1,$fish]
rfi-p> m
true
X=tom
Y=bnd[Anon222*1,$bird]
rfi-p> m
unknown
rfi-p> 
rfi-p> eats(tom,tweety)
true
rfi-p> 
rfi-p> eats(garfield,tweety)
unknown
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> %
rfi-p> % Queries for the "sort base"
rfi-p> %
rfi-p> subsumes(mammal,X)
true
X=dog
rfi-p> m
true
X=horse
rfi-p> m
true
X=cat
rfi-p> m
unknown
rfi-p> 
rfi-p> % Listing of the "terminal sorts" immediately possible:
rfi-p> tupof(cat(X),X)
[tom,garfield]
rfi-p> 
rfi-p> 
rfi-p> % Listing of all the sorts only possible after unsubsumes:
rfi-p> unsubsumes
rfi-p> sortbase
pet(X) :- mammal(X).
mammal(X) :- dog(X).
mammal(X) :- horse(X).
mammal(X) :- cat(X).
pet(X) :- fish(X).
fish(X) :- goldfish(X).
pet(X) :- bird(X).
bird(X) :- canary(X).
dog(lassy).
dog(fido).
horse(fury).
cat(tom).
cat(garfield).
goldfish(goldy).
canary(tweety).
rfi-p> 
rfi-p> tupof(pet(X), X)
[lassy,fido,fury,tom,garfield,goldy,tweety]
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> %
rfi-p> % UNARY PREDICATES FOR THE SORT TEST
rfi-p> %
rfi-p> az hunted(X : $bird) :- pet(Y), eats(Y, X).
rfi-p> 
rfi-p> hunted(tweety)
true
rfi-p> 
rfi-p> hunted(X)
true
X=bnd[Anon371*5,$bird]
rfi-p> 
rfi-p> 
rfi-p> rx hunted(X : $bird) :- pet(Y), eats(Y, X).
rfi-p> 
rfi-p> az hunted(X : $bird) :- eats(Y : $pet, X).
rfi-p> 
rfi-p> hunted(tweety)
true
rfi-p> 
rfi-p> hunted(X)
true
X=bnd[Anon383*4,$bird]
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> %
rfi-p> % In the interpreter mode there is no check to see if a sort has been defined
rfi-p> % in the sort lattice: 
rfi-p> 
rfi-p> $otto
bnd[_1*0,$otto]
rfi-p> 
rfi-p> % In the interpreter mode, since "is" always returns the left-hand side, 
rfi-p> % this has to be expressed by two is-terms (as already seen above).
rfi-p> $pet is $fish
bnd[_2*0,$fish]
rfi-p> 
rfi-p> % But
rfi-p> X is $pet, X is $fish
bnd[X,$fish]
X=$fish
rfi-p> 
rfi-p> %
rfi-p> % Sorts in compiled RELFUN
rfi-p> %
rfi-p> emul
Collecting modules for the emulator:
sortbase workspace 
rfe-p> compile
rfe-p> 
rfe-p> $otto
unknown
rfe-p> 
rfe-p> $pet is $fish
$fish
rfe-p> $dog is $cat
unknown
rfe-p> 
rfe-p> eats(X,Y)
true
X=$cat
Y=$fish
rfe-p> m
true
X=tom
Y=$bird
rfe-p> m
unknown
rfe-p> 
rfe-p> $pet is dom[fido,fury,otto]
dom[fido,fury]
rfe-p> 
rfe-p> $pet is exc[]
$pet
rfe-p> $pet is exc[goldy]
dom[lassy,fido,fury,tom,garfield,tweety]
rfe-p> $mammal is exc[goldy, fury]
dom[lassy,fido,tom,garfield]
rfe-p> inter
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> 
rfi-p> 
rfi-p> 
rfi-p> %
rfi-p> %            DYNAMIC MODEL
rfi-p> % Only for use in the inter(preter) mode!
rfi-p> 
rfi-p> sortstyle dynamic
rfi-p> sortstyle
dynamic
rfi-p> 
rfi-p> destroy
rfi-p> destroy-sortbase
rfi-p> 
rfi-p> consult-sortbase "pet-base-sub"
Reading file "/home/rfm/RELFUN/RFM/demo/types/sorts/pet-base-sub.rfp"
rfi-p> 
rfi-p> % Loading the glb-calculation ...
rfi-p> consult glb
Reading file "/home/rfm/RELFUN/RFM/demo/types/sorts/glb.rfp"
rfi-p> l
constant-in-sort(Const,Sort) :- Sort(Const) & Const.
constant-in-sort(Const,Sort) :- 
         subsumes(Sort,Subsort) & constant-in-sort(Const,Subsort).
greatest-lower-bound(X,Y) :- & remove-subsumed-lbs(all-lbs(X,Y)).
lb(X,X) :- & X.
lb(X,Y) :- subsumes(X,Z) & lb(Z,Y).
lb(X,Y) :- subsumes(Y,Z) & lb(Z,X).
all-lbs(X,Y) :- & remove-duplicates(tupof(lb(X,Y))).
remove-subsumed-lbs(Lbs) :- & rsl(Lbs,[]).
rsl([],Rlbs) :- & Rlbs.
rsl([Lb|Lb-rest],Rlbs) :- & 
         rsl(rsl1(Lb,Lb-rest),tup(Lb|rsl1(Lb,Rlbs))).
rsl1(Lb,[]) :- & [].
rsl1(Lb,[Lb1|Rest]) :- subsumes+(Lb,Lb1) !& rsl1(Lb,Rest).
rsl1(Lb,[Lb1|Rest]) :- & tup(Lb1|rsl1(Lb,Rest)).
subsumes+(X,Y) :- subsumes(X,Y).
subsumes+(X,Y) :- subsumes(X,Z), subsumes+(Z,Y).
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> % The following commands do not work in the dynamic model:
rfi-p> compile-sortbase
error - running dynamic sort model
rfi-p> complete-taxonomy
error - running dynamic sort model
rfi-p> unique-glb
error - running dynamic sort model
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> %
rfi-p> % UNIFICATION OF SORTS
rfi-p> %
rfi-p> 
rfi-p> X is $pet, X is $dog
bnd[X,$dog]
X=$dog
rfi-p> 
rfi-p> X is $dog, X is $pet
bnd[X,$dog]
X=$dog
rfi-p> 
rfi-p> X is $dog, X is $cat
unknown
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> X is $dog, X is lassy
lassy
X=lassy
rfi-p> 
rfi-p> X is lassy, X is $dog
lassy
X=lassy
rfi-p> 
rfi-p> X is $dog, X is fury
unknown
rfi-p> 
rfi-p> X is fury, X is $dog
unknown
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> X is $dog, X is dom[lassy,fido]
bnd[X,dom[lassy,fido]]
X=dom[lassy,fido]
rfi-p> 
rfi-p> X is $dog, X is dom[lassy,fido, fifi]
bnd[X,dom[lassy,fido]]
X=dom[lassy,fido]
rfi-p> 
rfi-p> X is $dog, X is dom[lassy,fido, goldy]
bnd[X,dom[lassy,fido]]
X=dom[lassy,fido]
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> 
rfi-p> %
rfi-p> % USE OF SORTS
rfi-p> %
rfi-p> 
rfi-p> % Anonymous sorts
rfi-p> 
rfi-p> az eats($cat, $fish).
rfi-p> 
rfi-p> eats(tom, goldy)
true
rfi-p> 
rfi-p> 
rfi-p> eats(X, Y)
true
X=bnd[Anon702*1,$cat]
Y=bnd[Anon703*1,$fish]
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> 
rfi-p> % Named sorts
rfi-p> 
rfi-p> az young(tom).
rfi-p> az eats(X : $cat, $bird) :- young(X).
rfi-p> 
rfi-p> 
rfi-p> eats(X,Y)
true
X=bnd[Anon704*1,$cat]
Y=bnd[Anon705*1,$fish]
rfi-p> m
true
X=tom
Y=bnd[Anon707*1,$bird]
rfi-p> m
unknown
rfi-p> 
rfi-p> eats(tom,tweety)
true
rfi-p> 
rfi-p> eats(garfield,tweety)
unknown
rfi-p> 
rfi-p> pause()

relfun
rfi-p> bye
true
rfi-p> 
rfi-p> 
rfi-p> 
rfi-p> %
rfi-p> % Queries for the "sort base"
rfi-p> %
rfi-p> subsumes(mammal,X)
true
X=dog
rfi-p> m
true
X=horse
rfi-p> m
true
X=cat
rfi-p> m
unknown



Harold Boley (boley@informatik.uni-kl.de)