Re: [Toss-devel] New Speagram: terms with sharing

[Lukasz K. <luk...@gm...>]

Hi.

> I see no (short term) value in doing that without a "vision". I think
> I will do a tests/Polish.trs or some other test to expose the
> "hierarchical" / inheritance aspect of new terms. I finally have an
> idea of which "supertypes" to display, and how :-) it is related to
> exposing GLB for use from the trs level. The default for printing
> terms will be to display those superclasses that are more specific
> than the corresponding declared supertypes. So I'm only thinking about
> finishing the Speagram work...

I think polish trs is a very nice idea, independent of everything else :).
But I am really convinced that doing formulas in Term is also important.
And yes - it is not a "vision" - and it has nothing visionary in itself. But it
is integration, and visions without integration become irrelevant very fast.

Still - I do have a few points which I think could be done with Term when
basic integration with Toss is ready. These are very preliminary suggestions,
so do not treat them too seriously - but maybe at least one is important.
(1) a language-interface to Toss finally (using SGRS and Term)
(2) typed formulas; I mean support for multi-typed structures, when the
  universe is divided into many subsets of different type and formulas are
  implicitly only about the subset; the guards in the formula could be then
  automatically derived from the types, so e.g you could say
  "ex x parent(x, y) and ex z drives_bicycle(y, z)" and automatically it would
  become "ex x (Person (x) and parent (x, y) and ex z (Object (z) and ...)))".
(3) finally support for functional formulas and constants! It is very disturbing
  to write every time "ex zero (is_zero(zero) and ex one (succ (zero, one) and
  succ (one, x))" when you want to say "x = succ (succ (zero))". We could try
  to put this inside Formula and Structure ml, but I think a lot can be done
  just by pre-processing. Still - it is too complex for FormulaParser I think,
  and it could be a good test for some features of Term.

I think I could also see a few more use cases just for Formulas, but the main
point - I hope you can see it - is to start really *using* the new
Term features.
It will surely reveal some problems and maybe we will learn other nice ways
of doing some things - but I think Term is ready to start being really used :).

Best!

Lukasz