headers
Ryu Hasegawa | 6 Apr 1989 15:31

implicit recursion

Date: Wed, 5 Apr 89 16:09:52 JST
Return-Path: <ryu@...>

>	IMPLICIT RECURSION IN THE POLYMORPHIC LAMBDA CALCULUS
>
>				Gavin Wraith
>	From: nax@... (Nax)
>	". . . is there a non-trivial sufficient 
>	condition on models (better, a characterization) for when
>	these constructions are intial [final]?"

In my master thesis, I studied such a problem on PL categories and obtained 
a sufficient condition, relating to parametric polymorphism.

In a category with a terminal object 1, any arrow k:A->B can be considered 
as representing a relation of A*B, that is, a:1->A relates to b:1->B 
under k if and only if a;k = b. This is naturally extended to S(k) for any 
multivariate endofunctor S(X-,X+), viz., a:1->S(A,A) relates to b:1->S(B,B) 
under S(k) if and only if a;S(1,k) = b;S(k,1) :1->S(A,B).

I will state the definition of parametricity informally.
Let T(X-,X+) be another endofunctor. An arrow t:S->T over X is 
called parametric if, for any A and B, and  k:A->B, that a relates to b 
under S(k) implies that a;t(A) relates to b;t(B) under T(k). This can be
taken for a categorical interpretation of Reynolds' parametricity, which
was originally defined on a set model.

In the thesis above, a parametric condition on PL categories is proposed,
and under it, it is showed, that (AX).(T(X)->X)->X is an initial T-algebra
where A stands for a universal quantification and T(X) is a positive
(Continue reading)

Permalink | Reply | 2 comments |
headers
David Wolfram | 18 Apr 1989 16:39
Picon
Picon

Numeral Systems

Date:    Mon, 17 Apr 89 16:14:42 BST

Is it possible to have a numeral system in pure simply typed lambda calculus
for which addition, multiplication, and subtraction or equality are lambda
definable?  This does not seem to be possible for simply typed Church numerals
by the Schwichtenberg - Statman result on extended polynomials.

David Wolfram.
Permalink | Reply | 0 comments |
headers
Carl Gunter | 21 Apr 1989 04:48

MFPS special session

Date: Thu, 20 Apr 89 17:49:36 -0400
Posted-Date: Thu, 20 Apr 89 17:49:36 -0400

This is a summary description of a special session of MFPS which may
be of interest to some types readers.

  SPECIAL SESSION ON THE SEMANTICS OF INHERITANCE POLYMORPHISM
                 Organized by Carl A. Gunter

A special session was held in conjunction with the New Orleans meeting
of the Conference on Mathematical Foundations of Programming Semantics
on Friday, March 31, 1989.  The purpose of the session was to bring
together researchers who have been working on the development of type
calculi for ``object oriented'' programming languages to discuss
differences of opinion and look for the best directions for future
research.  The session lasted three and a half hours and there were four
speakers:
  Val Breazu-Tannen (Penn)
  John Mitchell (Stanford)
  Atsushi Ohori (Penn)
  Luca Cardelli (DEC)
as well has a substantial period of discussion.  Here is a sort
description of the topics presented by the speakers:

  * Breazu-Tannen outlined the work of himself, Thierry Coquand, Carl
Gunter and Andre Scedrov (BCGS below) which has shown how to interpret
inheritance polymorphism as implicit coercion.  It was emphasized that
this concept is a semantic paradigm which works with many different
calculi and provides a rich supply of models.  A recently formulated
translation technique for inheritance involving the Amber recursion
(Continue reading)

Permalink | Reply | 0 comments |
headers
meyer | 26 Apr 1989 00:20
Picon

pam@...

Date:  Tue, 25 Apr 89 11:55:01 EST
From: pam@...
To: colloq@...
Subject: BU 4/26 colloq

			BOSTON UNIVERSITY
		      Computer Science Dept.
			111 Cummington St.

			 April 26, 1989
             Redex Capturing in Term Graph Rewriting

                           Bill Farmer

                     The MITRE Corporation
                           Bedford, MA

    Term graphs are a natural generalization of terms in which
structure sharing is allowed.  Structure sharing makes term graph
rewriting a time- and space-efficient method for implementing term
rewrite systems.  In term graph rewriting structure sharing schemes
can sometimes cause the left side of a rewrite rule to become a
subcomponent of the right side of the rule.  This phenomenon, called
"redex capturing", introduces cycles into the term graph which is
being rewritten -- even when the graph and the rule themselves do not
contain cycles.  In some applications redex capturing is undesirable,
such as in contexts where garbage collectors require that graphs be
acyclic.  In other applications, for example in the use of the
fixed-point combinator Y, redex capturing acts as a rewriting
optimization.  We show that in nearly all situations redex capturing
(Continue reading)

Permalink | Reply | 0 comments |

Gmane