next up previous contents
Next: C Builtin-Sorts Dialog Up: RELFUN Guide: Programming with Previous: A Tutorial Dialog

B Type-System Dialog

 

rfi-p> exec typin

relfun
rfi-p> %                    An Introduction to RELFUN Types
rfi-p> %                    ===============================
rfi-p> 
rfi-p> %  Harold Boley       -       Kaiserslautern       -        9-Jul-96
rfi-p> 
rfi-p> 
rfi-p> % The notion of types in RELFUN encompasses both
rfi-p> % groups and sorts.
rfi-p> 
rfi-p> % Groups are finite domains (dom terms),
rfi-p> % specifying permitted constants ('positive' individuals),
rfi-p> % or finite exclusions (exc terms),
rfi-p> % specifying forbidden constants ('negative' individuals).
rfi-p> 
rfi-p> % Sorts reuse certain unary predicates as types (with a "$"-prefix).
rfi-p> % Some sorts may be user-defined, employing RELFUN's sortbase;
rfi-p> % other sorts are builtin, i.e. derived from atom subpredicates.
rfi-p> 
rfi-p> % Types are first-class citizens, which can be employed anonymously or
rfi-p> % as occurrence bindings of logic variables (as bnd/":"-term rhs's).
rfi-p> 
rfi-p> % Orthogonally, types can appear in normal (hn/ft) clauses
rfi-p> % or in signature (sg) clauses.
rfi-p> 
rfi-p> destroy
rfi-p> destroy-sortbase
rfi-p> 
rfi-p> % Groups
rfi-p> % ------
rfi-p> 
rfi-p> % Finite domains
rfi-p> % ..............
rfi-p> 
rfi-p> % We might enumerate the cocktails drunk by Mary:
rfi-p> 
rfi-p> az drinks(mary,pina-colada).
rfi-p> az drinks(mary,vodka-lemon).
rfi-p> az drinks(mary,orange-flip).
rfi-p> 
rfi-p> % This could be queried using 'more' requests,
rfi-p> 
rfi-p> drinks(mary,What)
true
What=pina-colada
rfi-p> more
true
What=vodka-lemon
rfi-p> more
true
What=orange-flip
rfi-p> more
unknown
rfi-p> 
rfi-p> % or the 'tupof' primitive:
rfi-p> 
rfi-p> tupof(drinks(mary,What),What)
[pina-colada,vodka-lemon,orange-flip]
rfi-p> 
rfi-p> destroy
rfi-p> 
rfi-p> % Alternatively we may employ a finite domain:
rfi-p> 
rfi-p> az drinks(mary,dom[pina-colada,vodka-lemon,orange-flip]).
rfi-p> 
rfi-p> % Now a 'closed' solution is obtained by an ordinary query
rfi-p> % (the 'bnd' context around a 'dom' etc. can be ignored here,
rfi-p> % but will be explained in the part on occurrence bindings):
rfi-p> 
rfi-p> drinks(mary,What)
true
What=bnd[Anon1*1,dom[pina-colada,vodka-lemon,orange-flip]]
rfi-p> 
rfi-p> % Success is obtained by a query with a domain constant:
rfi-p> 
rfi-p> drinks(mary,orange-flip)
true
rfi-p> 
rfi-p> % Failure is obtained by a query with any non-domain constant:
rfi-p> 
rfi-p> drinks(mary,whisky-sour)
unknown
rfi-p> 
rfi-p> % A finite domain can also be used in the query,
rfi-p> % where domain unification performs intersection:
rfi-p> 
rfi-p> drinks(mary,dom[pina-colada,vodka-lemon,banana-flip])
true
rfi-p> 
rfi-p> % We can see dom intersection results by giving them a name:
rfi-p> 
rfi-p> drinks(mary,What), dom[pina-colada,vodka-lemon,banana-flip] is What
bnd[_1*0,dom[pina-colada,vodka-lemon]]
What=bnd[_1*0,dom[pina-colada,vodka-lemon]]
rfi-p> 
rfi-p> % Another intersection returns a singleton domain, dom[pina-colada],
rfi-p> % which reduces to its only element, pina-colada:
rfi-p> 
rfi-p> drinks(mary,What), dom[pina-colada,banana-flip] is What
pina-colada
What=pina-colada
rfi-p> 
rfi-p> 
rfi-p> % Finite exclusions
rfi-p> % .................
rfi-p> 
rfi-p> % Because we have no negated facts we cannot enumerate
rfi-p> % the cocktails not drunk by John
rfi-p> 
rfi-p> % But we may employ a finite exclusion for this purpose:
rfi-p> az drinks(john,exc[whisky-sour,vodka-lemon]).
rfi-p> 
rfi-p> % Now a 'negative' solution is obtained by an ordinary query:
rfi-p> 
rfi-p> drinks(john,What)
true
What=bnd[Anon8*1,exc[whisky-sour,vodka-lemon]]
rfi-p> 
rfi-p> % Success is obtained by a query with any non-excluded constant:
rfi-p> 
rfi-p> drinks(john,orange-flip)
true
rfi-p> 
rfi-p> % Failure is obtained by a query with an excluded constant:
rfi-p> 
rfi-p> drinks(john,whisky-sour)
unknown
rfi-p> 
rfi-p> % The unification of a domain and an exclusion subtracts the
rfi-p> % exc elements from the dom elements (failing if none is left):
rfi-p> 
rfi-p> drinks(john,dom[pina-colada,orange-flip])
true
rfi-p> drinks(john,What), dom[pina-colada,orange-flip] is What
bnd[_1*0,dom[pina-colada,orange-flip]]
What=bnd[_1*0,dom[pina-colada,orange-flip]]
rfi-p> 
rfi-p> drinks(john,dom[pina-colada,whisky-sour])
true
rfi-p> drinks(john,What), dom[pina-colada,whisky-sour] is What
pina-colada
What=pina-colada
rfi-p> 
rfi-p> drinks(john,dom[whisky-sour,vodka-lemon])
unknown
rfi-p> drinks(john,What), dom[whisky-sour,vodka-lemon] is What
unknown
rfi-p> 
rfi-p> % What John and Mary can drink together is obtained thus:
rfi-p> 
rfi-p> drinks(mary,What), drinks(john,What)
true
What=bnd[Anon27*2,dom[orange-flip,pina-colada]]
rfi-p> 
rfi-p> destroy
rfi-p> 
rfi-p> 
rfi-p> % Sorts
rfi-p> % -----
rfi-p> 
rfi-p> % User-defined sorts
rfi-p> % ..................
rfi-p> 
rfi-p> % If some 'positive' group of individuals is worth a permanent name
rfi-p> % we can define a unary predicate for it, using facts in the sortbase.
rfi-p> % For example, the cocktails drunk by Mary may be called 'lightmix'.
rfi-p> % A sortbase-defined predicate 'pred' is then usable as the sort '$pred'.
rfi-p> 
rfi-p> mcd sortbase
Module:  sortbase
Context: 
rfi-p> 
rfi-p> % A tiny sort lattice, defined by two subsumes 'higher-order' facts:
rfi-p> 
rfi-p> az subsumes(cocktail,lightmix).
rfi-p> az subsumes(cocktail,heavymix).
rfi-p> 
rfi-p> % Two sort extensions, as facts applying predicates to individuals:
rfi-p> 
rfi-p> az lightmix(pina-colada).
rfi-p> az lightmix(vodka-lemon).
rfi-p> az lightmix(orange-flip).
rfi-p> 
rfi-p> az heavymix(whisky-sour).
rfi-p> az heavymix("bloody-mary, strong").
rfi-p> 
rfi-p> compile-sortbase
rfi-p> 
rfi-p> mcd
Module:  workspace
Context: 
rfi-p> 
rfi-p> % The unification of two such user-defined sorts returns their glb:
rfi-p> 
rfi-p> $lightmix is $cocktail
bnd[_2*0,$lightmix]
rfi-p> $heavymix is $cocktail
bnd[_2*0,$heavymix]
rfi-p> $lightmix is $heavymix
unknown
rfi-p> 
rfi-p> % The sort $lightmix abbreviates our domain dom[pina-colada,...]:
rfi-p> 
rfi-p> az drinks(mary,$lightmix).
rfi-p> 
rfi-p> % Again a 'closed' solution is obtained by the ordinary query
rfi-p> 
rfi-p> drinks(mary,What)
true
What=bnd[Anon28*1,$lightmix]
rfi-p> 
rfi-p> % success is obtained by a query with a constant in the sort,
rfi-p> 
rfi-p> drinks(mary,orange-flip)
true
rfi-p> 
rfi-p> % and failure is obtained by a query with any constant not in the sort,
rfi-p> 
rfi-p> drinks(mary,whisky-sour)
unknown
rfi-p> 
rfi-p> % Again a finite domain can be used in the query,
rfi-p> % where sort-domain unification performs (extensionalized) intersection:
rfi-p> 
rfi-p> drinks(mary,dom[pina-colada,vodka-lemon,banana-flip])
true
rfi-p> 
rfi-p> % We can see dom intersection results by giving them a name:
rfi-p> 
rfi-p> drinks(mary,What), dom[pina-colada,vodka-lemon,banana-flip] is What
bnd[_1*0,dom[pina-colada,vodka-lemon]]
What=bnd[_1*0,dom[pina-colada,vodka-lemon]]
rfi-p> 
rfi-p> % A sort can also be used in the query:
rfi-p> 
rfi-p> az drinks(fred,vodka-lemon).
rfi-p> drinks(fred,$lightmix)
true
rfi-p> 
rfi-p> 
rfi-p> % Builtin sorts
rfi-p> % .............
rfi-p> 
rfi-p> % The builtin atom subpredicates such as stringp may also
rfi-p> % be used (with a "$"-prefix) as sorts:
rfi-p> 
rfi-p> az drinks(sue,"Barbara's special green-mix").
rfi-p> drinks(sue,$atom)
true
rfi-p> drinks(sue,$numberp)
unknown
rfi-p> drinks(sue,$stringp)
true
rfi-p> 
rfi-p> % A builtin sort may be unified with a finite domain,
rfi-p> % performing (generalized) intersection:
rfi-p> 
rfi-p> az drinks(jack,dom["Juan's drink",honey-liqueur,"Boston ward 8"]).
rfi-p> drinks(jack,What), $stringp is What
bnd[_1*0,dom["Juan's drink","Boston ward 8"]]
What=bnd[_1*0,dom["Juan's drink","Boston ward 8"]]
rfi-p> 
rfi-p> % A builtin sort may also be unified with a user-defined sort:
rfi-p> 
rfi-p> $stringp is $heavymix
"bloody-mary, strong"
rfi-p> $symbolp is $heavymix
whisky-sour
rfi-p> $numberp is $heavymix
unknown
rfi-p> 
rfi-p> 
rfi-p> % Occurrence bindings
rfi-p> % -------------------
rfi-p> 
rfi-p> % While the previous types were employed anonymously, they can also be
rfi-p> % associated to logic variables via occurrence bindings (bnd/":"-terms).
rfi-p> % This permits typed variables, forcing group or sort restrictions in a
rfi-p> % rule head, with premises using these variables in arbitrary goals.
rfi-p> 
rfi-p> % Domain binding:
rfi-p> 
rfi-p> az orders(laura,whisky-sour).
rfi-p> 
rfi-p> az drinks(peter,bnd[M,dom[whisky-sour,"bloody-mary, strong"]]) :-
                                                             orders(S,M).
rfi-p> drinks(peter,What)
true
What=whisky-sour
rfi-p> 
rfi-p> rx drinks(peter,bnd[M,dom[whisky-sour,"bloody-mary, strong"]]) :-
                                                             orders(S,M).
rfi-p> 
rfi-p> % Exclusion binding:
rfi-p> 
rfi-p> az drinks(steve,bnd[M,exc[whisky-sour,vodka-lemon]]) :- orders(S,M).
rfi-p> drinks(steve,What)
unknown
rfi-p> 
rfi-p> % User-defined sort binding:
rfi-p> 
rfi-p> az drinks(peter,bnd[M,$heavymix]) :- orders(S,M).
rfi-p> drinks(peter,What)
true
What=whisky-sour
rfi-p> 
rfi-p> % Builtin sort binding:
rfi-p> 
rfi-p> az drinks(adrian,bnd[M,$atom]) :- orders(S,M).
rfi-p> drinks(adrian,What)
true
What=whisky-sour
rfi-p> 
rfi-p> % For types (as seen in previous 'What' queries) occurrence bindings are
rfi-p> % also generated internally (by 'deanonymization' through bnd contexts).
rfi-p> % Generally, deanonymization causes correct unification failures for
rfi-p> % inconsistent uses of (list- or structure-)embedded anonymous variables,
rfi-p> % (dom or exc) groups, and (user-defined or builtin) sorts:
rfi-p> 
rfi-p> mcd sortbase
Module:  sortbase
Context: 
rfi-p> 
rfi-p> az person(steve).
rfi-p> az person(john).
rfi-p> az person(mary).
rfi-p> 
rfi-p> compile-sortbase
rfi-p> mcd
Module:  workspace
Context: 
rfi-p> 
rfi-p> spy
rfi-p> 
rfi-p> X is [_], [mary] is X
and(X is [_1*0],[mary] is X)
and([mary] is [_1*0])
and([mary])
[mary]
X=[mary]
rfi-p> X is [_], [mary] is X, [john] is X
and(X is [_1*0],[mary] is X,[john] is X)
and([mary] is [_1*0],[john] is [_1*0])
and([john] is [mary])
unknown
rfi-p> 
rfi-p> X is [dom[john,mary]], [mary] is X
and(X is [bnd[_1*0,dom[john,mary]]],[mary] is X)
and([mary] is [bnd[_1*0,dom[john,mary]]])
and([mary])
[mary]
X=[mary]
rfi-p> X is [dom[john,mary]], [mary] is X, [john] is X
and(X is [bnd[_1*0,dom[john,mary]]],[mary] is X,[john] is X)
and([mary] is [bnd[_1*0,dom[john,mary]]],
    [john] is [bnd[_1*0,dom[john,mary]]])
and([john] is [bnd[mary,dom[john,mary]]])
unknown
rfi-p> 
rfi-p> X is [exc[fred]], [mary] is X
and(X is [bnd[_1*0,exc[fred]]],[mary] is X)
and([mary] is [bnd[_1*0,exc[fred]]])
and([mary])
[mary]
X=[mary]
rfi-p> X is [exc[fred]], [mary] is X, [john] is X
and(X is [bnd[_1*0,exc[fred]]],[mary] is X,[john] is X)
and([mary] is [bnd[_1*0,exc[fred]]],[john] is [bnd[_1*0,exc[fred]]])
and([john] is [bnd[mary,exc[fred]]])
unknown
rfi-p> 
rfi-p> X is [$person], [mary] is X
and(X is [bnd[_1*0,$person]],[mary] is X)
and([mary] is [bnd[_1*0,$person]])
and([mary])
[mary]
X=[mary]
rfi-p> X is [$person], [mary] is X, [john] is X
and(X is [bnd[_1*0,$person]],[mary] is X,[john] is X)
and([mary] is [bnd[_1*0,$person]],[john] is [bnd[_1*0,$person]])
and([john] is [bnd[mary,$person]])
unknown
rfi-p> 
rfi-p> X is [$symbolp], [mary] is X
and(X is [bnd[_1*0,$symbolp]],[mary] is X)
and([mary] is [bnd[_1*0,$symbolp]])
and([mary])
[mary]
X=[mary]
rfi-p> X is [$symbolp], [mary] is X, [john] is X
and(X is [bnd[_1*0,$symbolp]],[mary] is X,[john] is X)
and([mary] is [bnd[_1*0,$symbolp]],[john] is [bnd[_1*0,$symbolp]])
and([john] is [bnd[mary,$symbolp]])
unknown
rfi-p> 
rfi-p> nospy
rfi-p> 
rfi-p> 
rfi-p> % Signatures
rfi-p> % ----------
rfi-p> 
rfi-p> % A signature (sg) clause restricts all clauses of a procedure to
rfi-p> % arguments unifying with the sg arguments. Besides constants, variables,
rfi-p> % and structures, the sg arguments can be types.
rfi-p> 
rfi-p> % Assuming, everybody drinks soft drinks,
rfi-p> 
rfi-p> az drinks(X,soft-drink).
rfi-p> 
rfi-p> % we may obtain unexpected results:
rfi-p> 
rfi-p> drinks(steve,What)
true
What=soft-drink
rfi-p> drinks(tweety,What)
true
What=soft-drink
rfi-p> 
rfi-p> % However, with a drinks signature clause we can prevent this by
rfi-p> % restricting the first argument to be a person:
rfi-p> 
rfi-p> style lisp
rfi-l> 
rfi-l> a0 (sg (drinks $person _something))
rfi-l> 
rfi-l> style prolog
rfi-p> 
rfi-p> % Now the bird Tweety no longer drinks soft drinks:
rfi-p> 
rfi-p> drinks(steve,What)
true
What=soft-drink
rfi-p> drinks(tweety,What)
unknown



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