4 Nov 1993 13:41


Here are two simple questions about simply typed lambda calculus.
Does anyone know the answers?  I will collect the replies and post
a summary.  Many thanks,  -- Phil Wadler

Recall the two ways in which a new rule may be inherent in an existing
set of rules.  (This paragraph is cribbed from Hindley and Seldin's
Intro to Combinators and Lambda Calculus, pp 69--70.)  A new rule is
said to be *derived* if there is a deduction of its conclusion from its
premises.  A new rule is said to be *admissable* if whenever all the
premises are provable then so is the conclusion.  Every derived rule is
necessarily admissable, but not vice versa.

Say we take the following as our definition of typed lambda
calculus:

Id	-----------------
Gamma, x:A |- x:A

Gamma, x:A |- u:B
->I	---------------------------
Gamma |- lambda x. u : A->B

Gamma |- s:A->B    Gamma |- t:A
->E	-------------------------------
Gamma |- s t : B

Then the following rules are admissable, but not derived:


5 Nov 1993 19:47

Re: Simple questions about simple types


Thanks to all for their responses.  I give my favorite answers for the two
questions below: special thanks to Djordje Cubric and Andrzej Filinski
for these.  Thanks also to Tom Thomson of ICL, who spotted a typo in my
CONT' rule: B should have been A.  A copy of the question and all
responses I received appears at the end.  Cheers,  -- P
-----------------------------------------------------------------------
Department of Computing Science                    tel: +44 41 330 4966
University of Glasgow                              fax: +44 41 330 4913
Glasgow G12 8QQ, SCOTLAND

Question 1.
-----------------------------------------------------------------
From: cubric@... (Djordje Cubric)

Unless I missed some subtleties of the formal system I propose the
known'' example:

Gamma |- u:A
(Norm) ---------------
Gamma |- n(u):A

where n(u) is the beta-normal form of u. (I saw something like that for
Cut.) It won't be derivable because for any number N one can choose u so
that n(u) requires N  many steps to achieve.

Another example one might be



10 Nov 1993 18:49

Paper available by ftp


The following draft paper is available by anonymous ftp:

The emptiness problem for intersection types''

Pawel Urzyczyn
Institute of Informatics, Warsaw University

Abstract: We prove that it is undecidable whether a given intersection type
is non-empty, i.e., whether there exists a closed term of this type.

148.81.12.1
Directory:
/pub/users/urzy
Compressed files:
inhabit.ps.Z
inhabit.dvi.Z


10 Nov 1993 09:58

Bohm Festschrift announcement

Workshop on Theory of Computing

On the occasion of the 70th birthday of Corrado Boehm

Rome, December 3 1993

Dipartimento di Scienze dell'Informazione
Via Salaria 113, Roma, ITALY

PROGRAM
10.00 Chairman D.P.Bovet
Opening by A. Caracciolo di Forino
10.30 M. Nivat "Ravello thirty years later"
11.30 D.Scott "What do people really want
from a theory of functions?"

12.30-15.00 Lunch Breack

15.00 Chairman G. Ausiello
15.00 J.Y.Girard "Reflections on the Lambda Calculus"
16.00 S.Micali "Computation has short certificates"

17.00 Chairman R.De Nicola

Presentation of the volume "Lambda Calculi",
North Holland 1993, to Corrado Boehm

Organizing Committee:
G.Ausiello, Dip.D'Informatica e Sistemistica
Univ. Roma "La Sapienza"


12 Nov 1993 18:11

Termination of system F-bounded


Announce of paper: Termination of System F-bounded (Note).

The possibility of writing non-terminating terms in typed lambda-calculi is
strictly related to the possibility of solving recursive'' type equations
such as T = T->U, or T <: T->U <: T, when subtyping is defined.

This raises the question of whether the addition of F-bounded
quantification to system F-sub may allow non-terminating terms to be
written. In this note we prove that this is note the case. Our proof is
based on the computability method, and our approach is similar to the one
used in [Mitchell 86], and, more closely, to the proof of termination of
Fsub given in [Ghelli 90]. By the way, the proof in [Ghelli 90] is so full
of typos, that this note may be a better read also for those which are just
interested in Fsub termination.

One basic trick to make the proof go easy has been the choice of the set of
rules for F-bounded. I would like to compare my formalization which someone
else's preferred one, but I was not able to find out a complete
formalization of F-bounded. Can somebody help me?

A postscript file F-bounded.ps.gz containing the note may be retrieved by
anonymous ftp from site 'di.unipi.it', directory pub/ghelli. It is Mac-
produced, and I stripped font 'Times' out. If somebody will be able, or
unable, to print it, I would like to know that.

Enjoy.

Giorgio Ghelli.



11 Nov 1993 19:34

confluence, subject reduction for F^{omega} with products, eta


I would be grateful if anyone could tell me what the status is for:

- confluence
- subject reduction

for Girard's System F^{\omega} extended with products (at both type
and kind level) and *eta-conversion* (for both function and product
types, including the polymorphic Delta).

