toss-devel — Toss develpment discussion

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

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

> These are quantified variants of translating terms to structures... So
> it would be natural to share code between translating to formulas and
> translating to structures. And start with the latter since it's simpler.

I'm afraid that I do not fully understand - why are these quantified variants
of translating to structures, and why is that easier? I am surely in favour
of starting with the easier thing!

Lukasz

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

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

On Sat, Sep 22, 2012 at 12:19 AM, Lukasz Kaiser <luk...@gm...> wrote:

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

These are quantified variants of translating terms to structures... So
it would be natural to share code between translating to formulas and
translating to structures. And start with the latter since it's
simpler.

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

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

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

On Fri, Sep 21, 2012 at 2:40 PM, Lukasz Kaiser <luk...@gm...> wrote:
>
> This looks nice - it will finish the term part without sharing, right?
> But the next step I was talking about does not require any vision
> at all. I meant exactly replacing the current FormulaParser with Term,
> i.e. just writing a trs specification for formulas, a function to get them
> back in ocaml, and actually replacing the parser with Term.
> What do you think about that?

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

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

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

Hi.

> I don't have a vision of how Toss specifications should look like, so
> I don't see short-term benefits. I'll finish basing rewriting on
> ISA-matching (it only needs revision of associating rules with
> functors), and expose Greatest Lower Bound so that the implemented
> machinery is available for use; leaving only the explicit sharing and
> term<->structure translations not implemented.

This looks nice - it will finish the term part without sharing, right?
But the next step I was talking about does not require any vision
at all. I meant exactly replacing the current FormulaParser with Term,
i.e. just writing a trs specification for formulas, a function to get them
back in ocaml, and actually replacing the parser with Term.
What do you think about that?

Lukasz

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

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

On Mon, Sep 17, 2012 at 6:30 PM, Lukasz Kaiser <luk...@gm...> wrote:
>
> a hard look at where we are with Toss, thinking about a release,
> and it seems to me that the new things (Term and Diagram) have
> one big problem - lack of integration. Of course - sharing will help
> integrate terms with structures a lot, but I think we should start
> by using Term as a parser for formulas. What do you think?
> Formulas are in fact the biggest part of any toss file, so if we
> move with formulas to term-based parsing, that will be a lot.
> And it could finally allow some type-checking inside formulas!

I don't have a vision of how Toss specifications should look like, so
I don't see short-term benefits. I'll finish basing rewriting on
ISA-matching (it only needs revision of associating rules with
functors), and expose Greatest Lower Bound so that the implemented
machinery is available for use; leaving only the explicit sharing and
term<->structure translations not implemented.

Good luck!

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

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

Hi.

> I propose that shared subterms have two representations: [...]

I like the representation with "Ref" that you are writing about, but
I think that we should go back a little bit and do a few other things
before we proceed with sharing (or diagrams for that matter). I took
a hard look at where we are with Toss, thinking about a release,
and it seems to me that the new things (Term and Diagram) have
one big problem - lack of integration. Of course - sharing will help
integrate terms with structures a lot, but I think we should start
by using Term as a parser for formulas. What do you think?
Formulas are in fact the biggest part of any toss file, so if we
move with formulas to term-based parsing, that will be a lot.
And it could finally allow some type-checking inside formulas!

Lukasz

