Re: [CoFI] Concrete syntax for basic specifications

[Anne Haxthausen <ah@it.dtu.dk>]

I have tested the (concise) concrete syntax proposal on some examples,
and generally I like it very much. I just found a minor visual problem:

The Latex macros for partial function symbol and existential equality symbol
  \stackrel{?}{\rightarrow} and \stackrel{!}{=} 
produce symbols which are higher than other symbols.
Hence, lines containing these symbols become higher than other lines.  

[Ouch! that aspect of the proposed notation hadn't occurred to me...
:-( --PDM]

It is possible to solve the problem for the partial function arrow
by making the raised "?" smaller, however for the existential equality
it is not possible to make the raised "!" small enough.

[Increasing \baselineskip would also remove the uneven line spacing
 problem - but that may not always be possible (nor perhaps desirable)
 in published articles containing CASL specifications.  So we do indeed
 need to find an alternative, more compact notation. --PDM]

So, I propose to use a smaller symbol than "!" to indicate existential
equality. That could for instance be a dot or a "~".

[The dot has the drawback that it is easy to overlook it.

 Putting the ~ over =, however, (\cong in LaTeX) usually indicates
 isomorphism rather than equality. 

 Moreover, the symbol obtained by replacing the top bar of = by ~
 (\simeq in LaTeX) is apparently used more for strong equality, with the
 ordinary = standing for existential equality (e.g. by Gordon Plotkin).

 There is also the earlier proposal of putting an e over = for
 existential equality (d for definedness would be too high).

 Which is the best of these?  Are there other possibilities?  

 --PDM]

For the visual effect, I would also prefer to use "~" instead of "?" above
the function arrow.

[That would indeed go visually well with ~ over = .  But I gather
 it is becoming conventional among theoreticians to use -` for
 partial function types (\rightharpoonup in LaTeX)...  --PDM]

Best regards,
   Anne Haxthausen

[Please would EVERYONE indicate their preferences for the display
 format of strong and existential equations, and of partial function
 types - mentioning any books and papers where the notation is used?
 Just send to cofi-language and I'll post a summary afterwards.  --PDM]