toss-devel Mailing List for Toss (Page 5)

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

> I guess I'll learn some stuff sooner, since I'm getting "NO PARSE:
> Function ?a '':'' '':'' ?a list as ?a list" right now...

Good luck!

Lukasz

On Wed, Jun 20, 2012 at 7:19 PM, Lukasz Stafiniak <luk...@gm...> wrote:
>
> I don't know, I'll keep it in mind. I should know more after recalling
> myself the SyntaxDef and ParseArc code in step (2), right?

I guess I'll learn some stuff sooner, since I'm getting "NO PARSE:
Function ?a '':'' '':'' ?a list as ?a list" right now...

> I've come to the conclusion that a variable can have (as originally)
> only one type, which is different from a term which can have several
> supertypes.

Ok - that should be really easy to change, it always uses just one now.

> I don't agree. I'm talking about basic algorithms (which don't have
> "wiggle room"), not auxiliary algorithms like adding an intermediate
> node in inheritance hierarchy stored as a well-formed set of
> declarations.

We will see how things work in practice, of course.

Best!

Lukasz

On Wed, Jun 20, 2012 at 7:32 PM, Lukasz Kaiser <luk...@gm...> wrote:
> Hi.
>
>> The spec that is posted to the list.
>
> I get that - I was not sure which part exactly. Because in the one
> that I was thinking about, it seems to me that the definition of
> terms was exactly as our OCaml term type - no need to update.
> So what am I missing?

I've come to the conclusion that a variable can have (as originally)
only one type, which is different from a term which can have several
supertypes.

>>> Sure - that will hopefully disambiguate all casts!
>>
>> But this step is is just about implementing the algorithms.
>
> I am very much against implementing algorithms without
> adjusting the tests and core language at the same step.
> (By "step" I mean something bigger than a commit, of course.)
> And when they are adjusted, a lot of ambiguities will be gone :).

I don't agree. I'm talking about basic algorithms (which don't have
"wiggle room"), not auxiliary algorithms like adding an intermediate
node in inheritance hierarchy stored as a well-formed set of
declarations.

Hi.

> The spec that is posted to the list.

I get that - I was not sure which part exactly. Because in the one
that I was thinking about, it seems to me that the definition of
terms was exactly as our OCaml term type - no need to update.
So what am I missing?

>> Sure - that will hopefully disambiguate all casts!
>
> But this step is is just about implementing the algorithms.

I am very much against implementing algorithms without
adjusting the tests and core language at the same step.
(By "step" I mean something bigger than a commit, of course.)
And when they are adjusted, a lot of ambiguities will be gone :).

> I don't know, I'll keep it in mind. I should know more after recalling
> myself the SyntaxDef and ParseArc code in step (2), right?

Sure. In fact you could try to do a mini-step first and just store the type
of terms in the term - where it should be. Simple - but a good way to get
a look at the code, and I think that quite a few things will need correcting.

Best!

Lukasz

On Wed, Jun 20, 2012 at 7:19 PM, Lukasz Stafiniak <luk...@gm...> wrote:
> On Wed, Jun 20, 2012 at 7:14 PM, Lukasz Kaiser <luk...@gm...> wrote:
>>
>> Hmm - which spec? We agreed that it is best not to start doing
>> sharing and other stuff before we are done with subtyping, right?
>> And for that the terms we have are enough, so what is here to do?
>
> The spec that is posted to the list.

Sharing is not yet covered in the specification that I've worked out,
and is left out in steps (1-5), so:

(6) specify explicit sharing,

(7) update the definition of terms to match the new specs,

... etc.

On Wed, Jun 20, 2012 at 7:14 PM, Lukasz Kaiser <luk...@gm...> wrote:
> Hi.
>
>> (1) update the term representation and the "mgu" to match the specs
>> and propagate the changes (I'm here, stuck on some stupid type error
>> in ParseArc),
>
> Hmm - which spec? We agreed that it is best not to start doing
> sharing and other stuff before we are done with subtyping, right?
> And for that the terms we have are enough, so what is here to do?

The spec that is posted to the list.