My understanding (from reading Gallier's excellent tutorial) is that
confluence for $\beta\eta$-conversion is a straightforward application
of Girard's Candidats sur le Reducibilit\'{e}.  My intuition is that
surjective pairing is locally confluent, hence confluence still holds
with surjective pairing.  Am I missing something here?  Are there any
complications for subject reduction?  Is any of this a corollary of
the proof theory worked out for System F with subtyping?

I am aware that matters become mildly nightmarish with dependent
types, I am personally interested in just the system described above.

Citable references would be very much appreciated, thanks
--dd

Spoken: Dominic Duggan	Internet: dduggan@...
Canada:	Dept of Computer Science, University of Waterloo,


17 Nov 1993 13:05

Re: Simple questions about simple types


and Yves Lafont (with a restricted positive result).  My thanks to them
both.  I've repeated the original question at the end.  -- P

-----------------------------------------------------------------------
Department of Computing Science                    tel: +44 41 330 4966
University of Glasgow                              fax: +44 41 330 4913
Glasgow G12 8QQ, SCOTLAND

----- Begin Included Message -----

>From aa@... Mon Nov 15 11:59:19 1993
Date: Mon, 15 Nov 93 10:08:16 +0200
From: aa@...
Subject: Re: Simple questions about simple types

in the east (See, e.g. Mints: "The derivability of admissible rules",
Journal of Soviet Mathematics 6 417-421 (1976)). They solve it, in fact,
for various fragment of Intuitionistic propositional logic- an equivalent
problem. A recent new solution, directly to the lambda-calculus case, is
given in W. DEkkers: "Inhabitation of types in the simply typed lambda
calculus", in which more references can be found (The address is: Dept. of
CS, University of Nijmegen, The Netherelands email: wil@...).
The paper
is not published yet.



16 Nov 1993 19:19

Wrong ftp address in 'Termination of System F-bounded'


I'm sorry, I have given wrong ftp instructions in my previous message
'Termination of System F-bounded'.

The correct ftp address and directory are:

ftp.di.unipi.it , directory  pub/Papers/ghelli.

Thanks to all who pointed the problem out to me.

Giorgio Ghelli

------------------------------------------------------------------------------
Giorgio Ghelli,    Universita' di Pisa, Dipartimento di Informatica,
Corso Italia 40, I-56125, Pisa, ITALY
E-mail: ghelli@...;  Phone: +39-50-510258;    Fax:
+39-50-510226
------------------------------------------------------------------------------


14 Nov 1993 20:41

unit-only LL is not trivial


>From Max Kanovich:

Here we focus on the study of the simplest fragments
of Linear Logic such as one-literal and constant-only ones
(the latter contains no literals at all) and demonstrate that
these extremely simple fragments are of the same expressive
power as the corresponding full versions.

According to one of the well-known approaches, the hierarchy of
natural fragments of Linear Logic can be developed in the
following way:
For a given fragment of Linear Logic LL{\sigma}
(its formulas are built up of literals and constants
by connectives from the set of connectives~$\sigma$,
constants are taken from \sigma),
we can reduce the number of the literals used to a fixed
number $k$ and study the corresponding fragment LL^k{\sigma}.

We study the simplest cases when $k$ is small, namely,
we will study the one-literal fragment LL1{\sigma} and
constant-only fragment LL0{\sigma}.

Actually, this approach is also quite traditional.

E.g., consideration of the one-literal fragment of
intuitionistic propositional logic allows us to obtain the full
characterization of this fragment and shed light on the
true nature of intuitionistic logic as a whole.



17 Nov 1993 18:21

Re: confluence, subject reduction for F^{omega} with products, eta

[Duggan asked about confluence and subject reduction for System F omega
extended with products and eta conversion.  Here is a reply from Ghelli,

[Note to contributors: When you supply an answer to a previous
question, please write a short introduction, so that I don't need to
write one for you!  Cheers,  -- P]

> System F with subtyping is not confluent w.r.t. beta-eta, hence the answer
> to this sub-question is NO.

> By the way F-sub admits an interesting
> confluent system which is beta-eta-top (top identifies terms of type Top)
> [Curien Ghelli]; extensions of beta-eta-top to products, for system F without
> subtyping, have been studied in [Curien Di Cosmo] and [Di Cosmo Kesner]
>
> Best Regards,
>
>    Giorgio Ghelli
>
> [Curien Ghelli] P.-L. Curien and G. Ghelli, Confluence and decidability of
> beta-eta-top reduction in Fsub, Information & Computation, to appear.
> A preliminary version in Proc. Conf. on Theoretical Aspects of Computer
> Software, Sendai, Japan, Springer-Verlag, Berlin, Lecture Notes in Comput.
> Sci. 526 (1991).
>
> [Curien Di Cosmo] P.-L. Curien,  R. Di Cosmo, Confluence in the Typed
> lambda-calculus Extended with Surjective Pairing and a Terminal Type, Proc.
`