Re: [TED] Action-188, ISSUE: production rule systems have "difficulty" with recursive rules in RIF Core

What is the model theory for <:? Remember that we decided to have a model
theory for the core.


	--michael  


> 
> Gary Hallmark wrote:
> 
> > ...
> > BTW, is "novar" a builtin, a constraint, or could never be in CORE 
> > because it is too operational?
> 
> It is a metapredicate that can be expressed as a constraint (e.g., in
> OSF, it is "X <: s" where X is a variable and s a minimal non-singleton
> sort symbol; the semantics of  "<:" is "strictly subsumes"; e.g., in the
> unsorted case such as Prolog, "nonvar(X)" is simply "X <: \top").
> 
> As you remarked during this past meeting, constraints are the perfect
> abstraction mechanism to express builtins as long as order of resolution
> does not matter. Even when order does matter, the discrimination between
> what is an atom and what is a constraint can be exploited without a priori
> "moving all constraints to one side" explicitly. (The "moving to one side"
> is just symbolic to ease formal notation expressing the constrained
> resolution rule as simply as posssible). Indeed, if important to the
> operational semantics, the original order of subgoals in the RHS may be
> preserved and the constrained resolution process made to process the
> constraints in the order they are given (if such is needed to preserve
> some order-sensitive operational semantics or effect).
> 
> -hak
> -- 
> Hassan Aït-Kaci
> ILOG, Inc. - Product Division R&D
> tel/fax: +1 (604) 930-5603 - email: hak @ ilog . com
> 
> 
> 
> 
>