[Toss-devel] Specification of Hierarchical Terms
Status: Beta
Brought to you by:
lukaszkaiser
|
From: Lukasz S. <luk...@gm...> - 2012-06-18 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 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.
|