[opentheory-users] lambda terms vs articles

[Joe Leslie-Hurd]

Hi Ramana,

> Was the OpenTheory design chosen after a careful comparison,
> or was it just a matter of using something familiar and straightforward?

I wish I could say that was true, but actually I have never compared
the current design against any other. During design of the article
format my number one priority was to make it easy to read in proofs,
both in terms of reducing the implementation complexity of a reader
and also reducing the maximum memory required to read in a proof.

Given well-specified commands there are known techniques for
implementing a virtual machine, and indeed by now there exist several
implementations of readers for OpenTheory articles. In addition, a
natural implementation will free objects (such as terms or theorems)
for garbage collection as soon as they are no longer required,
minimizing the memory required to read in a proof.

It would definitely be cleaner to represent higher order logic proofs
using lambda calculus, but I would hope these practical considerations
are also taken into account in the design of an alternative format.

Cheers,

Joe