Re: Union Type Object problem

[Hans Aberg]

At 22:28 +0200 2004/08/12, Laurence Finston wrote:
>> I think that those that work with TeX, and especially extensions of it,
>> work in C, and not Pascal. For example, Omega does.

>Knuth programmed TeX and Metafont in Pascal using his
>"WEB System for Structured Programming".
>He published his code in _TeX: The Program_ and _METAFONT: The Program_ in the
>series "Computers and Typesetting".
>He and Silvio Levy developed CWEB, which is analogous to WEB, but for C and
>C++.  I use CWEB for GNU 3DLDF.

OK. I did not realize that CWEB is the program which does the WEB to C
translation. (When you mention, I recall it, but I have not followed the
TeX stuff so carefully in late years).

>> Other approaches might though be to write say a Metafont code to 3DLDF
>> translator. You may even further admit the Metafont be included in segments
>> of its own syntax, similar to the "extern" construct in C++.

>Someday, maybe.   There are many other tasks that I think are more important.
>
>One of the most clever things about Metafont is that it can solve linear
>equations and perform certain other operations with unknown quantities.  For
>example, the following is valid MF code:
>
>a = 2b;
>b = .5c + 1;
>c = 3;
>show a;
>--> 5
>show b;
>--> 2.5
>
>Since `a', `b' and `c' aren't declared, MF considers them to be of type
>`numeric'.  Operations on variables of other types with unknown values are
>also allowed.
>
>I plan to try to implement this in 3DLDF, but I have several more basic
>features to implement, such as conditionals, loops, and macros.  First I have
>to try to get my parser code to compile in under 5 minutes, though.

I do not know how MetaFont implements that, but it easy to modify a Prolog
engine into CLP(R) to solve more general numeric equations. I experimented
with such stuff before starting to write a theorem prover. I can send you
some code, if you want to. (It is not a part of my current theorem prover,
as it turned out that other things are more important if one wants to be
able to do strict math.)

>In MF, `path a' can be a `declaration' or a
>`boolean expression', e.g.,
>
>path a; % `declaration'
>
>if (path a) % `boolean expression'
>...
>fi
>
>I'm not even going to try to implement this using Bison.

The simplest way is to experiment with Bison compilations, to see if it is
accepted or not.

>Maybe it would work,
>but I think it's so likely not to, that I'm going to just use `is_path', etc.,
>for the `boolean expressions' instead.

But this might be better, as one is otherwise creating functions with
multiple return types, which may rhyme poorly with a context free grammar.

>The same applies to the `=' operator, which is used for `equations' rather
>than `assignments'.  In the following code:
>
>transform t, u;
>t = identity xscaled 2.3 yscaled 1.4 shifted (1, 2, 3);
>u := t;
>u = t;
>
>The first `=' is equivalent to `:=' (the assignment operator) because this is
>the first time a value is assigned to `t'.  The expression `u = t', on the
>other hand, is an assertion. In this case, it's redundant, so MF will issue a
>warning.
>
>I'm not even going to try to implement this, and will use `==' to test for
>equality instead.

When experimenting with syntax in my theorem prover, I came to the
conclusion that it is important to not mix up assignments (for which I
prefer ":=") and Boolean comparison (which typically uses "="). In
metamath, there is an important notion of "a theory with equality", in
which case "=" is the comparison operator (formally, a binary predicate).
But in a computer context, "==" might be better in order to avoid confusion
with ":=".

By contrast, the C++ function name overloading system (sometimes called
"Koenig lookup" seems important). It fairly naturally falls into theorem
provers and Prolog via unification of formulas.

>Knuth emphasized that MF supported a declarative style of programming.  I've
>run across this idea in other places as well, and I think that it hasn't
>turned out to be such an important idea, after all.  I don't think there's
>anything wrong with telling the computer what to do without beating about the
>bush.  It doesn't mind.

If I should compare this with the theorem prover picture then in truth, one
cannot expect a theorem prover to prove much of the actual pure math humans
produce. So the declarative style goes pretty fast out of the window,
expect as a convenience tool to simplify the proofs.

By contrasts, I remade the Prolog engine into one more like C/C++ where the
types of each symbol must be declared. This seems to be important for the
readability of the code.

In addition, I have a variable environment system similar to that in C/C++
(needed in nested proofs and the like). For this, I have a stacked lookup
table where the parser puts defined objects, and which the lexer looks into
whenever an identifier is discovered.

  Hans Aberg