toss-devel Mailing List for Toss (Page 4)
Status: Beta
Brought to you by:
lukaszkaiser
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
(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
|
From: Lukasz S. <luk...@gm...> - 2012-07-29 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 <luk...@gm...> wrote: > Hi. > > I recently learned about YAGI from the paper below, > http://uoa.academia.edu/StavrosVassos/Papers/1674325/Action-Based_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 Tic-Tac-Toe 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 K. <luk...@gm...> - 2012-07-22 21:48:42
|
Hi. I recently learned about YAGI from the paper below, http://uoa.academia.edu/StavrosVassos/Papers/1674325/Action-Based_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 Tic-Tac-Toe 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 K. <luk...@gm...> - 2012-07-20 12:20:31
|
> I get "svn: generic failure" I just tried the following again in a new diectory. svn co --username=lukaszkaiser svn+ssh://luk...@sv.../p/toss/code-0/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 S. <luk...@gm...> - 2012-07-20 08:02:15
|
I get "svn: generic failure" On Wed, Jul 18, 2012 at 7:48 PM, Lukasz Kaiser <luk...@gm...> wrote: >> svn --username=yoursfusername co >> svn+ssh://you...@sv.../p/toss/code-0/trunk/Toss Toss |
From: Lukasz K. <luk...@gm...> - 2012-07-18 17:49:22
|
> svn --username=yoursfusername co > svn+ssh://luk...@sv.../p/toss/code-0/trunk/Toss Toss Sorry - of course replace "lukaszkaiser" with your username as well! Lukasz |
From: Lukasz K. <luk...@gm...> - 2012-07-18 17:48:22
|
Hi. Due to updates on sourceforge, the address of Toss SVN has changed. It is necessary to re-checkout the new svn (and delete the old, I suggest). The new checkout command for read-write access is: svn --username=yoursfusername co svn+ssh://luk...@sv.../p/toss/code-0/trunk/Toss Toss Lukasz |
From: Lukasz K. <luk...@gm...> - 2012-07-18 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 S. <luk...@gm...> - 2012-07-18 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 K. <luk...@gm...> - 2012-07-04 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 functional-like > typed programming language, instead go for TFS-based language for > expressing hypergraphs (still a programming language based on > rewriting) I do not like this idea. Sentences naturally have term-like 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 TFS-variables (with GLB) and type-variables (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 S. <luk...@gm...> - 2012-07-04 14:35:38
|
On Wed, Jul 4, 2012 at 3:29 PM, Lukasz Kaiser <luk...@gm...> 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 half-undo 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 functional-like typed programming language, instead go for TFS-based language for expressing hypergraphs (still a programming language based on rewriting) (3) have distinct TFS-variables (with GLB) and type-variables (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 K. <luk...@gm...> - 2012-07-04 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 half-undo 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 S. <luk...@gm...> - 2012-07-04 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 spelling-out 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 'if-then-else' 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 somehow-related types have LUB - add a different kind of variables, untyped LUB-variables. They would not stand for the GLB of what they match with, but the LUB of what they match with. So the TFS-like GLB-variables would be "sharing variables", and the LUB-variables would be "type variables". - Only the LUB-variables 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 S. <luk...@gm...> - 2012-07-04 08:43:21
|
http://aigamedev.com/open/interview/the-octagon-theory/ Cheers. |
From: Lukasz K. <luk...@gm...> - 2012-07-01 23:37:07
|
> It is simpler than I thought. :p To remove the problem that a term is > ISA-equivalent 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 S. <luk...@gm...> - 2012-07-01 23:18:16
|
It is simpler than I thought. :p To remove the problem that a term is ISA-equivalent 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 well-formed terms, reiterated when we formally introduce well-formedness: {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 symbol-number 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 well-formed 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 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,} {- 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 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 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 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"). 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 well-formed substitutions} by extending into a function over terms in the standard way a finite mapping from a set of variables to well-formed 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 well-formed term, well-formed substitutions return a well-formed 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 isa-matching} a term [p] against a term [t] (where [p] and [t] are well-formed) 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 well-formed substitution [R] and term [t], [R(t) ISA t]. There is probably no simpler algorithm to decide [t ISA p] than isa-matching [p] against [t]. We define {i eq-matching} a pattern [p] against a term [t] as the problem of finding a substitution [R] such that [t = R(p)]. Note that if eq-matching [p] against [t] exists, isa-matching also exists and is the same substitution. We define {i glb-unification} ({i Greatest Lower Bound Unification}) of two well-formed 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 glb-unification is of algorithmic value. We define {i eq-unification} of [t_1, t_2] as the standard (first-order) {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 glb-unification 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 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 there is a well-formed substitution [R] such that [R(t')=funtype( ; t_1, ..., t_{n-1}, 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 well-formed 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 well-formed if and only if [f(s_0; t_1, ..., t_n)] is well-formed. {3 Practical Considerations} We develop the isa-matching and glb-unification 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 eq-variants are possible. |
From: Lukasz K. <luk...@gm...> - 2012-07-01 15:21:51
|
> The move to left-linear rules is nice in that after introducing > sharing (according to the proposal), the semantics of non-linear 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 right-linear 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 S. <luk...@gm...> - 2012-07-01 03:53:44
|
On Sun, Jul 1, 2012 at 5:39 AM, Lukasz Stafiniak <luk...@gm...> wrote: > On Sun, Jul 1, 2012 at 5:07 AM, Lukasz Kaiser <luk...@gm...> wrote: >> >> Hmm - we currently enforce all our rules to be left-linear. >> Maybe we could handle the linear case first, and then >> join the non-linear case with sharing in the next step? >> (I know parsing must handle right sides as well, this is just a hope.) The move to left-linear rules is nice in that after introducing sharing (according to the proposal), the semantics of non-linear 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 S. <luk...@gm...> - 2012-07-01 03:39:43
|
On Sun, Jul 1, 2012 at 5:07 AM, Lukasz Kaiser <luk...@gm...> wrote: >> This is only (seriously) bad for non-linear 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 left-linear. > Maybe we could handle the linear case first, and then > join the non-linear 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, left-linear 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 K. <luk...@gm...> - 2012-07-01 03:08:33
|
> This is only (seriously) bad for non-linear 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 left-linear. Maybe we could handle the linear case first, and then join the non-linear case with sharing in the next step? (I know parsing must handle right sides as well, this is just a hope.) Lukasz |
From: Lukasz S. <luk...@gm...> - 2012-07-01 02:18:58
|
On Sun, Jul 1, 2012 at 12:57 AM, Lukasz Stafiniak <luk...@gm...> 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 non-linear terms, so semantically it seems tied with explicit sharing. (I.e. solving this problem should shed light on explicit sharing.) |
From: Lukasz S. <luk...@gm...> - 2012-06-30 22:57:53
|
The specs are still wrong, in particular currently a term / substitution is equivalent to its upper grounding w.r.t. ISA, which contradicts the remark (which is pretty much a requirement...) that isa-matching / glb-unification reduces to eq-matching / eq-unification (i.e. standard matching and MGU) when the latter exist. :p I'm "back at the drawing board" at the same time thinking about the central algorithm, glb-unification (if we have a straightforward algorithm, frankly we don't need formalization, but it's a nice to have, sort of like a test framework). On Sat, Jun 30, 2012 at 1:35 AM, Lukasz Stafiniak <luk...@gm...> wrote: > I've fixed the specification considerably. I've had a break since > Tuesday but I'm back since Thursday evening. |
From: Lukasz S. <luk...@gm...> - 2012-06-29 23:36:08
|
I've fixed the specification considerably. I've had a break since Tuesday but I'm back since Thursday evening. {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 t'] for some i, where [t=f(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 [t=f(s_1, ..., s_m; t_1, ..., t_n)] and [t'=f(s'_1, ..., s'_m; t'_1, ..., t'_n)]}} Actually we sometimes do not put a special case for the top symbol [Type] into algorithms, and therefore we rely on well-formed sets of declarations that no term except [Type] has no direct supertypes. 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, also 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,} {- 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 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, defined in the next section. {3 "Unification Theory" for Hierarchical Terms} 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 introduce an order on substitutions, by saying that [S ISA R] when for all [t], [S(t) ISA R(t)]. We define {i isa-matching} a term [p] against a term [t] (where [p] and [t] are well-formed) as the smallest substitution [R] such that [t ISA R(p)]. In context of matching, [p] is called a pattern. (There is probably no simpler algorithm to decide [t ISA p] than isa-matching [p] against [t].) We define {i eq-matching} a pattern [p] against a term [t] as the problem of finding a substitution [R] such that [t = R(p)]. Note that if eq-matching [p] against [t] exists, isa-matching also exists and is the same substitution. We define {i glb-unification} ({i Greatest Lower Bound Unification}) of two well-formed terms [t_1, t_2] as the greatest term [t] and smallest substitution [R] such that [f(;t,t) ISA R(f(;t_1,t_2))] (where [f] is an arbitrary symbol). We define {i eq-unification} of [t_1, t_2] as the standard (first-order) {i Most General Unifier, mgu} [U] of [t_1, t_2], together with the corresponding term [U(t_1)]. Note that if the mgu of [t_1, t_2] exists, the glb-unification also exists and is the same substitution. {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]. 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 well-formed 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 well-formed if and only if [f(s_0; t_1, ..., t_n)] is well-formed. |
From: Lukasz S. <luk...@gm...> - 2012-06-25 18:37:13
|
It's probably obvious, but I should state it "out loud". When we have hierarchical term "f(s_1, ..., s_m; t_1, ..., t_n)", it is like calling a class constructor. "t_1", ..., "t_n" are values for fields added to the object by class "f", and "s_1" up to "s_m" are calls to the constructors of superclasses of "f". So if "s_1 = g(...; u_1, ..., u_k)" then "u_1" ... "u_k" are values for fields added by the "g" superclass, etc. |
From: Lukasz S. <luk...@gm...> - 2012-06-25 15:17:57
|
On Wed, Jun 20, 2012 at 7:04 PM, Lukasz Stafiniak <luk...@gm...> wrote: > 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. 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). |
From: Lukasz S. <luk...@gm...> - 2012-06-21 10:34:55
|
On Wed, Jun 20, 2012 at 7:14 PM, Lukasz Kaiser <luk...@gm...> wrote: > >> (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. You are right, removing all encoding/decoding would be too much. Perhaps this heritage is worth to keep? Come to think of it, it wasn't my intention. What I'll do in step (4) is remove "term type" and SDtype (and rename SDfun to SDterm...) |