- From: Michael Kifer <kifer@cs.sunysb.edu>
- Date: Wed, 20 Dec 2006 07:22:13 -0500
- To: =?ISO-8859-1?Q?Hassan_A=EFt-Kaci?= <hak@ilog.com>
- Cc: Gary Hallmark <gary.hallmark@oracle.com>, Christian de Sainte Marie <csma@ilog.fr>, W3C RIF WG <public-rif-wg@w3.org>
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 > > > > >
Received on Wednesday, 20 December 2006 12:25:20 UTC