>> (2) "modernize" the parsing algorithm (this will be one of the two
>> sources of speedup),
>
> This is long overdue :). Since terms have types, the TypedTerm
> could simply be a term now, right?

Probably yes.

>> (3) implement the "subtyping"-related algorithms like
>> greatest-lower-bound, including building of well-formed sets of
>> declarations,
>
> Sure - that will hopefully disambiguate all casts!

But this step is is just about implementing the algorithms.

>> (4) remove the coding-decoding of types and adapt the grammar
>> representation to be based around well-formed sets of declarations,
>>
>> (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.
>
> I think we have to move to subtyping first - only when everything works
> nice with subtyping, and there are no disambiguities any more, can one
> remove the term and type coding. I do not see how to do it otherwise.

I don't know, I'll keep it in mind. I should know more after recalling
myself the SyntaxDef and ParseArc code in step (2), right?

Hi.

> (1) update the term representation and the "mgu" to match the specs
> and propagate the changes (I'm here, stuck on some stupid type error
> in ParseArc),

Hmm - which spec? We agreed that it is best not to start doing
sharing and other stuff before we are done with subtyping, right?
And for that the terms we have are enough, so what is here to do?

> (2) "modernize" the parsing algorithm (this will be one of the two
> sources of speedup),

This is long overdue :). Since terms have types, the TypedTerm
could simply be a term now, right?

> (3) implement the "subtyping"-related algorithms like
> greatest-lower-bound, including building of well-formed sets of
> declarations,

Sure - that will hopefully disambiguate all casts!

