[Prev][Next][Index][Thread]
[mcvax!doc.ic.ac.uk!chlo@uunet.UU.NET: Abramsky's Simulation ordering]
From: mcvax!doc.ic.ac.uk!chlo@uunet.UU.NET
Date: Wed, 20 Jan 88 14:48:01 GMT
To: meyer@theory.lcs.mit.edu
Subject: Abramsky's Simulation ordering
Dear Professor Meyer,
You may certainly forward my comments on the distinctions between the
simulation ordering and Bohm trees to TYPES.
Regards, Luke (Ong)
--------------------
From: mcvax!doc.ic.ac.uk!chlo@uunet.UU.NET
Date: Mon, 11 Jan 88 9:54:14 GMT
To: meyer@theory.lcs.mit.edu
Subject: Abramsky's Simulation ordering
Dear Prof. Meyer,
With reference to the postscript you attached to Samson Abramsky's
e-mail dated 23 Nov, the ``simulation ordering'' M preord N
is not equivalent to two straight-forward modifications of
Bohm-tree ordering (to handle weak head normal forms) which
I have investigated. They are Longo tree ordering and weak Bohm
tree ordering.
The former was introduced by Giuseppe Longo in his
'83 APAL paper (entitled ``Set-theoretic Models of Lambda-Calculus:
theories, expansions and isomorphisms''). Longo tree differs from
Bohm tree in that the former maps all strongly unsolvable terms
(i.e. those terms not beta-convertible to abstractions or lambda-free
hnf's) to the tree with singleton node, \bot.
Also, each unsolvable term M is mapped to the tree with singleton node
``\lambda x_1 ... x_n. \bot'' where n is the order of unsolvability of M;
and the unsolvable term of order infinity is mapped to \top.
This correctly reflects the discriminatory power in the lazy regime ---
since the ``atomic'' observable is ``convergence to abstraction'',
one can then compare unsolvable terms of different orders.
Following Bohm trees, one can define variants of Longo trees
that respect eta-expansion. Such variants are not equivalent to
the simulation ordering preord.
Weak Bohm trees are defined in the same way as Bohm trees except that
all abstractions have the same weak Bohm trees. This is prompted
by the usual practice in lazy functional programming of not
evaluating ``under an abstraction''. We may consider weak Bohm
tree ordering closed under all contexts; still, such an ordering
is not equivalent to preord.
All the tree-based preorders considered above are, however,
strictly contained in preord.
The main reason why I think the simulation ordering preord cannot be
captured by a tree-like preorder (like Bohm tree)
defined inductively over substructures which respect certain
operational pre-conditions (like identifying all strongly
unsolvable terms) lies in the fact that
the definition of preord involves universal quantification
over closed terms. This forces uniformity in the interpretation
of free variables in a way which is incompatible with tree-based
ordering.
Perhaps not too surprisingly, preord induces a lambda theory
which is maximal in the class of lambda theories that differentiate
between unsolvable terms iff they have different orders of
unsolvability.
Regards,
Luke Ong.