alti@staffa.ed.ac.uk (Thorsten Altenkirch) (06/03/90)
In article <BJORNL.90Jul26211631@tarpon.tds.kth.se> bjornl@tds.kth.se (Bj|rn Lisper) writes:
if(b,x,x)
where the evaluation of b is non-terminating but the evaluation of x
terminates? If "naive" left-to-right evaluation order is assumed, the
computation will not terminate. On the other hand, it is reasonable to
define the semantics of the if-function so that such a call returns the
value of x. (After all, the value of x will be the answer regardless of what
b evaluates to). What about "referential transparency" here?
So it seems that if we extend the semantics of if by the reduction
rule
IF B THEN M ELSE M
------------------
M
we could solve all of the problems mentioned in the recent discussion.
So we can define a fair OR, because
OR(x,y) = IF x THEN TRUE ELSE y
is defined if either x or y evaluate to TRUE. ANd we can proceed in
defining a symmetric multiplication :
MULT(x,y) = IF (x=0) OR (y=0) THEN 0 ELSE x*y
[x*y is the strict version]. In fact the mentioned rule is rather
straightforward, because in categorical terms it is just the eta rule
for sums [more precisely it is the counit of the adjunction {Sorry}].
But there is one crucial problem with this rule : I think it destroys
the Church-Rosser-Property! In 1980 it was shown by Klop that adding a
rule for surjective pairing [this is the eta-rule for pairs] destroys
CR for the untyped lambda calculus. In fact he showed, that CR is
already destroyed, if we add :
D M M
-----
E
(where D,E are new constants). [see Barendregt's book , p. 403 ...].
So I guess the same applies to this rule. One might assume that
this doesn't apply for a typed system, but I don't think so. In fact
most type systems allow us to simulate the untyped lambda calculus
by the construction of a retract.
I am not sure wether an improved type system would solve the problem,
maybe it is already enough to have infinte data structures and partial
values.
However I suggest, that it is quite important to have symmetric
operations. It's not just that you have two OR's otherwise, but you
might have many copies of higher order combinators (if the definition
uses OR n times this gives 2^n copies).
Any suggestions ?
Thorsten
--
Thorsten Altenkirch
JCMB Room 1404 JANET: alti@uk.ac.ed.lfcs
LFCS, Dept. of Computer Science UUCP: ..!mcvax!ukc!lfcs!alti
University of Edinburgh ARPA: alti%lfcs.ed.ac.uk@nsfnet-relay.ac.uk
Edinburgh EH9 3JZ, UK. Tel: 031-667-1081 / 031 229 24 88 (p)