You can subscribe to this list here.
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}

_{Dec}

S  M  T  W  T  F  S 

1
(7) 
2

3

4
(5) 
5

6

7

8

9

10

11

12

13

14

15

16

17

18
(4) 
19

20
(2) 
21

22
(1) 
23

24

25

26

27

28

29
(1) 
30
(1) 
31





From: Lukasz Kaiser <lukaszkaiser@gm...>  20120730 00:44:05

> 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 gridlike structure syntax is used, this seems to be much more readable, right? I just commited a change and moved TicTacToe, 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 
From: Lukasz Stafiniak <lukstafi@gm...>  20120729 16:41:53

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. On Sun, Jul 22, 2012 at 11:47 PM, Lukasz Kaiser <lukaszkaiser@...> wrote: > Hi. > > I recently learned about YAGI from the paper below, > http://uoa.academia.edu/StavrosVassos/Papers/1674325/ActionBased_Imperative_Programming_with_YAGI > and I looked at our rules in Toss and started thinking > that it could be more intuitive to represent directly > what needs to be added to and removed from relations, > instead of having these pairs of structures as we do now. > For example, in TicTacToe instead of the current RULE Cross: > [a  P:1 {}   ] > [a  P (a)   ] emb Q, P pre not WinQ() > we could just write > RULE Cross(a): +P(a) pre not P(a) and not Q(a) and not WinQ() > Or maybe even use "action" instead of "rule"? > This should be really easy to implement as our compiled > rule representation basically is just this: what to remove, > what to add, and pre. Maybe we should also have "new(e)" > and "del(e)" to add new elements and delete some of them? > What do you think about it? (Lukasz: is this what you have > been suggesting to me for some time? I hope you are not > angry that I need so much time to grow up to your advise!) > > Best! > > Lukasz 
From: Lukasz Kaiser <lukaszkaiser@gm...>  20120722 21:48:42

Hi. I recently learned about YAGI from the paper below, http://uoa.academia.edu/StavrosVassos/Papers/1674325/ActionBased_Imperative_Programming_with_YAGI and I looked at our rules in Toss and started thinking that it could be more intuitive to represent directly what needs to be added to and removed from relations, instead of having these pairs of structures as we do now. For example, in TicTacToe instead of the current RULE Cross: [a  P:1 {}   ] > [a  P (a)   ] emb Q, P pre not WinQ() we could just write RULE Cross(a): +P(a) pre not P(a) and not Q(a) and not WinQ() Or maybe even use "action" instead of "rule"? This should be really easy to implement as our compiled rule representation basically is just this: what to remove, what to add, and pre. Maybe we should also have "new(e)" and "del(e)" to add new elements and delete some of them? What do you think about it? (Lukasz: is this what you have been suggesting to me for some time? I hope you are not angry that I need so much time to grow up to your advise!) Best! Lukasz 
From: Lukasz Kaiser <lukaszkaiser@gm...>  20120720 12:20:31

> I get "svn: generic failure" I just tried the following again in a new diectory. svn co username=lukaszkaiser svn+ssh://lukaszkaiser@.../p/toss/code0/trunk/Toss Toss It wanted my password twice (don't know why) but then worked ok. Try it again please, maybe sf is having some problems. Lukasz 
From: Lukasz Stafiniak <lukstafi@gm...>  20120720 08:02:15

I get "svn: generic failure" On Wed, Jul 18, 2012 at 7:48 PM, Lukasz Kaiser <lukaszkaiser@...> wrote: >> svn username=yoursfusername co >> svn+ssh://yoursfusername@.../p/toss/code0/trunk/Toss Toss 
From: Lukasz Kaiser <lukaszkaiser@gm...>  20120718 17:49:22

> svn username=yoursfusername co > svn+ssh://lukaszkaiser@.../p/toss/code0/trunk/Toss Toss Sorry  of course replace "lukaszkaiser" with your username as well! Lukasz 
From: Lukasz Kaiser <lukaszkaiser@gm...>  20120718 17:48:22

Hi. Due to updates on sourceforge, the address of Toss SVN has changed. It is necessary to recheckout the new svn (and delete the old, I suggest). The new checkout command for readwrite access is: svn username=yoursfusername co svn+ssh://lukaszkaiser@.../p/toss/code0/trunk/Toss Toss Lukasz 
From: Lukasz Kaiser <lukaszkaiser@gm...>  20120718 16:36:12

