headers
wadler | 4 Nov 1993 13:41
Picon
Picon
Favicon

Simple questions about simple types


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

1.  Admissable vs. derived rules

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

Permalink | Reply | 0 comments |
headers
wadler | 5 Nov 1993 19:47
Picon
Picon
Favicon

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
-----------------------------------------------------------------------
Professor Philip Wadler                        wadler@...
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)

Let me try to say something about your question 1.
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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Pawel Urzyczyn | 10 Nov 1993 18:49
Picon
Picon

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.

Internet address: 
        148.81.12.1
Directory:
       /pub/users/urzy
Compressed files:
       inhabit.ps.Z 
       inhabit.dvi.Z
Permalink | Reply | 0 comments |
headers
Simona RONCHI DELLA ROCCA | 10 Nov 1993 09:58
Picon

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

Permalink | Reply | 0 comments |
headers
Giorgio Ghelli | 12 Nov 1993 18:11
Picon
Picon

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

Permalink | Reply | 0 comments |
headers
Dominic Duggan | 11 Nov 1993 19:34
Picon
Picon

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, 
	Waterloo, Ontario, Canada N2L 3G1
Permalink | Reply | 0 comments |
headers
wadler | 17 Nov 1993 13:05
Picon
Picon
Favicon

Re: Simple questions about simple types


Further answers from Arnon Avron (with details about negative results)
and Yves Lafont (with a restricted positive result).  My thanks to them
both.  I've repeated the original question at the end.  -- P

-----------------------------------------------------------------------
Professor Philip Wadler                        wadler@...
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@...
To: wadler@...
Subject: Re: Simple questions about simple types

Your first question was answered negatively in the seventies by logicans
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.
(Continue reading)

Permalink | Reply | 1 comment |
headers
Giorgio Ghelli | 16 Nov 1993 19:19
Picon
Picon

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 
------------------------------------------------------------------------------
Permalink | Reply | 0 comments |
headers
Sergei N. Artemov | 14 Nov 1993 20:41
Picon

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

Permalink | Reply | 0 comments |
headers
Dominic Duggan | 17 Nov 1993 18:21
Picon
Picon

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,
with Duggan's comments interleaved.  -- Phil Wadler, moderator]

[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. 

Thanks, I already knew this.  

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

Permalink | Reply | 0 comments |

Gmane