[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Comments on V.096 comments [350 lines]
Dear friends,
AT> 1. p. 6, just before sect. 2.1.1:
AT>
AT> We permit overloading of identifiers across various kinds of
entities:
AT> fine. But what about variables, which are not mentioned here?
AT> Overloading variables and constants might lead to strange
AT> ambiguities in the syntax of terms, so maybe they should be kept
AT> separate.
PDM>If parsing is context-free, one (presumably) can't see any
PDM>difference between constants and variables, they are just IDs.
PDM>If parsing is context-sensitive, one can see whether an ID is a
PDM>(possibly-overloaded) constant or a (non-overloaded) variable; if
PDM>both are allowed by the context, the enclosing atomic formula is
PDM>surely illegal in any case.
Kolyang, in cooperation with me, has developed a context-free parser for
CASL. As Peter says, variables and constants are just IDs at this level.
To distinguish between variables and constants is a task of static
semantic analysis, in particular of the overload resolution algorithm.
I see no problem here, if we take the convention that a variable
is not equivalent to a constant of the same name (I refer to the
equivalence relation defined in section 4.2).
AT> 2. sect. 2.1.2 and elsewhere.
AT>
AT> I must admit, i do not like too much the changes related to the
AT> introduction of constants as separate things. I think that what was
AT> here before, forcing the application of a zero-ary function to the
AT> empty list of arguments, was okay and was quite readable (and any
AT> potential inconveniences might be resolved at the level of a
AT> concrete syntax then). Moreover, this was quite uniform throughout
AT> the language, and everything (e.g. partiality) was nicely symmetric.
PDM>Agreed!
AT> Okay: I also buy some of Bernd's arguments about the
AT> possible future interaction with a higher-order extension.
PDM>This was the ONLY reason that I switched style i v0.96: I couldn't
PDM>see how to give a smooth extension of the AS from CASL to HO-CASL with
PDM>v0.95 AS.
AT> However, if constants are to be treated separately in the language,
AT> differently than functions, then I think we should do this
AT> systematically throughout the entire formalism in a "proper" way.
AT> Otherwise we loose some sense of uniformity of the language.
PDM>Agreed. Although one might also argue that constants have just as
PDM>much right to be uniform with variables as with functions, perhaps?
A higher-order version which would keep the symmetry between
total and partial functions would be:
CONST-DECL ::= const-decl NAME TYPE
TYPE ::= BASIC-TYPE | TOTAL-CON-TYPE | PARTIAL-CON-TYPE |
TOTAL-FUN-TYPE | PARTIAL-FUN-TYPE
BASIC-TYPE ::= basic-type SORT
TOTAL-CON-TYPE ::= total-con-type TYPE
PARTIAL-CON-TYPE ::= partial-con-type TYPE
TOTAL-FUN-TYPE ::= total-fun-type TYPE+ TYPE
PARTIAL-FUN-TYPE ::= partial-fun-type TYPE+ TYPE
[Maura suggested (last Friday) removing the partial/total distinction
from the TYPE and putting it directly in the CON/FUN-DECL. Her point
was that the distinction between partial and total functions is
irrelevant when using type qualification to resolve overloading. This
idea might help to simplify the syntax proposed above. Please
consider the extent to which the totality should be a part of
higher-order function types; would it really affect type-checking? If
not, please let's remove it! Bernd, re your concrete syntax proposal:
you could still use two different kinds of arrows in the concrete
syntax for function types, they would just map to the same bit of
abstract syntax. --PDM]
Since the higher-order extension has a richer set of types,
usually ONLY constant values are declared at the level
of BASIC-ITEMs, since the type of the constant may be itself
functional. Otherwise, we would have a strange difference
between constants of type s1 -> s2 and functions from f1 to f2,
This difference is present in some algebraic higher-order approaches
but I do not like it very much.
So the issue of constant declaration has not so much to do
with partial versus total constant, but with the question
which things can be declared a the outmost level (constants
or functions?). And the higher-order extension works nicer
if we allow ONLY constants at the outermost level.
Thus, inside we can surely treat constants as parameterless
functions and get essentially the same, but are more
uniform with the rest of the language (as Andrzej wants):
CONST-DECL ::= const-decl NAME TYPE
TYPE ::= BASIC-TYPE | TOTAL-FUN-TYPE | PARTIAL-FUN-TYPE
BASIC-TYPE ::= basic-type SORT
TOTAL-FUN-TYPE ::= total-fun-type TYPE* TYPE
PARTIAL-FUN-TYPE ::= partial-fun-type TYPE* TYPE
Now from this we can derive the first-order restriction
as follows:
CONST-DECL ::= const-decl NAME TYPE
TYPE ::= BASIC-TYPE | TOTAL-FUN-TYPE | PARTIAL-FUN-TYPE
BASIC-TYPE ::= basic-type SORT
TOTAL-FUN-TYPE ::= total-fun-type SORT* SORT
PARTIAL-FUN-TYPE ::= partial-fun-type SORT* SORT
and since
basic-type s
and
total-fun-type s
are interchangeable, we can omit either BASIC-TYPEs or TOTAL-FUN-TYPEs
with empty argument list.
Thus we have three possibilities:
1. Keep both BASIC-TYPEs or TOTAL-FUN-TYPEs with empty argument list
(as above).
2. Omit BASIC-TYPEs, and we get:
CONST-DECL ::= const-decl NAME TYPE
TYPE ::= TOTAL-FUN-TYPE | PARTIAL-FUN-TYPE
TOTAL-FUN-TYPE ::= total-fun-type SORT* SORT
PARTIAL-FUN-TYPE ::= partial-fun-type SORT* SORT
which is basically what we have in V0.95.
BUT this omission is ONLY possible in the first-order, not
in the higher-order case.
3. Omit TOTAL-FUN-TYPEs with empty argument list, and we get:
CONST-DECL ::= const-decl NAME TYPE
TYPE ::= BASIC-TYPE | TOTAL-FUN-TYPE | PARTIAL-FUN-TYPE
BASIC-TYPE ::= basic-type SORT
TOTAL-FUN-TYPE ::= total-fun-type SORT+ SORT
PARTIAL-FUN-TYPE ::= partial-fun-type SORT* SORT
and this resembles much Bernd's proposal (Bernd has a special
PARTIAL-CONST for parameterless partial functions).
BUT this introduces an asymmetry between partial and total functions.
Since there are problems with 2. and 3., I vote for possibility 1
(even if it bears some redundancy).
[I don't see the problems with 2. - surely the extension to HO can simply
extend TYPE with BASIC-TYPE? I would find it *very* difficult to explain
the redundancy of 1. in the Summary (and even more so in the Rationale :-)
With Maura's removal of total/partial distinctions from TYPE we might take:
CONST-DECL ::= const-decl NAME FUN-TYPE TOTALITY
FUN-TYPE ::= fun-type SORT* SORT
TOTALITY ::= total | partial
and the generalization to HO-CASL could be by adding to the above:
CONST-DECL ::= ... | const-decl NAME TYPE TOTALITY
TYPE ::= BASIC-TYPE | FUN-TYPE
BASIC-TYPE ::= basic-type SORT
FUN-TYPE ::= ... | fun-type TYPE* TYPE
where with order-sorted abstract syntax the first-order case is still
there as subsorts. --PDM]
[Continuing:]
I only have comments to other comments, no direct
comments on v0.96 (but I share most of Andrzej's comments).
Constants and functions, cont'd
-------------------------------
I start with an extension of my proposal for treating constants and
functions.
In the higher-order extension, it is desirable also to have products.
So replace TYPE* by PRODUCT-TYPE:
CONST-DECL ::= const-decl NAME TYPE
TYPE ::= BASIC-TYPE | TOTAL-CON-TYPE | PARTIAL-CON-TYPE |
TOTAL-FUN-TYPE | PARTIAL-FUN-TYPE |
PRODUCT-TYPE
BASIC-TYPE ::= basic-type SORT
TOTAL-FUN-TYPE ::= total-fun-type TYPE TYPE
PARTIAL-FUN-TYPE ::= partial-fun-type TYPE TYPE
PRODUCT-TYPE ::= product-type TYPE*
(Not that Bernd's partial constant type here is recovered
as partial-fun-type product-type () t, where t is any type.)
Then the first-order restriction is:
CONST-DECL ::= const-decl NAME TYPE
TYPE ::= BASIC-TYPE | TOTAL-CON-TYPE | PARTIAL-CON-TYPE |
TOTAL-FUN-TYPE | PARTIAL-FUN-TYPE
BASIC-TYPE ::= basic-type SORT
TOTAL-FUN-TYPE ::= total-fun-type PRODUCT-TYPE SORT
PARTIAL-FUN-TYPE ::= partial-fun-type PRODUCT-TYPE SORT
PRODUCT-TYPE ::= product-type SORT*
[This change seems quite innocuous. How about APPLICATION, should we
replace TERM* by TERMS there? --PDM]
Subsorts and compound identifiers
---------------------------------
PDM> Perhaps you might also remind me of the arguments against *always*
PDM> extending subsorting to compound sort identifiers when forming or
PDM> amalgamating signatures - these arguments are not in S-2, as far
PDM> as I can see. The language summary will have to warn readers
PDM> about the lack of monotonicity. (I recall now that Michel was
PDM> worried about this in Paris, but I missed the point then...) [...]
PDM>
AT> In S-2 we did not address this issue at all, leaving it for
AT> the subsorting group. If I recall right, the input from them was
AT> ambiguous: basically, we would like to get that subsorting does carry
AT> through compound identifiers usually, but there were some anomalies
AT> Till pointed out.
PDM>Till, would you please describe those anomalies? Especially since
PDM>your comment on this point in (the annotated-discharged language
PDM>summary) S-1 v1.3 suggests resolving the question to confirm the v0.95
PDM>wording, whereas the dischargement contradicts your recommendation!
The anomaly mainly was in the example
spec LIST (ELEM) =
sorts Empty < Stack(Elem)
...
Then, we would have both Empty < Stack(Int) and Empty < Stack(Bool),
which makes the axiom D(Empty) ill-formed.
But of course this example can be repaired by making Empty into
a compound sort, too.
[Presumably you mean D(empty), where empty:Empty. I must admit that I
find it a bit disconcerting that D(empty) is ill-formed, and cannot be
easily disambiguated... One could make Stack(Elem) < Stack, I
suppose, which would ensure that all stack functions were in the
overloading relation - isn't there an easier way? --PDM]
And moreover, we have to require that the subsort relation
extends to compound sorts in an instantiation context, so there
would be no way to avoid the above phenomenon.
So we agree that Elem < Seq (Elem) leads to
Nat < Seq (Nat) within an instantiation, as it is in V0.96.
The other question is whether Nat < Int should lead
to Seq (Nat) < Seq (Int), and whether this should be a general
restriction on signatures or be required only when both
compound sorts are produced by an instantiation ("require"
here means that the needed subsort relation is generated
automatically if not explicitly given).
I have no particular bias to any alternative here.
But let me note that in S-2, compound ids are intimately linked
with instantiations, while their structure is not "visible"
in other contexts. If we make this to a general rule in CASL,
this would imply that Nat < Int leads to Seq (Nat) < Seq (Int)
only in instantiation context (or not even that, because
it is not required in an instantiation).
[Wouldn't it be semantically cleaner to decouple this form of subsort
compatibility from instantiation? --PDM]
But I also have nothing against Peter's proposal:
>PROPOSAL: Require subsorting between compound sort identifiers to be
>compatible with subsorting between their components.
ISO-DECLs
---------
AT> 5) sect.4.1, p. 13:
AT>
AT> It is stated here that an embedding declaration cannot lead to
AT> implicit (other than imposed by ISO-DECLs) cycles in the sort
AT> ordering. I believe that in Paris/Lille we were discussing a stronger
AT> requirement: that in no context a new cycle can appear, except for an
AT> explicit declaration in ISO-DECL. I do not think this is ever
AT> mentioned now in the summary.
AT>
AT> However, I think now that perhaps this was a suggestion which goes a
AT> bit contrary to the overall language design. If I recall right, the
AT> only reason for this was that "if a new cycle is introduced
AT> implicitly then this is probably an error". In other similar cases
AT> (e.g. name clashes, notably in instantiations of generic specs) we
AT> have taken the opposite view: "okay, this might have been an error,
so
AT> perhaps a tool should warn the user, but since this makes perfect
AT> semantic sense, we do not throw this out as a possibility for the
AT> user".
AT>
AT> Perhaps the similar philosophy should be applied here, and we should
AT> allow cycles to be introduced by language constructs?
PDM>Should we then eliminate ISO-DECL altogether?
But this would contradict the above-mentioned philosophy, because we
then even could not warn the user. So I propose to keep ISO-DECLs
as a possibility to introduce cycles without getting a warning.
Type checking
-------------
AT> 6) This is more a question to the subsorting group than a comment: do
AT> we have a decent "type-checking" algorithm to type terms and formulae
AT> and check if they are well-formed? (sorry if this was written
AT> somewhere and I missed this among the tones of CoFI material).
PDM>A paper including this has been written, but not released yet. It
PDM>works on AS trees, adding qualifications where missing. I don't know
PDM>whether it can be combined with parsing. [Till? --PDM]
Kolyang, Bernd and I will present a paper on the ADT workshop which
covers parsing, static semantic analysis, overload resolution (i.e.
the "type-checking") and a semantic embedding into higher-order logic.
Partial restrictions
--------------------
Finally, a comment on the example
>sort s s'
>s < s'
>f: s -> s (partial or total)
>f: s' -> s' (partial or total)
>a: s
There was a controversy between Maura and Andrzej/Michel,
which concluded with:
MC>Andrzej is (as always) right!
MC>Sorry.
Correct up to here...
MC>This proves once more that I'm NOT one of the "subsorting people".
But Maura, your interpretation is exactly what Olaf proposed once
within the subsorting group (remember his "weak overloading" with
partial restrictions). Only later on we decided to throw this out :-).
Greetings,
Till