> I realized that with terms=types, I need to make the syntax of syntax > definitions more cumbersome to avoid explosion of ambiguity. Instead > of a term be a Tp part of syntax definition by itself, I'll make > syntax_element_tp_sd be ''{'' ?t ''}'', i.e. the term needs to be > within curly brackets. Is it OK? (I'll update the .trs files.) Looks ok to me. Lukasz 
From: Lukasz Stafiniak <lukstafi@gm...>  20120718 16:12:12

I realized that with terms=types, I need to make the syntax of syntax definitions more cumbersome to avoid explosion of ambiguity. Instead of a term be a Tp part of syntax definition by itself, I'll make syntax_element_tp_sd be ''{'' ?t ''}'', i.e. the term needs to be within curly brackets. Is it OK? (I'll update the .trs files.) Regards. 
From: Lukasz Kaiser <lukaszkaiser@gm...>  20120704 14:53:10

Hi. > (1) drop the proposal, go back and start again with the simplest type > system with subtyping Well  this may be the best option, but let's keep it as the last resort, right? > (2) drop parametric polymorphism and the idea of a functionallike > typed programming language, instead go for TFSbased language for > expressing hypergraphs (still a programming language based on > rewriting) I do not like this idea. Sentences naturally have termlike structure when first parsed, and types seem to be natural constraints (maybe to me, sure). Of course  things later also have hypergraph structure, and if we can get it earlier, then great. But I can also just parse sentences to normal terms (= trees) and have another step to derive hypergraphs from sequences of sentences = tree terms. Looks like quite a natural way to me, and easier. > (3) have distinct TFSvariables (with GLB) and typevariables (with LUB) > > I understand that you oppose (2), just wanted to make sure. I'm not > interested in (1). I'll work towards (3) then. I guess that sums it up nicely. I hope we can still get something nice from it  else we can revert as in (1) and think about making hypergraphs from terms as the "next step"  after parsing and types and stuff. Maybe that could interest you in case (3) does not work. But for now let's stay optimistic and try out (3)  maybe it'll do just fine! Lukasz 
From: Lukasz Stafiniak <lukstafi@gm...>  20120704 14:35:38

On Wed, Jul 4, 2012 at 3:29 PM, Lukasz Kaiser <lukaszkaiser@...> wrote: > > Well  it is hard to say. I was never very concerned with lack > of expressiveness of the old basic speagram type system  it > was the speed of parsing we were aiming for. And my hope was > that 2 conceptual things will make it faster: keeping types with > terms (to avoid recomputing them) and subtyping. I am now > quite convinced that the first thing failed  we will have to get > back to it and do something to halfundo it to bring speed back. > But maybe it is not so relevant if the second thing works  how > about that? If you have GLB done, we should be able to test > it quite soon, right? And we will see then  I really hope that > some gains will start to show up! I'm not aiming at the speed of parsing, I'm aiming at a language for expressing hypergraphs directly. But I understand that you aim at the speed of parsing and I hope that the speed will return somewhat even before introducing subtyping to the library (the substitution algo might be to blame). I'll repeat the options: (1) drop the proposal, go back and start again with the simplest type system with subtyping (2) drop parametric polymorphism and the idea of a functionallike typed programming language, instead go for TFSbased language for expressing hypergraphs (still a programming language based on rewriting) (3) have distinct TFSvariables (with GLB) and typevariables (with LUB) I understand that you oppose (2), just wanted to make sure. I'm not interested in (1). I'll work towards (3) then. 
From: Lukasz Kaiser <lukaszkaiser@gm...>  20120704 13:29:49

Hi. > I implemented GLB yesterday, not compiled/tested yet, and it's really > simple. So I think the above is doable. > > What do you think? Well  it is hard to say. I was never very concerned with lack of expressiveness of the old basic speagram type system  it was the speed of parsing we were aiming for. And my hope was that 2 conceptual things will make it faster: keeping types with terms (to avoid recomputing them) and subtyping. I am now quite convinced that the first thing failed  we will have to get back to it and do something to halfundo it to bring speed back. But maybe it is not so relevant if the second thing works  how about that? If you have GLB done, we should be able to test it quite soon, right? And we will see then  I really hope that some gains will start to show up! Lukasz 
From: Lukasz Stafiniak <lukstafi@gm...>  20120704 09:21:06

