Re: [PRD] Issues to resolve before publication (et proposed resolutions)

Gary Hallmark wrote:
>>
>> #10. Section 3.4.1: matching theory. As I explain in [2], it is needed 
>> to take the semantics of datatypes into account. That is mentionned in 
>> an editor's note only, out of laziness rather than anything else (and 
>> also because it relates to the question of application-specific 
>> background knowledge).
>>
>> Options:
>> 1. keep the editor's note as it is;
>> 2. add a paragraph in the text re how it takes into account the
>> semantics of data types etc, and leave an editor's note saying that this
>> might be extended to take application-specific theories into account
>> (such as app-specific object models etc).
>>
>> I propose that we go by option 1 for the FPWD.
> 
> I wouldn't even talk about application-specific theories until we first 
> have defined what matching means for the datatypes and builtins in DTB.

What matching means is well-defined and nothing specific to PRD: it is 
only that I did not specify all the details in the draft, out of 
laziness (and because it is such a well-establised definition).

And matching is usually defined wrt an arbitrary matching theory (well, 
maybe not all definitions call it that way: if you have a prefered 
definition taht use a different termonilogy, I have nothing against 
changing).

The way out, here, is maybe to copy one standard definition of pattern 
matching out of a text book, so that it is clear that RIF is just using 
the standard definition, including wrt matching theories?

Cheers,

Christian