Re: How core is Core?

>    "why do we continue to talk about all dialects extending Core and 
> everyone implementing Core when that seems unlikely given that Core has 
> term unification? what does that imply for the extensibility mechanism, 
> do we need profiles or something?"

I think of the decision about what goes into Core or other dialects as
essentially a marketing question.  Does that seem right?

RIF software doesn't have to know what's in Core or any other dialect,
except when constructing good error messages.  Implementors decide which
components they will implement, and that's what the software knows
about.

I'd like to see us defining and characterizing components, mostly
separate from whether they will be in Core or not.  Maybe we'll focus
more on the ones for Core, but I think we'll really just each focus on
the ones we each want, whether they end up in Core or not.

It may be that we'll do the core-or-not-core labeling much later in the
process.  We can, I think, go to Last Call and Candidate Recommendation
with components published as "as risk" for Core, saying we'll figure out
later, based on implementation experience, whether they belong in Core
or not.  Basically, we'll include them in Core unless someone ends up
really finding them too hard to implement.

Bringing this back to lists.  Am I understanding correctly that
transparent (cons-cell) lists are trivial to implement given term
unification?  And term unification is synonymous with logic functions?
And term unification is something "at risk" for Core -- some folks are
unsure about being able to implement it.

So, this discussion seems to revolve around several components:

   * Logic Functions.  (also known, loosely, as "terms".)  Kind of in
     the syntax as "Uniterm", but Uniterm is overloaded.  (This may be a
     reason to go back and split apart Uniterm.)

   * Evaluable Functions.  Syntactically, these might look like Logic
     Functions, but probably should not, so we can have them be a
     separate component.

   * An evaluator predicate, "is" in prolog, which lets you bind a
     variable to an evaluable expression, or test a constant against the
     value of an evaluable expression.   It does not let you solve
     constraint expressions, like "?x + 4 is (?x - 2) * 5".

   * A true equality predicate.

Does someone have a purely-logical semantics for the handling of
evaluables?  Does CLP give that?  My naive best guess is to treat
evaluable functions and the evaluator as like true logic functions and
equality but with some kind of incompleteness in reasoning, or as being
identical whenever the evaluable form is allowed.  ("Allowed" may be
tricky to define; it's not just syntax, since it has to do with variable
bindings.)

Anyway, it seems like could write "x is three plus five" as:

  a)  eval(?x, eval_sum(3,5))
  b)  equal(?x, true_sum(3,5))

and it would mean the same thing.  Something like "eight is y plus five"
could only be written in one way:

  a)  eval(8, eval_sum(?y,5))    <==   ERROR
  b)  equal(8, true_sum(?y,5))
  
So, eval and equal are identical, and eval_sum and true_sum are
identical, for all cases where eval and eval_sum are allowed.

I don't think the "b" forms work in a logic programming world, with the
unique names assumption.   In prolog, you can absolutely say "X=3+5", it
just unifies X with the term "+(3,5)", which is by definition different
from the number eight.   At least I think the problem here is UNA.

     -- Sandro

Received on Monday, 2 July 2007 14:27:39 UTC