I brutally realized that "Typed Feature Structures" do not have parametric polymorphism, not a trace of it. Heck, haven't I kept repeating that the proposal is not a type system. I still think that it is a promising language for spellingout hypergraphs/structures (with the direct translation I described). There are some options. The current specification already "oscillates" a bit beyond Typed Feature Structures in how it uses variables. At present it is somewhat inconsistent and I planned to bring it consistently back to TFSes by syntactically forbidding variables in place of supertypes. But now that I realize you are unlikely to give up parametric polymorphism... Consider the parametric declaration: 'If' boolean 'then' ?X 'else' ?X as ?X. What restrictions does it place on how it is used? If it was a TFS, it would mean that 'then' and 'else' branches are unified: either they are equal, or there is a common subtype that contains both branches (but the package is still shared by both positions). So you see, not at all the parametric type interpretation. With parametric types as we had them in "Middle Speagram", ?X would become the common supertype of both branches. With a top type (like the "type" in the proposal), using 'ifthenelse' could never fail in "Middle Speagram", it would just assume more and more general type. There is a way to get parametric polymorphism back but going much beyond Typed Feature Structures:  add the restriction that two classes can have at most one Least Upper Bound, this is the part that restricts expressiveness :(  add algo for computing Least Upper Bound  remove the "top" type so that only somehowrelated types have LUB  add a different kind of variables, untyped LUBvariables. They would not stand for the GLB of what they match with, but the LUB of what they match with. So the TFSlike GLBvariables would be "sharing variables", and the LUBvariables would be "type variables".  Only the LUBvariables would be allowed in place of supertypes. Their specification would be like the one before my recent fixing, i.e. ISA would be defined without them and extended to terms with them by existence of a substitution. I implemented GLB yesterday, not compiled/tested yet, and it's really simple. So I think the above is doable. What do you think? 
From: Lukasz Stafiniak <lukstafi@gm...>  20120704 08:43:21

http://aigamedev.com/open/interview/theoctagontheory/ Cheers. 
From: Lukasz Kaiser <lukaszkaiser@gm...>  20120701 23:37:07

> It is simpler than I thought. :p To remove the problem that a term is > ISAequivalent to its upper grounding, we make variables *strictly > more general* than their types. Actually, I've made a variable ISA > only another variable, while any other term t ISA a variable if t ISA > the variable's type. But I've kept checking for syntactic equality of > subterms that match the same variable, it makes sense and will be > helpful when moving to explicit sharing. This is nice to hear! :) > I probably should have written it in latex in the reference document, > rather than in ocamldoc. Yes. I have nothing against leaving it in the OCaml file, especially in the period when it changes a lot (like now). But please  when you feel that it is stable enough (already? after implementing?) then look at the section about terms in the reference and maybe simply replace it entirely. It will be definitely easier to read for me if it is there. Best! :) Lukasz 
From: Lukasz Stafiniak <lukstafi@gm...>  20120701 23:18:16

