Re: model theory of error

> Michael Kifer wrote:
> > Christian de Sainte Marie wrote:
> >> Michael Kifer wrote:
> >>
> >>> How do you define an error independently of the evaluation strategy?
> >>> What does it mean to say that "RIF does not mandate any 
> >>> specific behaviour"? What is "behavior" exactly, if RIF (at least BLD) does
> >>> not define any evaluation strategy?
> >> Let me try without using the words "error" or "behaviour"...
> >>
> >> An evaluated function is defined over a domain, and it is undefined 
> >> outside of that domain.
> >>
> >> If a function is used in a rule, we assume that any party that evaluates 
> >> that rule knows the domain of the function, whether it is specified 
> >> within RIF (builtin function) or not (application-specific).
> >>
> >> So, anybody who may have to evaluate the function knows where it is 
> >> defined and where it is not, and is able to check, before evaluating it, 
> >> whether the arguments are in the domain, and the function defined, or not.
> >>
> >> For the strict purpose of rule interchange, RIF needs to make sure that 
> >> all users have the same understanding of the rule - that is, draw the 
> >> same inferences - where the function is defined.
> >>
> >> But does RIF need to guarantee anything beyond the common understanding 
> >> that the function is undefined, where it is undefined? Except, maybe, 
> >> that such cases must not be handled silently.
> >>
> >> The same question applies wrt evaluated predicates.
> >>
> >> Is that any clearer? And, if yes, does it make sense? And, if no, at 
> >> what step did I take the wrong turn?
> > 
> > 
> > It is clear like mud. You still fail to understand that we are supposed to
> > give formal semantics: model-theoretic, denotational, operational in that
> > order. We decided that for BLD we will give a model-theoretic semantics. If
> > you want to redefine the mission - fine.  But make sure you ask for another
> > 12 months of extension.
> 
> I may be misunderstanding Christian but I take him to be trying to work 
> from an intuition about the useful operational semantics for rule 
> interchange backwards to what that means for the model theory.
> 
> In pragmatic terms if type errors are "handled silently" they are a 
> lurking source of problems. For example, an error in a translator which 
> led to a mis-application of a builtin will be detected more quickly if 
> consumers of the translation see the equivalent of an exception rather 
> than seeing the rule set execute but giving unexpected values only on 
> appropriate test cases.
> 
> It seems to me that your option (b) with the additional E truth value 
> corresponds to an operational semantics in which errors will be 
> propagated outwards and underlying bugs in translators (or rule sets) 
> will be discovered a little more quickly.

The truth theory of error is of no use to the compiler.
And in the most general form the problem of whether a variable can be bound
to an out-of-the-domain value is undecidable. Furthermore, the problem
itself depends on the evaluation strategy, and for the bottom-up evaluation
it likely does not make sense at all.

> Other things being equal that suggests we should choose (b).
> 
> You've clearly stated that other things are not equal and that (b) is an 
> added complication that will eat yet more of our limited remaining time.
> So we have to make a judgement about the cost/benefit ratio.

Yes.

> I think you could argue that it is up to the source languages to help 
> find the bugs in rule sets, and that translators can be tested with 
> sufficiently comprehensive test suites and so error handling behaviour 
> is not so important for an interchange language.

> I personally would prefer (b) but I'm not volunteering to do the hard 
> work and so am prepared to accept your judgement that the cost of 
> formally checking (b) is too high.

I agree that, in principle, (b) would be preferable. But I am afraid that
we do not have the time to go after that option.


	--michael  


> Dave
> -- 
> Hewlett-Packard Limited
> Registered Office: Cain Road, Bracknell, Berks RG12 1HN
> Registered No: 690597 England
>

Received on Thursday, 10 January 2008 14:45:40 UTC