Re: [Toss-devel] Specification of Hierarchical Terms

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

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.