It is simpler than I thought. :p To remove the problem that a term is ISAequivalent to its upper grounding, we make variables *strictly more general* than their types. Actually, I've made a variable ISA only another variable, while any other term t ISA a variable if t ISA the variable's type. But I've kept checking for syntactic equality of subterms that match the same variable, it makes sense and will be helpful when moving to explicit sharing. I probably should have written it in latex in the reference document, rather than in ocamldoc. {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 {i direct supertypes} and terms [t_1, ..., t_n] are called {i direct subterms} of the term, or [X(s)], where [X] is a variable symbol and term [s] is called the type of the variable, and also its direct supertype (especially when we don't distinguish between variables and other terms). For a term [f(s_1, ..., s_m; t_1, ..., t_n)], resp. [X(s)], 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. A term [s] is a {i supertype} of [t] when it is a direct supertype of [t], or is a direct supertype of a supertype of [t]. A term [t'] is a {i subterm} of [t] when it is a direct subterm of [t], or is a direct subterm of either a subterm or a supertype of [t]. For terms [s] and [t], by [s=t] we denote sytanctic equality of [s] and [t]. We require certain conditions to hold on wellformed terms, reiterated when we formally introduce wellformedness: {ul { for any two occurrences of a variable [X(s)] and [X(s')], [s=s'],} { for any two supertypes [s] and [s'] of a term, if they have the same head symbol, they are syntactically equal: [s=s'].}} We define a path in a term as a sequence of symbolnumber pairs, where the first symbol is the head symbol of a term or its supertype, the first number is the position in the subterm list in that term or supertype, and the remaining of a path selects a subterm in the indicated subterm recursively. Formally, we say that a term [t] has a subterm [t'] at path [p=(f,i),p'], denoted [t_p=t'], when either [t] or one of its supertypes is equal to [f(...;t_1,...,t_i,...)] and [t_i_p'=t']; also, [t_e=t] for empty path [e]. 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]. [t ISA t'] holds if and only if one of the following holds: {ul { [s_i ISA t'] for some i, where [t=f(s_1, ..., s_m; t_1, ..., t_n)],} { [t' = X(s)] and [t ISA s],} { [t = X(s)], [t' = Y(s')], and [s ISA s'],} { the following two conditions both hold: {ul { [s_i ISA s'_i] for all [i], [t_i ISA t'_i] for all [i], where [t=f(s_1, ..., s_m; t_1, ..., t_n)] and [t'=f(s'_1, ..., s'_m; t'_1, ..., t'_n)]} { for any paths [p,p'] in [t'], if they select the same variable, then they are also paths in [t], and [t_p = t_p'].}}}} We consider a variable to be strictly more general than its type. Note that the second part of the last condition only needs to be checked at the root (i.e. only for the originally compared terms, since if it holds, it also holds for subterms and supertypes). We also ensure that there is a top symbol [type] with declaration [type( ; )], from which all other terms inherit (we rely on wellformed sets of declarations that no term except [type] has no direct supertypes). (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, also essential notions. A {i wellformed 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 glbunification result for any two (or more) elements from the set,} { no term except [type] has no direct supertypes,} { 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 three 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. (The condition "must have direct supertypes" also needs to be ensured in {!BuiltinLang}.) A {i wellformed term with respect to a set of declarations} given a wellformed set of declarations, is a term [t] such that: {ul { its supertypes and subterms are wellformed (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 of a variable [X(s)] and [X(s')] in [t], [s=s'],} { for any two supertypes [s] and [s'] of [t], if they have the same head symbol, they are syntactically equal: [s=s'].}} We limit all terms considered to terms that are wellformed with respect to a set of declarations (fixed by the context; we will drop constantly mentioning "w.r.t. a set of declarations"). The intent of the above definitions is to be a representational variant of {i Typed Feature Structures} known from the literature, for now reducing sharing constraints to syntactical equality. After introducing explicit sharing, they will fully represent Typed Feature Structures. {3 "Unification Theory" for Hierarchical Terms} We define {i wellformed substitutions} by extending into a function over terms in the standard way a finite mapping from a set of variables to wellformed terms, requiring that [X(s)] is mapped to [t] only when [t ISA s]. Additionally, all appearances of a variable in any term of the image of the substitution have the same type. When applied to a wellformed term, wellformed substitutions return a wellformed term. We introduce an order on substitutions, by saying that [S ISA R] when for all [t], [S(t) ISA R(t)]. We define {i isamatching} a term [p] against a term [t] (where [p] and [t] are wellformed) as the smallest (i.e. most informative) substitution [R] such that [t ISA R(p)]. In context of matching, [p] is called a pattern. Note that for any wellformed substitution [R] and term [t], [R(t) ISA t]. There is probably no simpler algorithm to decide [t ISA p] than isamatching [p] against [t]. We define {i eqmatching} a pattern [p] against a term [t] as the problem of finding a substitution [R] such that [t = R(p)]. Note that if eqmatching [p] against [t] exists, isamatching also exists and is the same substitution. We define {i glbunification} ({i Greatest Lower Bound Unification}) of two wellformed terms [t_1, t_2] as the greatest term [t] such that [f(;t,t) ISA f(;t_1,t_2)] (where [f] is an arbitrary symbol), together with the smallest substitution [R] such that [f(;t,t) ISA R(f(;t_1,t_2))]. Inclusion of the substitution in the definition of glbunification is of algorithmic value. We define {i equnification} of [t_1, t_2] as the standard (firstorder) {i Most General Unifier, mgu} [U] of [t_1, t_2], together with the corresponding term [U(t_1)=U(t_2)]. Note that if the mgu of [t_1, t_2] exists, the glbunification also exists and is the same substitution [U] (and the GLB term is the corresponding term [U(t_1)]). {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 glbunification, for use in contravariant positions. To simplify we sacrifice flexibility: we use the standard firstorder unification instead of glbunification on function argument types. We introduce function type symbol [funtype] and higherorder variables [X(s; t_1, ..., t_n)]. Formally, the definition of [ISA] extends to [funtype] as follows: For [t=funtype( ; t_1, ..., t_{n1}, t_n)], [t ISA t'] if and only if there is a wellformed substitution [R] such that [R(t')=funtype( ; t_1, ..., t_{n1}, t'_n)] and [t_n ISA t'_n]. The definition of [ISA] for [X(s_0; t_1, ..., t_n)] is the same as that for [f(s_0; t_1, ..., t_n)], only the conditions for wellformed terms change. A variable symbol can appear as both the term [X(funtype( ; s_1, ..., s_n, s_0))] and a term [X(s_0; t_1, ..., t_n)] as long as [t_i ISA s_i] for [1 <= i <= n]. Moreover, a term [f(funtype( ; t_1, ..., t_n, s_0); )] is wellformed if and only if [f(s_0; t_1, ..., t_n)] is wellformed. {3 Practical Considerations} We develop the isamatching and glbunification algorithms to meet the specifications above (as far as they are without error). But the computational burden of these algorithms needs to be explored, perhaps algorithms intermediate between isa/glb variants and eqvariants are possible. 
From: Lukasz Kaiser <lukaszkaiser@gm...>  20120701 15:21:51

> The move to leftlinear rules is nice in that after introducing > sharing (according to the proposal), the semantics of nonlinear rules > change: sharing in pattern requires sharing in matched (sub)term. That was the idea  to help with sharing in the future. I also thought about making the rules rightlinear and adding a "where" clause, e.g. instead of "f(x, x)" you would write "f(x, y) where y = x". This could allow to distinguish copying from sharing  we will probably need both, and we could have "f(x, y) where y = copy(x)" and f(x, y) where y == x", or something like this, with the second one meaning a shared term. But let's concentrate on glb/isa now, I guess this is enough to do ;). Lukasz 
From: Lukasz Stafiniak <lukstafi@gm...>  20120701 03:53:44

On Sun, Jul 1, 2012 at 5:39 AM, Lukasz Stafiniak <lukstafi@...> wrote: > On Sun, Jul 1, 2012 at 5:07 AM, Lukasz Kaiser <lukaszkaiser@...> wrote: >> >> Hmm  we currently enforce all our rules to be leftlinear. >> Maybe we could handle the linear case first, and then >> join the nonlinear case with sharing in the next step? >> (I know parsing must handle right sides as well, this is just a hope.) The move to leftlinear rules is nice in that after introducing sharing (according to the proposal), the semantics of nonlinear rules change: sharing in pattern requires sharing in matched (sub)term. > I've solved it (I'm still writing down the details, I'll post the > updated specs again). I've strayed away from the definition of "Typed > Feature Structures" unnecessarily worrying of introducing sharing too > early, but I can treat identity that later will be sharing as > (syntactic) equality for now. 
From: Lukasz Stafiniak <lukstafi@gm...>  20120701 03:39:43

On Sun, Jul 1, 2012 at 5:07 AM, Lukasz Kaiser <lukaszkaiser@...> wrote: >> This is only (seriously) bad for nonlinear terms, so semantically it >> seems tied with explicit sharing. (I.e. solving this problem should >> shed light on explicit sharing.) > > Hmm  we currently enforce all our rules to be leftlinear. > Maybe we could handle the linear case first, and then > join the nonlinear case with sharing in the next step? > (I know parsing must handle right sides as well, this is just a hope.) I've solved it (I'm still writing down the details, I'll post the updated specs again). I've strayed away from the definition of "Typed Feature Structures" unnecessarily worrying of introducing sharing too early, but I can treat identity that later will be sharing as (syntactic) equality for now. (And it plays nice with the "eq" variants of algorithms.) You are right, leftlinear matching leads to a faster algorithm because one can drop the search for positions repeating a variable in the pattern so as to check identity (before introducing explicit sharing, syntactical equality, later actual sharing) of subterms in the matched term. Recall that I'd like to generalize matching pattern (i.e. rule's LHS) "p" against term "t" as deciding "t ISA p". But I'd like this optimization to be optional (either a parameter or separate functions) to have a nice specification and its implementation. Best! 
From: Lukasz Kaiser <lukaszkaiser@gm...>  20120701 03:08:33

> This is only (seriously) bad for nonlinear terms, so semantically it > seems tied with explicit sharing. (I.e. solving this problem should > shed light on explicit sharing.) Hmm  we currently enforce all our rules to be leftlinear. Maybe we could handle the linear case first, and then join the nonlinear case with sharing in the next step? (I know parsing must handle right sides as well, this is just a hope.) Lukasz 
From: Lukasz Stafiniak <lukstafi@gm...>  20120701 02:18:58

On Sun, Jul 1, 2012 at 12:57 AM, Lukasz Stafiniak <lukstafi@...> wrote: > The specs are still wrong, in particular currently a term / > substitution is equivalent to its upper grounding w.r.t. ISA This is only (seriously) bad for nonlinear terms, so semantically it seems tied with explicit sharing. (I.e. solving this problem should shed light on explicit sharing.) 