[PRD] Assert and separating syntax and semantics cleanly (Was: Re: [PRD] PRD Review By Example)

All,

Gary Hallmark wrote: 
> 
> Surely you agree we must handle the initial fact p:A(0)
> 
> [...]
>
> We need to align with the Core syntax.  I think you are right, they can 
> be handled in the semantics as rules that are always true.
> 
> [...]
>
> Actually, I think it boils down to defining the syntax for the initial 
> facts.  As usual, I prefer maximum overlap with BLD/Core.

I believe that we agree on how the assertion of p:A(0) should be handled, but I wonder if there might not be some confusion between the semantics and the (concrete) syntax, especially considering the modifications Gary made in the definitions of an atomic action (sect. 3.1.1) and an action block (sect. 3.1.3).

In PR languages, and, accordingly, in the semantics of PRD, an assertion is an action, no doubt about that; and, followingly, a sequence of assertions is, in PRD-ese, an action_block.

Gary is right and the initial definition of the Assert action, in sect. 3.1.1, was confusing, since the asserted fact is not an atomic action: it is a fact.

But I think that the correction that Gary proposes is confusing as well, because, even if we choose to use the syntax of the asserted fact itself to denote the assertion, the assertion is still, in the semantics of PRD, an atomic action; and a sequence of assertion is still an action block in the semantics of PRD, even if we choose to use to represent it with the same syntax as for the conjunction of the asserted facts.

And so they should be defined, at the abstract syntax level.

What I propose is:

1. to keep the same abstract syntax as before Gary's modification, that is, to have any single assertion, retraction etc be defined as atomic actions (or whatever other name that the group may prefer), and have any sequence of actions be defined as an action block, so that the semantics of atomic actions, and of action blocks, resp., can be specified uniformally;

And:

2. to add wording to the effect that, based on the design principle that "same semantics <=> same syntax", the syntax for the assertion of a single fact and the syntax for an action block that contains only assertions will be the same as in Core and BLD, that is, respectively, that of the single fact itself and that of a conjunction of the asserted facts.

NB: I did not include the new "Bind" action in this discussion, because I am not sure that I understand its semantic status yet. I have to sleep on Gary's proposal first, and allow it to percolate in my brain :-)

Cheers,

Christian

Received on Friday, 24 October 2008 15:31:47 UTC