Screenshot instructions:
Windows
Mac
Red Hat Linux
Ubuntu
Click URL instructions:
Rightclick on ad, choose "Copy Link", then paste here →
(This may not be possible with some types of ads)
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}

S  M  T  W  T  F  S 






1

2

3
(2) 
4

5

6
(7) 
7
(14) 
8

9

10

11

12

13
(1) 
14
(13) 
15
(3) 
16
(7) 
17
(3) 
18
(2) 
19
(2) 
20
(10) 
21
(1) 
22

23

24

25
(2) 
26

27

28

29
(1) 
30
(1) 
From: Lukasz Stafiniak <lukstafi@gm...>  20120630 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 isamatching / glbunification reduces to eqmatching / equnification (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, glbunification (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 <lukstafi@...> wrote: > I've fixed the specification considerably. I've had a break since > Tuesday but I'm back since Thursday evening. 
From: Lukasz Stafiniak <lukstafi@gm...>  20120629 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 wellformed 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 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 [X(s)] and [X(s')] of variable symbol [X], [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"). In particular, we only allow {i wellformed substitutions}: substitutions that when applied to a wellformed term, return a wellformed term, defined in the next section. {3 "Unification Theory" for Hierarchical Terms} A {i wellformed 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 isamatching} a term [p] against a term [t] (where [p] and [t] are wellformed) 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 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] 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 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)]. Note that if the mgu of [t_1, t_2] exists, the glbunification 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 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 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'_{n1}, t'_n)] and [s(t_n) ISA t'_n], [s(t_i) = t'_i] for [1 <= i <= n1]. 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. 
From: Lukasz Stafiniak <lukstafi@gm...>  20120625 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 Stafiniak <lukstafi@gm...>  20120625 15:17:57

On Wed, Jun 20, 2012 at 7:04 PM, Lukasz Stafiniak <lukstafi@...> 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 > greatestlowerbound, including building of wellformed sets of > declarations, > > (4) remove the codingdecoding of types and adapt the grammar > representation to be based around wellformed sets of declarations, > > (5) switch the parser to use subtyping (replace "mgu" with "glb") and > start moving the builtin 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 ISAmatching (perhaps permanently keeping both strategies for rewriting). 
From: Lukasz Stafiniak <lukstafi@gm...>  20120621 10:34:55

On Wed, Jun 20, 2012 at 7:14 PM, Lukasz Kaiser <lukaszkaiser@...> wrote: > >> (4) remove the codingdecoding of types and adapt the grammar >> representation to be based around wellformed sets of declarations, >> >> (5) switch the parser to use subtyping (replace "mgu" with "glb") and >> start moving the builtin 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...) 
From: Lukasz Kaiser <lukaszkaiser@gm...>  20120620 18:06:15

> 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 
From: Lukasz Stafiniak <lukstafi@gm...>  20120620 17:52:20

On Wed, Jun 20, 2012 at 7:19 PM, Lukasz Stafiniak <lukstafi@...> 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... 
From: Lukasz Kaiser <lukaszkaiser@gm...>  20120620 17:49:45

> 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 wellformed set of > declarations. We will see how things work in practice, of course. Best! Lukasz 
From: Lukasz Stafiniak <lukstafi@gm...>  20120620 17:43:47

On Wed, Jun 20, 2012 at 7:32 PM, Lukasz Kaiser <lukaszkaiser@...> 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 wellformed set of declarations. 
From: Lukasz Kaiser <lukaszkaiser@gm...>  20120620 17:33:14

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 ministep 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 
From: Lukasz Stafiniak <lukstafi@gm...>  20120620 17:23:20

On Wed, Jun 20, 2012 at 7:19 PM, Lukasz Stafiniak <lukstafi@...> wrote: > On Wed, Jun 20, 2012 at 7:14 PM, Lukasz Kaiser <lukaszkaiser@...> 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 (15), so: (6) specify explicit sharing, (7) update the definition of terms to match the new specs, ... etc. 
From: Lukasz Stafiniak <lukstafi@gm...>  20120620 17:19:29

On Wed, Jun 20, 2012 at 7:14 PM, Lukasz Kaiser <lukaszkaiser@...> 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 >> greatestlowerbound, including building of wellformed sets of >> declarations, > > Sure  that will hopefully disambiguate all casts! But this step is is just about implementing the algorithms. >> (4) remove the codingdecoding of types and adapt the grammar >> representation to be based around wellformed sets of declarations, >> >> (5) switch the parser to use subtyping (replace "mgu" with "glb") and >> start moving the builtin 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? 
From: Lukasz Kaiser <lukaszkaiser@gm...>  20120620 17:14:53

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 > greatestlowerbound, including building of wellformed sets of > declarations, Sure  that will hopefully disambiguate all casts! > (4) remove the codingdecoding of types and adapt the grammar > representation to be based around wellformed sets of declarations, > > (5) switch the parser to use subtyping (replace "mgu" with "glb") and > start moving the builtin 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 
From: Lukasz Stafiniak <lukstafi@gm...>  20120620 17:05:19

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 greatestlowerbound, including building of wellformed sets of declarations, (4) remove the codingdecoding of types and adapt the grammar representation to be based around wellformed sets of declarations, (5) switch the parser to use subtyping (replace "mgu" with "glb") and start moving the builtin and core grammars and the standard library to use subtyping. Cheers! 
From: Lukasz Stafiniak <lukstafi@gm...>  20120620 00:57:15

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 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,} { 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 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 [X(s)] and [X(s')] of variable symbol [X], [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"). In particular, we only allow {i wellformed substitutions}: substitutions that when applied to a wellformed term, return a wellformed term: A {i wellformed 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 wellformed) 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 glbunification} ({i Greatest Lower Bound Unification}) of two or more wellformed terms [t_1, ..., t_n] as: given that there exist a wellformed term [t] and a wellformed 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 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 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'_{n1}, t'_n)] and [s(t_n) ISA t'_n], [s(t_i) = t'_i] for [1 <= i <= n1]. 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]. 
From: Lukasz Stafiniak <lukstafi@gm...>  20120619 23:08:00

On Tue, Jun 19, 2012 at 1:13 AM, Lukasz Stafiniak <lukstafi@...> wrote: > > 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,} > { 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 wellformed substitutions, they are not defined properly. I'll post the whole updated specification soon. 
From: Lukasz Stafiniak <lukstafi@gm...>  20120619 13:00:28

On Tue, Jun 19, 2012 at 1:13 AM, Lukasz Stafiniak <lukstafi@...> wrote: > > Formally, the definition of [ISA] extends to [funtype] as follows: > > [funtype( ; t_1, ..., t_{n1}, t_n) ISA funtype( ; t'_1, ..., > t'_{n1}, 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 <= n1]. 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_{n1}, t_n)] and [r(t')=funtype( ; t'_1, ..., t'_{n1}, t'_n)] are both ground and [s(t_n) ISA r(t'_n)], [s(t_i) = r(t'_i)] for [1 <= i <= n1]. 
From: Lukasz Stafiniak <lukstafi@gm...>  20120618 23:14:19

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 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,} { all subterms and supertypes of a term from the set are also in the set,} { there is at most one glbunification result for any two (or more) elements from the set.}} A {i wellformed term with respect to a set of declarations} given a wellformed set of declarations, is a term [t] such that its supertypes and subterms are wellformed (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 wellformed 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 wellformed substitutions}: substitutions that when applied to a wellformed term, return a wellformed term. We define matching a pattern [p] against a ground term [t] (where [p] and [t] are wellformed) 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 glbunification} ({i Greatest Lower Bound Unification}) of two or more wellformed terms [t_1, ..., t_1] as: given that there exist a wellformed term [t] and a wellformed 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 glbunification, for use in contravariant positions. To simplify we sacrifice flexibility: we use the standard firstorder unification instead of glbunification on function argument types. Formally, the definition of [ISA] extends to [funtype] as follows: [funtype( ; t_1, ..., t_{n1}, t_n) ISA funtype( ; t'_1, ..., t'_{n1}, 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 <= n1]. Questions? Requests for clarification are welcome. 
From: Lukasz Stafiniak <lukstafi@gm...>  20120618 15:23:01

Hi, It turns out to be a nice thing to implement terms without sharing first, because the sharingbased 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. 
From: Lukasz Stafiniak <lukstafi@gm...>  20120617 15:09:20

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". 
From: Lukasz Kaiser <lukaszkaiser@gm...>  20120617 14:22:36

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 
From: Lukasz Stafiniak <lukstafi@gm...>  20120617 13:49:53

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@... y; x@... z would be displayed as: x@... as R y and C z; x 
From: Lukasz Stafiniak <lukstafi@gm...>  20120616 21:18:27

On Sat, Jun 16, 2012 at 11:11 PM, Lukasz Stafiniak <lukstafi@...> wrote: > I've found a simple solution for higherorder types (so called > "funtype" in Speagram)! Nothing changes in the unification algorithm I > presented for hierarchical types. Higherorder 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 firstorder sense, not in the hierarchical terms sense. 
From: Lukasz Stafiniak <lukstafi@gm...>  20120616 21:11:56

I've found a simple solution for higherorder types (so called "funtype" in Speagram)! Nothing changes in the unification algorithm I presented for hierarchical types. Higherorder 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. 
From: Lukasz Stafiniak <lukstafi@gm...>  20120616 13:19:22

On Sat, Jun 16, 2012 at 4:07 AM, Lukasz Stafiniak <lukstafi@...> wrote: > New ''lastrow'' number as Node. > Let lastrow 0 be Node. > Let lastrow n be R lastrow n1. > New ''stackrow'' Node as Node. > Let stackrow x@... y be z@... x; z@... stackrow y. > Let stackrow x be C x. > New ''board'' number number as Node. > Let board 0 n be lastrow n. > Let board m n be stackrow board m1 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@... as R y (as v@...) and C z (as v@...)" 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@... 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. 