Re: Layout syntax

<joachim.durchholz@web.de> 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.


This is a type of discussion about the influence of computers that I
have already lived through several times: When calculators first
arrived in the seventies, many felt one should not departure from
knowledge about how it was calculated. But eventually, the calculators
became more accurate, and then nobody, expect experts, cares exactly
how those calculations are done.


The same thing will most surely happen with computer languages: At a
point in time when the implementations of algorithms and proofs can be
mathematically rigorously and reliably checked by the computer, there
will be no need for humans to do that checking, except when
implementing the proof checking programs themselves. Those that write
proofs will do that interactively with a computer, just as one is
doing in programming. So it will not be needed to wrote proofs so that
humans can directly check them, even though humans still must be able
to write proofs.


But getting there is a long way to go.


>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.


Let's generalize typical computer type systems, and see where we might
land: Hindley-Milner type systems rely on unification to resolve
polymorphic types. The next generalization might be a type system that
make use of a Prolog engine, of which unification is a part then. And
generalizing that, one might instead make use of a proof checking
engine, based on metamathematics. Then the type system might be
something like axiomatic set theory. If one gets that far, one has
unified computer type systems with pure math. :-)


>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),


Church's (lambda x.f) is in working math often written as x |-> f. The way
I handle these syntactic differences when implementing my proof checking
program is by designing it around "semantic trees": A semantic tree is a
(finite) labelled ordered tree. A parse tree is a semantic tree, and one
can get new semantic trees by specializing via suitable grammar rule
actions. With this terminology in hand, the semantic trees of (lambda x.f)
and x |-> f will be
        lambda |->
          / \ / \
        x f x f
That is, they will be the same except for a trivial relabelling of the
nodes: lambda <-> |->. This is in fact a common situation in math: Even
though notation may vary, one often seems to agree fairly well on what
these semantic trees should be.


So it is by that easy to find a common semantic representation in the
computer. And so it will not make any difference which syntax is used in a
formula, in the sense that one can allow local parsing contexts.


    Hans Aberg

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