[Prev][Next][Index][Thread]
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@dcs.glasgow.ac.uk
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@math.tau.ac.il Mon Nov 15 11:59:19 1993
Date: Mon, 15 Nov 93 10:08:16 +0200
From: aa@math.tau.ac.il
To: wadler@dcs.gla.ac.uk
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@cs.kun.nl). The paper
is not published yet.
Arnon Avron
----- End Included Message -----
----- Begin Included Message -----
>From lafont@lmd7.univ-mrs.fr Wed Nov 10 18:48:18 1993
Date: Wed, 10 Nov 93 19:47:39 +0100
From: lafont@lmd7.univ-mrs.fr
To: Wadler <wadler@dcs.gla.ac.uk>
Subject: your questions
Dear Phil,
I have some remarks about your questions on the type list.
1a) Modulo derivability, your extended system is clearly equivalent
to ordinary sequent calculus. This means in particular that the
following rules are derivable, as you can check easily:
Gamma |- s:A Delta, x:A |- t:B
CUT ---------------------------------
Gamma, Delta |- t[s/x]:B
Gamma |- s:A Delta, x:B |- t:C
->L ---------------------------------
Gamma, Delta, y:A->B |- t[y s/x]:C
1b) First, we consider the pure proof theoretical version of your
problem WITHOUT TERMS.
Assume you have an admissable rule whose premisses contain EXACTLY
ONE VARIABLE OF CONTEXT. For example, the rule may be
Gamma, A |- B Delta, C, D |- E
---------------------------------
Gamma, Delta, F |- G
where A, B, C, D, E, F, G are composed formulae (not necessarily
variables of formulae).
Of course, the following sequents are provable:
A->B, A |- B C->D->E, C, D |- E
By definition, the following sequent is also provable:
A->B, C->D->E, F |- G
Now our rule is derived as follows:
Delta, C, D |- E .
---------------- .
Delta, C |- D->E .
----------------
Gamma, A |- B Delta |- C->D->E A->B, C->D->E, F |- G
------------- ----------------------------------------- CUT
Gamma |- A->B Delta, A->B, F |- G
----------------------------------------------- CUT
Gamma, Delta, F |- G
For example, Weak and Cont can be derived from CUT + your three
initial rules.
Note also that there would be no problem if a variable of context
occurs more than once (or not at all) in the CONCLUSION of the rule :
you can just repeat the cuts or use the structural rules.
I hope that the same argument applies to rules WITH TERMS. Note that
this argument is modular: It only uses the fact that we have
implication, not the fact that we have no other connective
1c) If you have connectives like disjunction, then the pure proof
theoretical version of your problem has a clear answer. For example,
if the formula NOT C -> A OR B is provable intuitionistically, then
the formula (NOT C -> A) OR (NOT C -> B) is also provable but the
following rule is clearly not derived
|- NOT C -> A OR B
-------------------------------
|- (NOT C -> A) OR (NOT C -> B)
However, the term corresponding to the proof of (NOT C -> A) OR
(NOT C -> B) is defined by case on the internal structure of the term
corresponding to the proof of NOT C -> A OR B, and you would
certainly not allow this in a rule. In fact, I guess you would only
allow substitution as a meta-operation on terms.
1d) The specialist of admissibility I know is Paul Roziere
(roziere@logique.jussieu.fr).
2) Concerning the second question, note that the resticted class of
context (eliminators) corresponds to operations which are interpreted
by linear maps in the coherence semantics of lambda-calculus (see the
book "Proof and Types" by J.Y. Girard & all, Cambridge).
Best wishes,
Yves.
----- End Included Message -----
----- Begin Included Message -----
>From wadler@dcs.gla.ac.uk Fri Nov 12 18:00:03 1993
Date: Fri, 12 Nov 93 17:59:40 GMT
From: wadler@dcs.gla.ac.uk
To: lafont@lmd.univ-mrs.fr
Subject: Re: your questions
Cc: wadler@dcs.gla.ac.uk
Thanks for the comment Yves.
Perhaps you've seen my later summary note, which included several
examples of rules that are admissable but not derivable.
You give another such example. But you also make several
other detailed remarks which I didn't quite follow. 1b
seemed to be a specific example of a general result, but
I don't see the general result you have in mind!
The weak commuting conversions work for any strict context.
A context uses its `hole' exactly once, and linear functions
are strict, so it makes sense that these notions should coincide.
Cheers, -- P
-----------------------------------------------------------------------
Professor Philip Wadler wadler@dcs.glasgow.ac.uk
Department of Computing Science tel: +44 41 330 4966
University of Glasgow fax: +44 41 330 4913
Glasgow G12 8QQ, SCOTLAND
----- End Included Message -----
----- Begin Included Message -----
>From lafont@lmd7.univ-mrs.fr Mon Nov 15 12:34:36 1993
Date: Mon, 15 Nov 93 10:54:20 +0100
From: lafont@lmd7.univ-mrs.fr
To: wadler@dcs.gla.ac.uk
Subject: Re: your questions
Dear Phil,
About 1b, a possible general result is the following.
Consider a calculus which is complete for a fragment of propositional
intuitionistic logic containing at least the implication and such
that the cut rule as well as the right -> rule are derivable.
Then, all admissible rules satisfying certain assumptions about the
variables of contexts are derivable.
Is it clear?
In fact, I have some difficulties to formalize your question because,
for example, I don't know if you consider that the following rule is
an instance of contraction:
Gamma, Gamma |- A
-----------------
Gamma |- A
Best wishes,
Yves.
----- End Included Message -----
----- Begin Included Message -----
>From types-dist-request@dcs.gla.ac.uk Thu Nov 4 14:29:18 1993
From: wadler@dcs.gla.ac.uk
Subject: Simple questions about simple types
Date: Thu, 4 Nov 93 12:41:25 GMT
To: types@dcs.gla.ac.uk
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:
Gamma |- u:B
Weak -----------------
Gamma, x:A |- u:B
Gamma, x:A, y:B |- v:C
Cont --------------------------
Gamma, z:A |- v[z/x,z/y]:C
(Use the cute name `typothesis' for the portion to the left
of the turnstyle. Assume throughout that order is irrelevant
in the typothesis, and that all variables in the typothesis are
distinct.)
On the other hand, say we use the following system.
Id ----------
x:A |- x:A
Gamma, x:A |- u:B
->I ---------------------------
Gamma |- lambda x. u : A->B
Gamma |- s:A->B Delta |- t:A
->E -------------------------------
Gamma, Delta |- s t : B
Gamma |- u:B
Weak -----------------
Gamma, x:A |- u:B
Gamma, x:A, y:B |- v:C
Cont --------------------------
Gamma, z:A |- v[z/x,z/y]:C
Does this system have any rules that are admissable but
not derived? (I'd be interested in any rules whatsoever,
whether they are intrinsically interesting or not.)
2. Commuting conversions
Say we have an equational typed theory with sums, including
the equations
(beta) (case Inl t of Inl x => v; Inr y => w) = v[t/x]
(beta) (case Inr u of Inl x => v; Inr y => w) = w[u/y]
(eta) (case s of Inl x => Inl x; Inr y => Inr y) = s
If we have categorical sums, we will have the commuting conversion
(cc) C[case s of Inl x => v; Inr y => w)
= case s of Inl x => C[v]; Inr y => C[w]
for *every* context C[]. By use of (eta) and (cc) with suitable choice
of C[], we can derive the useful rule
(*) case z of Inl x => v; Inr y => w
= case z of Inl x => v[Inl x/z]; Inr y => w[Inr y/z]
However, for (cc) to hold for all contexts C[] is incompatible
with the existence of fixpoints. Usually (and also in proof theory)
we have only `weak' commuting conversions, where the context must
have its hole as the principal connective of an eliminator (of
a function, product, or sum):
C[] ::= [] t
| fst []
| snd []
| case [] of Inl x => v; Inr y => w
Is (*) derivable from (beta), (eta), and (cc) with contexts restricted
in this way?
-----------------------------------------------------------------------
Professor Philip Wadler wadler@dcs.glasgow.ac.uk
Department of Computing Science tel: +44 41 330 4966
University of Glasgow fax: +44 41 330 4913
Glasgow G12 8QQ, SCOTLAND
----- End Included Message -----