Re: Layout syntax

Joachim Durchholz <>
27 Dec 2003 14:13:12 -0500

          From comp.compilers

Related articles
[2 earlier articles]
Re: Layout syntax (2003-12-13)
Re: Layout syntax (Carl Cerecke) (2003-12-13)
Re: Layout syntax (Joachim Durchholz) (2003-12-14)
Re: Layout syntax (2003-12-20)
Re: Layout syntax (Joachim Durchholz) (2003-12-21)
Re: Layout syntax (2003-12-23)
Re: Layout syntax (Joachim Durchholz) (2003-12-27)
Re: Layout syntax (2004-01-02)
Re: Layout syntax (Joachim Durchholz) (2004-01-07)
Re: Layout syntax (2004-01-09)
Re: Layout syntax (Joachim Durchholz) (2004-01-12)
Re: Layout syntax (2004-01-16)
Re: Layout syntax (Joachim Durchholz) (2004-01-18)
[5 later articles]
| List of all articles for this month |

From: Joachim Durchholz <>
Newsgroups: comp.compilers
Date: 27 Dec 2003 14:13:12 -0500
Organization: Oberberg Online Infosysteme
References: 03-12-016 03-12-060 03-12-081 03-12-104 03-12-112 03-12-124 03-12-131
Keywords: syntax, practice
Posted-Date: 27 Dec 2003 14:13:12 EST

Hans Aberg wrote:

> The question is what happens when math is written proof verification
> system, as the computer can easily check any nesting: then manual
> unnesting will no longer needed. So one will probably see more of
> such nesting then.

I don't think that this would be a Good Thing.
After all, proofs aren't just read by computers, they are also read by
humans (e.g. to check whether a proof states what was intended, or to
modify a proof to prove something slightly different but more
interesting), and humans don't parse nested constructs very well.

> I certainly admit nesting in my proof verification system: It is
> declarative, and one can have local variables, just as in say C/C++
> and most other modern declarative languages.

It's good to allow nesting. Two or three levels of nesting are usually
easily parsed by a human. It's just that nesting shouldn't go to
arbitrary levels. I routinely remove deeply-nested construct and put
them into separate, named constructs and then just use the name. (Just
as mathematicians are told to do.)

>> That's exactly my point: mathematical syntax, designed for
>> consumption by humans, isn't easily transferable to computer
>> language syntax, designed for consumption by computers. In other
>> words, drawing syntactical inspiration from actual mathematical
>> usage may be helpful, but sooner or later one is going to run into
>> trouble.
> My development strategy is to wrestle a bit with the more common
> popular syntactic features, such as sets, function definitions and
> the like, to make them close to actual mathematical usage. Then, if I
> get so far, added user math should use a less complicated syntax,
> perhaps defined by some operator precedence.

Seems reasonable.

>> Which is just my point: mathematics isn't the best source of
>> inspiration when it comes to syntax. (It's an excellent source of
>> inspiration when considering semantics! At least if a precise
>> semantics is desired.)
> Quite on the contrary: Just because of these difficulties, math
> becomes an important source if inspiration, because these apparent
> syntactic quirks are in reality there so as to produce a syntax that
> is efficient to humans. So, as computer languages can, in view of
> better computers, become more adapted to humans, it is important to
> have this input.

I think we're largely in agreement, and just differ in how far one
should go when trying to import mathematical conventions into a
computerized language.
I.e. I agree that arithmetic operators should be in any language, I'm
not so sure about difficult-to-parse constructs like lambdas without a
lambda keyword (but it might be worth the effort if the language is
specifically tailored towards expressing traditional math), and I
wouldn't even consider mimicking tabular layout to represent matrices
(but that's just me - if conformance to mathematical conventions is
important enough, it might be important enough to at least give it a stab).


Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.