P.S. As to diagrams, I decided that I first need to refactor AssignmentSet
a bit, because it is simply to complicated to replace outright. And one thing
that I should have done some time ago is to remove MSO assignments.
This is not that easy - they are used in some parts - but I started working
on it and, as a first step, removed `MSO variant from variables.

[Toss-devel] New Speagram: terms with sharing

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

Hi,

I propose that shared subterms have two representations: either as a
sharing variable, possibly referring to a term in an accompanying
iterated substitution but it could also be a free variable, or as a
new variant, [Ref of string * term], with an implementation invariant:
two Refs in a term that have the same name contain physically equal
term. Basically, applying an iterated substitution "subst" would
replace "SVar (v, ...)" with "Rev (v, subst(v))" rather than directly
with "subst(v)".

There is a complication leading to the need to store the "Ref" name
inside "subst" rather than relying on the name of substituted
variable. When sharing variables "x" and "y" are unified they need to
be substituted with the same Ref name; but Term already uses the
notion of order on variables (just string comparison), it will be
natural to add.

Regards.

Re: [Toss-devel] Fwd: [Caml-list] existing implementation of data structures for storing points/doing nearest neighbour search in OCaml

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

> Might be useful.

Thanks, it will be! I hope to get to these things relatively soon.

Lukasz

Re: [Toss-devel] Moving to Git?

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

Hi.

> Everyone and their mom seems to be using github these days. I know
> you've put some work into updating the svn repository, but do you
> think it might be worthwhile to move to git? Just asking.

I do not see the value in it as long as there are so few developers
(I think git excels at larger projects and involved merges). I was
also not happy with this svn change, but sourceforge was pushing it,
so it looked inevitable. I'm not sure git is so far already ;).

Best,

Lukasz

[Toss-devel] Moving to Git?

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

Hi,

Everyone and their mom seems to be using github these days. I know
you've put some work into updating the svn repository, but do you
think it might be worthwhile to move to git? Just asking.

Cheers.

[Toss-devel] Fwd: [Caml-list] existing implementation of data structures for storing points/doing nearest neighbour search in OCaml

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

Might be useful.


---------- Forwarded message ----------
From: Francois Berenger <ber...@ri...>
Date: Wed, Sep 5, 2012 at 4:01 AM
Subject: [Caml-list] existing implementation of data structures for
storing points/doing nearest neighbour search in OCaml
To: caml-list <cam...@in...>


Hello,

I was looking for a few data structures to accelerate some
geometric operations on 3D point sets.
I was happily surprised. The harvest was gorgeous:

kd-tree in OCaml:
- https://github.com/bpr/kd_tree

R-tree in OCaml:
- https://github.com/mariusaeriksen/ocaml-rtree

Vantage point tree in OCaml:
- http://codepad.org/F1hckj5K

Regards,
F.

--
Caml-list mailing list.  Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Toss-devel] New Speagram commit

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

Hi,

If you currently use Speagram (i.e. Term), do not update from svn :-/
I've just committed the long work with "step 6", because there is
already a lot of vetted code, but there is a serious regression
(rewriting does not work) and tests are not adapted to changes. Who
knows how many days it would take me before commit if I waited till
everything works, now I can commit whenever I fix something...

Best.

[Toss-devel] Dyna programming language

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

It's not directly related to Toss, but I recommend it as "food for thought"

http://www.dyna.org/wiki/index.php?title=Papers

It is a Prolog (Datalog without restrictions) language with equations
(over some algebra, usually reals) attached to Horn clauses, whose
fixpoint is the solution to weights associated with terms.
(Implementation is probably unavailable.)

Re: [Toss-devel] Speagram, resigning from preference-based disambiguation

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

Hi.

> I'll add a builtin.trs file with "fictitious" declarations matching
> those in BuiltinLang, should it be in lib/ or in tests/ ? I guess
> tests/ makes more sense although they "precede" core.trs.

I don't think this file is necessary for one simple reason - we have
tought about this same problem during speagram times :). It took
me a while to recall what was our solution, but now I know - we
added an option to the old speagram to print out the "as if" version
of BuiltinLang. It still works - just call ./TRSTest.native -l "" -b and
it will print it out. I prefer this to a fixed file, as you have to update
the file whenever you change BuiltinLang - and the printed-out stuff
is always up-to-date. Maybe we should add a "make builtin" option
to Term to have it printed out? On the other hand, this:

> [...] if I could move brackets (parentheses) to user space [...]

is another issue. I tried to only put things in BuiltinLang if they were
absolutely needed in the code - everything else should be in core.
I do not recall any more why parentheses were in BuiltinLang - but
if you can put them out, then of course do it - the less the better :).

Best!

Lukasz

Re: [Toss-devel] Speagram, resigning from preference-based disambiguation

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

I'll add a builtin.trs file with "fictitious" declarations matching
those in BuiltinLang, should it be in lib/ or in tests/ ? I guess
tests/ makes more sense although they "precede" core.trs.

On Tue, Aug 21, 2012 at 10:51 PM, Lukasz Stafiniak <luk...@gm...> wrote:
> But there might be a different reason to keep these facilities in
> BuiltinLang, to remove the overhead during "normalization". They add a
> silly-looking type prefix to types of values, and shorter prefixes to
> types of expressions. While they shouldn't affect rewriting, they use
> some memory and are un-aesthetic. They can be removed after parsing,
> only not from syntax definitions.

Re: [Toss-devel] Speagram, resigning from preference-based disambiguation

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

But there might be a different reason to keep these facilities in
BuiltinLang, to remove the overhead during "normalization". They add a
silly-looking type prefix to types of values, and shorter prefixes to
types of expressions. While they shouldn't affect rewriting, they use
some memory and are un-aesthetic. They can be removed after parsing,
only not from syntax definitions.

On Tue, Aug 21, 2012 at 10:36 PM, Lukasz Stafiniak <luk...@gm...> wrote:
> Hi,
>
> Do you recall how much BuiltinLang was motivated by having the
> preference job to do? It would be great to move as much of it to
> core.trs as possible. This would make the language simpler to explain
> (although one could always provide an "as if" .trs in documentation).
> In particular if I could move brackets (parentheses) to user space,
> then the facilities for operator associativity and precedence (other
> than "hierarchical terms theory") would be entirely a dozen lines in
> user-space.

[Toss-devel] Speagram, resigning from preference-based disambiguation

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

Hi,

Do you recall how much BuiltinLang was motivated by having the
preference job to do? It would be great to move as much of it to
core.trs as possible. This would make the language simpler to explain
(although one could always provide an "as if" .trs in documentation).
In particular if I could move brackets (parentheses) to user space,
then the facilities for operator associativity and precedence (other
than "hierarchical terms theory") would be entirely a dozen lines in
user-space.

Re: [Toss-devel] New Speagram: plan of action

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

I've finished the first half of step (5), but it turns out that using
subtyping for "parsing stuff" like associativity is not trivial,
requires some work that deserves a step number of its own. So the
future steps below get a +1. I'm not committing step 5 because
internet stopped working on my desktop computer and svn says "generic
failure" on my laptop :-( totally inexplicable.

On Mon, Jun 25, 2012 at 5:17 PM, Lukasz Stafiniak <luk...@gm...> wrote:
> On Wed, Jun 20, 2012 at 7:04 PM, Lukasz Stafiniak <luk...@gm...> wrote:
>>
>> (5) switch the parser to use subtyping (replace "mgu" with "glb") and
>> start moving the built-in and core grammars and the standard library
>> to use subtyping.
>
> Looking a bit into the future:
>
> (6) specify explicit sharing and come up with a representation,
>
> (7) adapt terms to sharing and propagate the changes -- modify algorithms,
>
> (8) implement the translation of terms to hypergraphs (structures / models),
>
> (9) implement alternative rewriting based on ISA-matching (perhaps
> permanently keeping both strategies for rewriting).

Re: [Toss-devel] Toss Repository Change

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

> Sorry, sent by mistake

No problem! The lack of commit emails looks like a bug
of the new sf and it irritates me very much as well!

Lukasz

Re: [Toss-devel] Toss Repository Change

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

Sorry, sent by mistake

2012/8/9 Lukasz Stafiniak <luk...@gm...>:
> Commitowałem niedawno, ale nie dostałem maila z svn...

Re: [Toss-devel] Toss Repository Change

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

Commitowałem niedawno, ale nie dostałem maila z svn...

Re: [Toss-devel] Toss Repository Change

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

Przepraszam miałem drobny kryzys po powrocie do Wrocławia, można
powiedzieć że lenistwo wakacyjne. Od ostatniego maila nic z Tossa nie
zrobiłem, jak mówiłem "New Speagram step 4" jest bardzo blisko w
debugowaniu, wywala się na samym końcu "lib", potem trzeba jeszcze
zrobić "tests". Udało mi się tym razem checkoutować. Dzięki.

Re: [Toss-devel] Wolfram SystemModeler

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

Link:
http://blog.wolfram.com/2012/08/01/building-a-refrigerator-in-wolfram-systemmodeler/

Re: [Toss-devel] Imperative Rule Representation

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

> I'm sorry for not checking the paper right now, but I think that rules
> based on adding/deleting are already fully implemented (including a
> nice syntax), with *a lot* of flexibility (for example, with compiling
> defined relations into structure relations). Providing rules by
> structures is just an option.

I forgot that we already even had the syntax - that's really nice!
Now I think that we should move most our standard examples to
the imperative rule syntax, what do you think? Except for rules
where explicit grid-like structure syntax is used, this seems to be
much more readable, right? I just commited a change and moved
Tic-Tac-Toe, but I'll wait with the other games to know what you think.

Another small change I made is to replace MATCH with pre. I am
not 100% sure, but it seems to me that there is no real difference if
you write precondition inside MATCH or later after pre, right?
If so, then I prefer to have it all together in the front - exactly as
it is done in YAGI in the paper I cited in the previous mail (maybe
you don't need to read the whole paper, but just the first column of
the "YAGI by example" section on page 3). Do you agree with this
change? I hope that this will really make the rules more readable!

Lukasz