11 Feb 19:43 1991

### Long beta/eta normal forms

```Date: Mon, 11 Feb 91 14:14:49 gmt

The presentation of eta-rules for exponentials and pairing in the
simply typed lambda calculus as contractions

lambda x.fx ==> f
<p1(c),p2(c)> ==> c

(pi is the ith projection) leads to a number of difficulties. Notably,
confluence only holds when the only terms of type 1 which appear are
instances of the constant *:1. One solution to this problem is to
perform the reuction in two stages: first beta-reduce as much as
possible and then perform some eta-expansions

f ==> lambda x.fx
c ==> <p1(c),p2(c)>

The question here is "Why are there two reduction systems in play?"

I came to this problem while trying to create a semantics for the
lambda calculus in which these reductions appear as 2-cells, or an
ordering, between the morphisms of a category. In order to have a
the local unit of the adjunctions must be given by eta-expansions. The
local triangle laws become

fa 	    ==> (lambda x.fx)a 		==> fa
lambda x.fx ==> lambda y.(lambda x.fx)y ==> lambda y.fy

pi(c) 	    ==> pi<p1(c),p2(c)> 	==> pi(c)
```

14 Feb 14:53 1991

### equational versions of fixed-point induction

```Date: Wed, 13 Feb 91 16:04:08 -0800

This is a question that came up in the context of a class I am teaching.
I wanted to find a simple, equational version of induction that
would let me prove some nontrivial equations between typed lambda
expressions involving a fixed-point operator FIX. The best I can
think of at the moment is the following rule, which relies on
reduction instead of an equational hypothesis.

F  -->>  M F
------------------
F  =   FIX M

This seems sound in any model equating terms with identical Bohm trees.
It becomes unsound if the hypothesis of the rule is replaced by the
equation F = M F. A conterexample is just to take M to be the identity.
Otherwise, the rule is similar to McCarthy's recursion induction rule.

My question is whether anyone else has something similar but better.

As an example of the kind of proof you can do with this, here is
a proof that the term G ::=  (FIX \f.\g. g(fg)) is equal to FIX.
Let F be the term Gx. Then we have F ->> x(Gx). So by the above rule,
F = FIX x. Hence \x.Gx = \x.FIX x, which gives the desired conclusion
by eta-equivalence. I assume that other reasonable proofs can be carried
out using this rule. If not, I would be interested in counterexamples.

John Mitchell

```

2 Mar 22:47 1991

### MFPS'91 Schedule

```Date: Sat, 2 Mar 91 14:31:28 EST

MATHEMATICAL FOUNDATIONS OF PROGRAMMING SEMANTICS (MFPS91)
March 25-28, 1991
Carnegie Mellon University
School of Computer Science
Pittsburgh, PA 15213

CONFERENCE SCHEDULE

SUNDAY 24 MARCH

6:00-10:00pm		Reception and Registration (Skibo Hall)

MONDAY 25 MARCH

9:00-10:00		Invited Talk
John Reynolds (Carnegie Mellon University)

10:00-10:40		Call-by-Value Combinatory Logic and the
Lambda-Value Calculus
Bruce F. Duba (Rice University)
John Gateley (Rice University)

10:40-11:00		Break

11:00-11:40		From Operational to Denotational Semantics
Scott F. Smith (The Johns Hopkins University)

11:40-12:20		A Simple Language Supporting Angelic Nondeterminism
```

2 Mar 22:52 1991

### 2nd Russian Conference on Logic Programming

```Date: Fri, 01 Mar 91 14:15:13 -0800

2nd Russian Conference on Logic Programming

SECOND ANNOUNCEMENT AND CALL FOR PAPERS

September 11-16, 1991, Leningrad (or possibly St.Petersburg)

The 2nd Russian Conference on Logic Programming  is  organized  by
the Russian  Association  for  Logic  Programming,  Joint  Venture
"Intertech"  (Moscow),  International  Laboratory  of  Intelligent
Systems (Novosibirsk) and Eurobalt Corp. It will take  place  from
September 11 to September 16. The first two  days  the  Conference
will be held in Leningrad (or, as we  hope,  in  St.  Petersburg).
>From September 13 it will continue on the board of a  ship  coming
along Neva River or  Ladoga  Lake.  The  Conference  program  will
include welcome party, 4 days of sessions and  conference  dinner.
The size of the ship allows to invite 150 participants. We  expect
>from abroad. The conference fee is 400 USD  for  participants  and
450 USD for accompanying persons. The conference fee includes full
board on the ship from the evening of September 11 to the  morning
of September 16.  Participants from the Eastern  countries  should
contact one of the co-chairs of the Organizing Committee about the
possibility to pay in the local currency. The official language is
English. Conference proceedings will be published in a volume of a
series  Lecture  Notes  in  Artificial  Intelligence  by  Springer
Verlag. Papers in all areas of Logic Programming are welcome. Send
5 copies of an extended abstract (up to 15 double spaced pages) to
the Conf. Secretary at the following address:
```