case statement semantic in kernel language

[Marko Zerdin]

Dear Peter,

thank you for your prompt and comprehensive answer. Unfortunately, I 
must've been unsuccessful when trying to get my point across, so I'm 
going to have to try again.

On page 67, it says the following when explaining the semantics of the 
case statement (I'm quoting just the relevant part)::
<snip>
If the activation condition is true (E(<x>) is determined), then do the 
following actions:
* If the label of E(<x>) is <lit> and its arity is [<feat1> ... 
<featn>], then push (<s1>, 
E+{<x1>->E(<x>).<feat1>,...,<xn>->E(<x>).<featn>}) on the stack.
* Otherwise, push (<s2>, E) on the stack.
</snip>
Based on this semantic, the match is determined solely based on the 
record label and arity - as soon as those match, the alternative is 
chosen. However, assume for a second that we are matching rec(a:1) 
against rec(a:2). According to the described semantic, we have the 
following chain of events:
- Activation condition is obviously true, so the matching can proceed.
- Both the label and arity match. Therefore, the match was found and the 
new entry is added on the stack.
The unfortunate fact in this case however is that we don't actually have 
a match. When the new environment is created, unification failure should 
occur because the binding 1->2 obviously won't be welcome in the store. 
I don't think this case is actually addressed in the semantic above. How 
is this resolved? What happens next?

I don't want to presume that I thought of everything, so please let me 
know if there is some simple fact that I'm missing in my reasoning.

Kind regards,

Marko.

Peter Van Roy wrote:

> Dear Marko,
>
> I think you are confusing the 'full' case statement with the 'kernel' 
> case statement.
> The 'kernel' case statement matches only a single record; its 
> semantics is given on
> page 67.  The 'full' case statement can have nested records (like in 
> exercise 6 on
> page 108); on pages 82-83 it is explained how to translate full case 
> statements into
> kernel case statements.
>
> The definition of 'determined' is given in several places.  Briefly, a 
> variable is
> determined if it is bound to a number, procedure, or record.  A formal 
> definition
> is given on page 791.  From this definition it is clear that the 
> record's arguments
> can be unbound variables.
>
> So I do think that the kernel language is completely formally defined 
> in the book,
> and certainly in sufficient detail to be implemented independently!
>
> Best regards,
>
> Peter
>
>
>
> Marko Zerdin wrote:
>
>> Hello.
>>
>> First, let me thank Peter and Seif for a great book, and all Oz gurus 
>> for this most amazing language that you created. Second, I want to 
>> apologize for posting this question here. It is strictly the book 
>> question, but I wasn't certain where else to post it.
>>
>> In CTMCP, I've noticed a puzzling incompleteness of the case 
>> statement semantic (on page 67) while trying to solve some of the 
>> exercises. I'm sure I'm missing something somewhere along the way, so 
>> I would appreciate it if somebody could follow through with my 
>> reasoning and point to me what's wrong with it.
>>
>> First, the book says that the activation condition is true if the 
>> test expression is determined, but doesn't specify what exactly 
>> "determined" is supposed to mean in this case. Based on the observed 
>> semantic of the case statement (clearly demonstrated by exercise 
>> 2.6),  the expression does not need to be fully determined for the 
>> option to be chosen (second case), but knowing only the record label 
>> and arity is also not enough, which is what would follow from 
>> semantic description. So what exactly is the activation condition?
>>
>> Second, according to the semantic on page 67, the alternative to be 
>> taken is decided solely based on both expressions' record label and 
>> arity, which is quite obviously not at all what is actually 
>> happening. Let us assume that the label and arity both match, and 
>> therefore the alternative is chosen. The interpreter is supposed to 
>> create a new environment now, binding the values of all features in 
>> both records. A few fundamental questions remain unanswered: What 
>> happens at the point of creation of the new environment if one of the 
>> bindings fails? As an alternative answer to the previous question, 
>> how exactly and when are the bindings performed, and how exactly do 
>> they influence the alternative selections process? The alternative is 
>> surely not determined solely based on record label and arity, so how 
>> exactly is it determined?
>>
>> I understood from the book that the kernel language definition is 
>> supposed to be complete and should be simple enough to be implemented 
>> independently for pedagogical purposes. However, I'm quite certain 
>> that no such implementation could be done based solely on the 
>> information that can be found in the book. Therefore, I would really 
>> appreciate if you could give a full semantic of the case statement 
>> upon which a determined and compatible implementation of the kernel 
>> language could be based.
>>
>> Kind regards,
>>
>> Marko Zerdin.
>
>
>
>
>