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.

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.

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.

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

Received on Thursday, 10 January 2008 09:40:29 UTC