[Toss-devel] Specification of Hierarchical Terms

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

Hi,

The formal recipe is ready:


    {3 Specification of Hierarchical Terms}

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

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

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

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

    We need two more essential notions.

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

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

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

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

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

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

    {3 Extension to Function Types}

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

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

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


Questions? Requests for clarification are welcome.