headers
Colin B Jay | 11 Feb 1991 19:43
Picon

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
satisfying notion of adjunction in this setting (a local adjunction)
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)
(Continue reading)

Permalink | Reply | 0 comments |
headers
John C. Mitchell | 14 Feb 1991 14:53
Picon

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Stephen.Brookes | 2 Mar 1991 22:47
Picon

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
voronkov | 2 Mar 1991 22:52
Picon

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 
about 100 participants from the USSR  and  about  50  participants 
>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:
(Continue reading)

Permalink | Reply | 0 comments |

Gmane