> (4) remove the coding-decoding of types and adapt the grammar
> representation to be based around well-formed sets of declarations,
>
> (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.

I think we have to move to subtyping first - only when everything works
nice with subtyping, and there are no disambiguities any more, can one
remove the term and type coding. I do not see how to do it otherwise.

Best!

Lukasz

Here are the incremental steps as I see it right now:

(1) update the term representation and the "mgu" to match the specs
and propagate the changes (I'm here, stuck on some stupid type error
in ParseArc),

(2) "modernize" the parsing algorithm (this will be one of the two
sources of speedup),

(3) implement the "subtyping"-related algorithms like
greatest-lower-bound, including building of well-formed sets of
declarations,

(4) remove the coding-decoding of types and adapt the grammar
representation to be based around well-formed sets of declarations,

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

Cheers!

The updated specification:

    {3 Specification of Hierarchical Terms}

    Hierarchical terms have the form: [f(s_1, ..., s_m; t_1, ...,
    t_n)] where [f] is a (function/constant/class) symbol, terms [s_1,
    ..., s_m] are called direct supertypes and terms [t_1, ..., t_n]
    are called direct subterms of the term, or [X(s)], where [X] is a
    variable symbol and term [s] is called the type of the variable.
    When [f(s_1, ..., s_m; t_1, ..., t_n)], resp. [X(s)] is not a
    subterm or supertype of another term, we call [f], resp. [X] its
    head symbol. Hierarchical terms are related by [ISA] as formally
    presented below; we drop "hierarchical" when referring to terms
    for convenience.

    We call the {i upper grounding} of a term [t], [ug(t)], the term
    [t] with all occurrences of [X(s)] for any variable symbol [X] and
    term [s] replaced by [s].

    We start by defining [t ISA t'] for [t] and [t'] ground terms
    (i.e. terms without occurrences of variable symbols).
    It holds if and only if one of the following holds:

    {ul
    {- [t' = Type] for the top symbol [Type],
    {- [s_i ISA g(s'_1, ..., s'_m'; t'_1, ..., t'_n')] for some i,
    where [s(t)=f(s_1, ..., s_m; t_1, ..., t_n)] and
    [r(t')=g(s'_1, ..., s'_m'; t'_1, ..., t'_n')]}
    {- [s_i ISA s'_i] for all [i], [t_i ISA t'_i] for all [i],
    where [s()t=f(s_1, ..., s_m; t_1, ..., t_n)] and
    [r(t')=f(s'_1, ..., s'_m; t'_1, ..., t'_n)]}}

    We define {i ground substitution over variables [V]} by extending
    into a function over terms in the standard way a finite mapping
    from all variables in [V] to terms, requiring that [X(s)] is
    mapped to [t] only when: [t] does not contain variable symbols,
    and [t ISA ug(s)]. By [FV(t)] we denote the free variables of [t].

    [t ISA t'] if and only if for all ground substitutions [s] over
    [FV(t)] there is a ground substitution [r] over [FV(t')] such that
    [s(t) ISA r(t')].

    (We present [ISA] as describing generality, "is less (or equally)
    general than". Notice that this relation is often presented as
    describing the amount of information, the reverse quantity, as "has
    more information than".)

    We need two more essential notions.

    A {i well-formed set of declarations} is defined as a set of terms
    such that all of the following conditions hold:

    {ul
    {- no two terms in it have the same head symbol,}
    {- head symbols of terms in it are not variables,}
    {- there is at most one glb-unification result for any two (or
    more) elements from the set,}
    {- every symbol used in any term in the set is a head symbol of
    some element of the set,}
    {- for any subterm or supertype of a term from the set, its upper
    grounding ISA the element of the set which has the same head
    symbol.}}

    Note that the last two conditions will be enforced by parsing the
    term to be introduced into the set of declarations, so in the
    current module we only need to check the first three conditions.

    A {i well-formed term with respect to a set of declarations} given
    a well-formed set of declarations, is a term [t] such that:

    {ul
    {- its supertypes and subterms are well-formed (w.r.t. this set of
    declarations),}
    {- there is a term [d] in the set of declarations such
    that [t ISA d] and either the head symbol of [t] is a variable or
    it is the same as the head symbol of [d],}
    {- for any two occurrences [X(s)] and [X(s')] of variable symbol
    [X], [s=s'].}}

    We limit all terms considered to terms that are well-formed with
    respect to a set of declarations (fixed by the context; we will
    drop constantly mentioning "w.r.t. a set of declarations"). In
    particular, we only allow {i well-formed substitutions}:
    substitutions that when applied to a well-formed term, return a
    well-formed term:

    A {i well-formed substitution} is defined by extending into a
    function over terms in the standard way a finite mapping from
    variables (terms whose head symbols are variable symbols) to
    terms, requiring that [X(s)] is mapped to [t] only when [t ISA s].

    We define matching a pattern [p] against a ground term [t] (where
    [p] and [t] are well-formed) as the problem of deciding [t ISA p]
    by finding the substitution [r] from the definition of
    [ISA]. (Groundness of [t] is not essential as we can rename its
    variables to fresh constants.)

    We define {i glb-unification} ({i Greatest Lower Bound
    Unification}) of two or more well-formed terms [t_1, ..., t_n] as:
    given that there exist a well-formed term [t] and a well-formed
    substitution [r], such that for all substitutions [s] such that
    [s(r(t_i))] are all ground, for all [i], [s(t) ISA s(r(t_i))].

    {3 Extension to Function Types}

    In type systems, types of functions interact with subtyping in
    such a way that only the result type is covariant -- behaves like
    supertypes and subterms above -- while argument types are
    contravariant. To ensure proper behavior and have maximal
    flexibility, we would need to define "least upper bound
    unification" mutually recursively with glb-unification, for use in
    contravariant positions. To simplify we sacrifice flexibility: we
    use the standard first-order unification instead of
    glb-unification on function argument types.

    We introduce function type symbol [funtype] and higher-order
    variables [X(s; t_1, ..., t_n)].

    Formally, the definition of [ISA] extends to [funtype] as follows:

    For [t=funtype( ; t_1, ..., t_{n-1}, t_n)], [t ISA t'] if and only
    if for all ground substitutions [s] over [FV(t)] there is a ground
    substitution [r] over [FV(t')] such that [r(t')=funtype( ; t'_1,
    ..., t'_{n-1}, t'_n)] and [s(t_n) ISA t'_n], [s(t_i) = t'_i] for
    [1 <= i <= n-1].

    For [t=X(t_0; t_1, ..., t_n)], [t ISA t'] if and only if for all
    ground substitutions [s] over [FV(t)] there is a ground
    substitution [r] over [FV(t')] such that [r(t')=funtype( ; t'_1,
    ..., t'_n, t'_0)] and [s(t_0) ISA t'_0], [s(t_i) = t'_i] for
    [1 <= i <= n].

On Tue, Jun 19, 2012 at 1:13 AM, Lukasz Stafiniak <luk...@gm...> wrote:
>
>    A {i well-formed set of declarations} is defined as a set of terms
>    such that all of the following conditions hold:
>
>    {ul
>    {- no two terms in it have the same head symbol,}
>    {- head symbols of terms in it are not variables,}
>    {- all subterms and supertypes of a term from the set are also in
>    the set,}

This part is wrong, it should be "all subterms and supertypes of a
term from the set ISA some corresponding element in the set and should
not use symbols not already declared".

I'm also thinking about (working on) variables and well-formed
substitutions, they are not defined properly. I'll post the whole
updated specification soon.

On Tue, Jun 19, 2012 at 1:13 AM, Lukasz Stafiniak <luk...@gm...> wrote:
>
>    Formally, the definition of [ISA] extends to [funtype] as follows:
>
>    [funtype( ; t_1, ..., t_{n-1}, t_n) ISA funtype( ; t'_1, ...,
>    t'_{n-1}, t'_n)] if and only if for all substitutions [s] there is
>    a substitution [r] such that [s(t)] and [r(t')] are both ground
>    and [s(t_n) ISA r(t'_n)], [s(t_i) = r(t'_i)] for [1 <= i <= n-1].

Slight mistake, should be:

    [t ISA t'] if and only if for all substitutions [s] there is a
    substitution [r] such that [s(t)=funtype( ; t_1, ..., t_{n-1},
    t_n)] and [r(t')=funtype( ; t'_1, ..., t'_{n-1}, t'_n)] are both
    ground and [s(t_n) ISA r(t'_n)], [s(t_i) = r(t'_i)] for [1 <= i <=
    n-1].

Hi,

The formal recipe is ready:

    {3 Specification of Hierarchical Terms}

    Hierarchical terms have the form: [f(s_1, ..., s_m; t_1, ...,
    t_n)] where [s_1, ..., s_m] are direct supertypes and [t_1, ...,
    t_n] are direct subterms of the term. [f] can be a symbol or a
    variable and is called the head symbol of the term. They are
    related by [ISA] as formally presented below:

    [t ISA t'] if and only if for all substitutions [s] there is a
    substitution [r] such that [s(t)] and [r(t')] are both ground and
    one of the following holds:

    {ul
    {- [s_i ISA g(s'_1, ..., s'_m'; t'_1, ..., t'_n')] for some i,
    where [s(t)=f(s_1, ..., s_m; t_1, ..., t_n)] and
    [r(t')=g(s'_1, ..., s'_m'; t'_1, ..., t'_n')]}
    {- [s_i ISA s'_i] for all [i], [t_i ISA t'_i] for all [i],
    where [s()t=f(s_1, ..., s_m; t_1, ..., t_n)] and
    [r(t')=f(s'_1, ..., s'_m; t'_1, ..., t'_n)]}}

    (We present [ISA] as describing generality, "is less (or equally)
    general than". Notice that this relation is often presented as
    describing the amount of information, the reverse quantity, as "has
    more information than".)

    We need two more essential notions.

    A {i well-formed set of declarations} is defined as a set of terms
    such that all of the following conditions hold:

    {ul
    {- no two terms in it have the same head symbol,}
    {- head symbols of terms in it are not variables,}
    {- all subterms and supertypes of a term from the set are also in
    the set,}
    {- there is at most one glb-unification result for any two (or
    more) elements from the set.}}

    A {i well-formed term with respect to a set of declarations} given
    a well-formed set of declarations, is a term [t] such that its
    supertypes and subterms are well-formed (w.r.t. the set of
    declarations), there is a term [d] in the set of declarations such
    that [t ISA d] and either the head symbol of [t] is a variable or
    it is the same as the head symbol of [d].

    We limit all terms considered to terms that are well-formed with
    respect to a set of declarations (fixed by the context; we will
    drop constantly mentioning "w.r.t. a set of declarations"). In
    particular, we only allow {i well-formed substitutions}:
    substitutions that when applied to a well-formed term, return a
    well-formed term.

    We define matching a pattern [p] against a ground term [t] (where
    [p] and [t] are well-formed) as the problem of deciding [t ISA p]
    by finding the substitution [r] from the definition of
    [ISA]. (Groundness of [t] is not essential as we can rename its
    variables to fresh constants.)

    We define {i glb-unification} ({i Greatest Lower Bound
    Unification}) of two or more well-formed terms [t_1, ..., t_1] as:
    given that there exist a well-formed term [t] and a well-formed
    substitution [r], such that for all substitutions [s] such that
    [s(r(t_i))] are all ground, for all [i], [s(t) ISA s(r(t_i))].

    {3 Extension to Function Types}

    In type systems, types of functions interact with subtyping in
    such a way that only the result type is covariant -- behaves like
    supertypes and subterms above -- while argument types are
    contravariant. To ensure proper behavior and have maximal
    flexibility, we would need to define "least upper bound
    unification" mutually recursively with glb-unification, for use in
    contravariant positions. To simplify we sacrifice flexibility: we
    use the standard first-order unification instead of
    glb-unification on function argument types.

    Formally, the definition of [ISA] extends to [funtype] as follows:

    [funtype( ; t_1, ..., t_{n-1}, t_n) ISA funtype( ; t'_1, ...,
    t'_{n-1}, t'_n)] if and only if for all substitutions [s] there is
    a substitution [r] such that [s(t)] and [r(t')] are both ground
    and [s(t_n) ISA r(t'_n)], [s(t_i) = r(t'_i)] for [1 <= i <= n-1].

Questions? Requests for clarification are welcome.

Hi,

It turns out to be a nice thing to implement terms without sharing
first, because the sharing-based unification, and the idea behind
sharing in general, has the unpleasant feature that it is imperative,
therefore terms as data structures are not persistent. Persistence is
necessary for parsing, where multiple partial solutions are pursued.
So the solution with substitutions instead of updating the data
structure has its unavoidable merits. I thought we could solve the
problem (when the time hopefully soon comes) by indeed returning
substitutions, but of instance variables (with reference cells inside)
for free (immutable) variables; but this won't work, because the
instantiation of a variable can also be refined during parsing.
Fortunately, we have "Term Rewriting and All That", and the solution
is to use *iterated substitutions* from exercise 4.22 (end of section
4.7). This should do the job for explicit sharing as well, with the
substitution (re)presenting the sharing.

Cheers.

Actually it means that there should be the covariant unification that
finds the greatest lower bound (with <= being ISA) and invariant
unification that just finds the substitution that makes terms equal;
and the covariant unification should use the invariant unification for
"funtype".

Hi,

> I assume "as" is the right concrete syntax keyword to introduce the
> ISA part of a term, right? "and"-separated list will be ok?
>
> I'm going to add a flag to mark ISA part terms that were built by
> "grammatical" inference (formerly known as "type inference"), to avoid
> displaying them. I don't see a counterexample (that it would lose
> information).

Yes, I think both these things are ok.

> In the future when we have terms with sharing, I think it is OK to
> show the whole unified subterm at which a variable is once, and then
> only the variable. E.g. in our example of a board (grid): [...]

Looks good, but of course we will get back to it when it is time.

Best!

Lukasz

I assume "as" is the right concrete syntax keyword to introduce the
ISA part of a term, right? "and"-separated list will be ok?

I'm going to add a flag to mark ISA part terms that were built by
"grammatical" inference (formerly known as "type inference"), to avoid
displaying them. I don't see a counterexample (that it would lose
information).

In the future when we have terms with sharing, I think it is OK to
show the whole unified subterm at which a variable is once, and then
only the variable. E.g. in our example of a board (grid):

x@R y; x@C z

would be displayed as:

x@Grid as R y and C z; x

On Sat, Jun 16, 2012 at 11:11 PM, Lukasz Stafiniak <luk...@gm...> wrote:
> I've found a simple solution for higher-order types (so called
> "funtype" in Speagram)! Nothing changes in the unification algorithm I
> presented for hierarchical types. Higher-order types automatically

*hierarchical terms

> become invariant (one cannot be strictly speaking a strict subtype of
> another, but they can unify).

Here "unify" in the standard first-order sense, not in the
hierarchical terms sense.

I've found a simple solution for higher-order types (so called
"funtype" in Speagram)! Nothing changes in the unification algorithm I
presented for hierarchical types. Higher-order types automatically
become invariant (one cannot be strictly speaking a strict subtype of
another, but they can unify). In other words, "funtype" is not
hierarchical: doesn't have the ISA part and cannot be inside ISA part.

On Sat, Jun 16, 2012 at 4:07 AM, Lukasz Stafiniak <luk...@gm...> wrote:
> New ''last-row'' number as Node.
> Let last-row 0 be Node.
> Let last-row n be R last-row n-1.
> New ''stack-row'' Node as Node.
> Let stack-row x@R y be z@C x; z@R stack-row y.
> Let stack-row x be C x.
> New ''board'' number number as Node.
> Let board 0 n be last-row n.
> Let board m n be stack-row board m-1 n.

Fajne, nie? Zanim się zabiorę powoli pomagać Ci z programowaniem, chcę
ogarnąć jeszcze tematy: programowanie / typy wyższego (lub
przynajmniej drugiego) rzędu, bo w początkowym sformułowaniu tego
zagadnienia "typowo typowego" zupełnie nie ma (a trzeba m.in.
wprowadzić kontrawariancję).

Myślałem że wyświetlanie termów hierarchicznych to też sprawa do
przemyślenia, jak upchać całą informację wyinferowaną przy parsowaniu
-- czy próbować pomijać część rzeczy które parsowanie potrafi
odtworzyć, potem pomyślałem że najlepiej wyświetlać całą informację,
termy wyżej w hierarchii na prawo od "as", np. "x@Grid as R y (as
v@Node) and C z (as v@Node)" ale i to już trochę masakra... Może
wbudować w termy pole czy dany podterm został w 100% wyinferowany z
gramatyki, wtedy powyższe da "x@Grid as R y and C z", to jest myśl.
BTW "x@" pochodzi z termu Var, to mógłby też być bezpośrednio "Grid as
R y and C z".

OK, dwa tematy.

Pozdrawiam.

Unlike in term rewriting, we often have more variables on the RHS than
in the LHS, since the variables are just a way to name new nodes.

*** Board example ***

I'll use numbers below. I'm in favor of having at least floating point
numbers as built-in, which if not eliminated by rewriting, are
translated into structures directly as structure function values.

I'll write it in some concrete syntax... parentheses are fully
optional ;-) but I'll use them for clarity, in the
functional-programming style.

First, we need a way to ignore terms, to use them for the
"side-effect" of constraining a variable. Let's also define the
parentheses. Sorry for not using the Speagram syntax, I like
succinctness.

x ';' y ISA y.
x; y => y.
'(' x ')' ISA x.
(x) => x.

Let's build the last row of a board:

'last-row' number ISA Node.
last-row 0 => x.
last-row n => R (last-row (n-1)).

Realize that "last-row 0 => x" is the same as "last-row 0 => Node",
because the variable "x" is inferred to be a "Node" -- being a
variable, it doesn't add any other constraint. Now let's stack more
rows in front:

'stack-row' Node ISA Node.
stack-row x@R y => z@C x; z@R (stack-row y).
stack-row x => C x.

The rule "stack-row x => C x" matches when the first rule doesn't
match, i.e. at the end of the row. Now let's do the loop:

'board' number number ISA Node.
board 0 n => last-row n.
board m n => stack-row (board (m-1) n).

Should I clarify anything? Perhaps I'll collect the definitions
together. Super-concise concrete syntax this time. In concrete syntax
the ISA part is after the argument part, while in the abstract syntax
I prefer to have it first...

Because the maximal sharing inside ISA part of definitions is
required, we can leave to the system to ensure it.

'Node'.
'R' Node ISA Node.
'C' Node ISA Node.
'Grid' ISA R Node AND C Node.
x ';' y ISA y.
x; y => y.
'(' x ')' ISA x.
(x) => x.
'last-row' number ISA Node.
last-row 0 => Node.
last-row n => R (last-row (n-1)).
'stack-row' Node ISA Node.
stack-row x@R y => z@C x; z@R (stack-row y).
stack-row x => C x.
'board' number number ISA Node.
board 0 n => last-row n.
board m n => stack-row (board (m-1) n).

Again, in a bit less terse, more Speagram syntax, only without "type"
/ "function". Also, without introducing variables before use.

Variables x, y, z.
New ''Node''.
New ''R'' Node as Node.
New ''C'' Node as Node.
New ''Grid'' as R Node and C Node.
New x '';'' y as y.
Let x; y be y.
New ''('' x '')'' as x.
Let (x) be x.
New ''last-row'' number as Node.
Let last-row 0 be Node.
Let last-row n be R (last-row (n-1)).
New ''stack-row'' Node as Node.
Let stack-row x@R y be z@C x; z@R (stack-row y).
Let stack-row x be C x.
New ''board'' number number as Node.
Let board 0 n be last-row n.
Let board m n be stack-row (board (m-1) n).

I assume above that variable bindings last only for one instruction.
Note that variables by themselves do not have "types", they just get
bound to ever more specific terms: explicitly by "@" and implicitly by
inference during parsing. E.g. in "last-row 0 => x" -- "Let last-row 0
be x." -- "x" is by parsing inference bound to new "Node".

Let's try how readable it is without parentheses:

Variables x, y, z.
New ''Node''.
New ''R'' Node as Node.
New ''C'' Node as Node.
New ''Grid'' as R Node and C Node.
New x '';'' y as y.
Let x; y be y.
New ''last-row'' number as Node.
Let last-row 0 be Node.
Let last-row n be R last-row n-1.
New ''stack-row'' Node as Node.
Let stack-row x@R y be z@C x; z@R stack-row y.
Let stack-row x be C x.
New ''board'' number number as Node.
Let board 0 n be last-row n.
Let board m n be stack-row board m-1 n.

On Sat, Jun 16, 2012 at 2:46 AM, Lukasz Kaiser <luk...@gm...> wrote:
> Hi.
>
>> I'm sorry, I still haven't finished the example with generating the
>> board. In the drafts I have a description of matching as an algorithm
>> to compute "ISA", therefore rewriting can be based on computing
>> "subterm ISA pattern".
>
> In the future, sure - but I think for now the rewriting we have is quite ok, no?

For things that already work, yes, but not even in the example with a
board: continuing with the "square" example, the term that is both an
R to the next in row term and a C to the next in column term, that
term is Grid while we want to match it as an R (or a C).

On Sat, Jun 16, 2012 at 2:46 AM, Lukasz Kaiser <luk...@gm...> wrote:
>
>> As for "Var", it has so many parameters to be compatible with the
>> current system, right? In the end it will most probably be "Var of
>> string * term option ref". See "Term Rewriting and All That" section
>> 4.8 "Unification of term graphs".
>
> Just the contrary - the parameters of the variable are necessary,
> also in principle, in any system I think. The reason is that we have
> functional variables - and we certainly want them (map, fold, etc :).)
> So variables take parameters when the var-function is applied, and
> it must be like this. And the integer - current arity - is just to know if
> we have a ternary function fully applied or rather a ternary function but
> still as a functional variable - unapplied. Maybe this could be removed,
> but I see no reason - it does not cost much, and is really useful some
> times. So I guess the variables have to be like that. And maybe there
> is some use of functional variables in the type system, or maybe not?

Thanks for clarification! I forgot :-)

Hi.

> I'm sorry, I still haven't finished the example with generating the
> board. In the drafts I have a description of matching as an algorithm
> to compute "ISA", therefore rewriting can be based on computing
> "subterm ISA pattern".

In the future, sure - but I think for now the rewriting we have is quite ok, no?

> As for "Var", it has so many parameters to be compatible with the
> current system, right? In the end it will most probably be "Var of
> string * term option ref". See "Term Rewriting and All That" section
> 4.8 "Unification of term graphs".

Just the contrary - the parameters of the variable are necessary,
also in principle, in any system I think. The reason is that we have
functional variables - and we certainly want them (map, fold, etc :).)
So variables take parameters when the var-function is applied, and
it must be like this. And the integer - current arity - is just to know if
we have a ternary function fully applied or rather a ternary function but
still as a functional variable - unapplied. Maybe this could be removed,
but I see no reason - it does not cost much, and is really useful some
times. So I guess the variables have to be like that. And maybe there
is some use of functional variables in the type system, or maybe not?

Lukasz

*** Matching ***

We need to further restrict the conditions on well-formed grammar definition.

We require that whenever for definitions "d1" and "d2" we have "d1 ISA
d2" if and only if there is exactly one graph homomorphism under
representation (2). It means that whenever a definition inherits from
another definition, it does so in only one way, i.e. the graph of the
definition has "full sharing" in the "ISA" part. (For example,
"A(B(X@D ; ), C(X@D ; ); )" which means that "A" inherits from both
"B" and "C" which both inherit from "D", but as required inherits "D"
in only one way.)

Then, checking "t1 ISA t2" should reduce to: find in "t1" the subterm,
"t1" itself or in the ISA part, corresponding to "t2", and perform
matching of "t2" (as pattern) with that subterm of "t1", using
standard first-order matching. Therefore, checking whether "term ISA
pattern" generates an assignment.

I could have gotten something wrong in the above; the theory needs
formal definitions, lemmas and proofs... But "theory should agree with
experiment", i.e. the simple algorithms :-)

Note that "type inference", i.e. parsing, performs unification of
"available" "type" and expected "type", not just checking of ISA
(which "type checking" would do) -- the result ISA the expected thing.
I don't like writing "type" because ISA is both transitive _and_
reflexive.

*** Rewriting ***

Using the above matching, rewriting works using the standard
first-order term rewriting scheme, and corresponds to graph rewriting
under representation (2). (Or at least I hope so.)

P.S. I planned to include *Board example* in this email, but decided
to get it out sooner. I'm not moving very fast because, well, we're
breaking some new ground :-)

2004	Jan	Feb	Mar	Apr	May	Jun	Jul	Aug (1)	Sep	Oct	Nov	Dec
2005	Jan (1)	Feb	Mar	Apr	May	Jun	Jul	Aug	Sep	Oct	Nov	Dec
2009	Jan	Feb	Mar (1)	Apr	May	Jun	Jul	Aug (17)	Sep (34)	Oct	Nov	Dec
2010	Jan	Feb (100)	Mar (122)	Apr (5)	May	Jun (17)	Jul (36)	Aug (9)	Sep (111)	Oct (92)	Nov (76)	Dec (26)
2011	Jan (3)	Feb (35)	Mar (36)	Apr (10)	May (9)	Jun (2)	Jul (3)	Aug (2)	Sep	Oct (7)	Nov (12)	Dec
2012	Jan (19)	Feb (1)	Mar (4)	Apr (1)	May (6)	Jun (69)	Jul (21)	Aug (12)	Sep (14)	Oct (1)	Nov (3)	Dec
2013	Jan (6)	Feb (1)	Mar (6)	Apr (3)	May (6)	Jun (1)	Jul	Aug	Sep	Oct (2)	Nov (3)	Dec
2014	Jan	Feb	Mar (6)	Apr	May	Jun	Jul	Aug	Sep	Oct	Nov	Dec
2015	Jan (4)	Feb	Mar	Apr	May	Jun	Jul	Aug	Sep	Oct	Nov (1)	Dec (3)
2016	Jan (6)	Feb (1)	Mar (3)	Apr (1)	May (3)	Jun (1)	Jul (1)	Aug (3)	Sep (2)	Oct (1)	Nov (1)	Dec (1)
2017	Jan	Feb (2)	Mar (1)	Apr	May	Jun	Jul (2)	Aug	Sep	Oct	Nov	Dec

toss-devel Mailing List for Toss (Page 5)

toss-devel — Toss develpment discussion