Path: utzoo!attcan!uunet!mcsun!ukc!edcastle!newshost!alti From: alti@staffa.ed.ac.uk (Thorsten Altenkirch) Newsgroups: comp.lang.functional Subject: Laziness & Symmetry - was: Purity and Laziness Message-ID: Date: 3 Jun 90 01:29:59 GMT Organization: Laboratory for Foundations of Computer Science. Lines: 68 In-reply-to: bjornl@tds.kth.se's message of 26 Jul 90 19:16:31 GMT In article 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)