[Prev][Next][Index][Thread]
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@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
Question 1.
-----------------------------------------------------------------
From: cubric@triples.Math.McGill.CA (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
Gamma |- u:A
(NE) --------------
FV(u) |- u:A
where FV(u) means the typothesis of the typed variables which actually
appear in u. It won't be derivable because Gamma - FV(u) can be
arbitrarily long.
-----------------------------------------------------------------
Question 2.
-----------------------------------------------------------------
From: Andrzej_Filinski@JEROME.TIP.CS.CMU.EDU
For the second question, the answer is, perhaps surprisingly, no.
Let us look at just a simple instance of (*) at type bool = 1 + 1 with
the usual syntactic sugar:
(+) if z then z else z =?= if z then true else false
Even assuming that function spaces and products satisfy the usual
strong conditions (i.e., the CCC equations), (+) is not derivable, and
in fact there exist simple models in which it does not hold. For
example, consider a CBN language with side effects (say, Algol with
full higher-order functions). Then (beta), (eta), and (cc) for your
"strict" contexts are satisfied, but (+) fails when z is bound to an
expression with a side effect (such as incrementing a global cell).
However, (*) probably does hold if the only possible computational
effect is nontermination [which I guess could be axiomatized as some
form of idempotence condition on the relevant monad].
-----------------------------------------------------------------
----- 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 -----
----- Begin Included Message -----
>From cubric@triples.math.mcgill.ca Thu Nov 4 16:22:30 1993
Date: Thu, 4 Nov 93 11:17:58 EST
From: cubric@triples.Math.McGill.CA (Djordje Cubric)
To: wadler@dcs.gla.ac.uk
Dear Professor Wadler,
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
Gamma |- u:A
(NE) --------------
FV(u) |- u:A
where FV(u) means the typothesis of the typed variables which actually
appear in u. It won't be derivable because Gamma - FV(u) can be
arbitrarily long.
And what about some non interesting example as:
Gamma |- v:A->A
(NI)------------------------------
Gamma, x:A |- vvvv...vx:A
where vvvv...vx actually means: apply |v|-many v's on x (|v| is number of
symbols in v).
As for the second problem: well similar ones can be tough perhaps this one
is tough as well.
Best regards
Djordje Cubric
----- End Included Message -----
----- Begin Included Message -----
>From ma@src.dec.com Thu Nov 4 17:15:49 1993
To: wadler@dcs.gla.ac.uk
Subject: Re: Simple questions about simple types
Date: Thu, 04 Nov 93 09:15:26 -0800
From: ma@src.dec.com
Phil,
For question 1, off hand I can think only of silly examples:
E.g.,
Gamma, x:A |- x:A->A
--------------------
Gamma, x:A->A |- x:A
Here the top line is not derivable at all, so the rule is admissible.
But there may be others.
You must have meant something else.
Cheers,
Martin
----- End Included Message -----
----- Begin Included Message -----
>From herbelin@margaux.inria.fr Thu Nov 4 17:57:41 1993
Date: Thu, 4 Nov 93 18:55:45 +0100
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
To: wadler@dcs.gla.ac.uk
Subject: Admissible
Cc: herbelin@margaux.inria.fr
Hi,
one interesting admissible rule in sequent calculi is the cut rule.
An - artificial - translation of the cut rule in a natural deduction
framework is the following one:
First define a calculus of normal forms. This can be done for instance
by replacing the rule
Gamma |- s:A->B Delta |- t:A
->E -------------------------------
Gamma, Delta |- s t : B
by the rule
Gamma, x:A1->...->An->B |- ti:Ai (1<=i<=n)
App --------------------------------------------
Gamma, x:A1->...->An->B |- (x t1 ... tn) : B
In such a calculus, the rule ->E becomes an admissible rule (of which the
admissibility proof is a proof of normalisation).
Hoping this message is of interest for you,
Hugo Herbelin.
----- End Included Message -----
----- Begin Included Message -----
>From Andrzej_Filinski@JEROME.TIP.CS.CMU.EDU Thu Nov 4 20:57:43 1993
To: wadler@dcs.gla.ac.uk
Subject: Re: Simple questions about simple types
Date: Thu, 04 Nov 93 15:56:22 EST
From: Andrzej_Filinski@JEROME.TIP.CS.CMU.EDU
Phil,
For your first question, at least as currently stated, the answer is
probably no. Consider a rule like:
Gamma |- (lambda x.x) u : A
---------------------------
Gamma |- u : A
This is admissible, but (as far as I can tell) not derivable in either
of the systems you present.
For the second question, the answer is, perhaps surprisingly, also no.
Let us look at just a simple instance of (*) at type bool = 1 + 1 with
the usual syntactic sugar:
(+) if z then z else z =?= if z then true else false
Even assuming that function spaces and products satisfy the usual
strong conditions (i.e., the CCC equations), (+) is not derivable, and
in fact there exist simple models in which it does not hold. For
example, consider a CBN language with side effects (say, Algol with
full higher-order functions). Then (beta), (eta), and (cc) for your
"strict" contexts are satisfied, but (+) fails when z is bound to an
expression with a side effect (such as incrementing a global cell).
However, (*) probably does hold if the only possible computational
effect is nontermination [which I guess could be axiomatized as some
form of idempotence condition on the relevant monad].
I'm not all that interested in Q.1, but let me know if the above does
not convince you about Q.2.
-- Andrzej
----- End Included Message -----
----- Begin Included Message -----
>From Andrzej_Filinski@JEROME.TIP.CS.CMU.EDU Thu Nov 4 23:02:46 1993
To: wadler@dcs.gla.ac.uk
Subject: Re: Simple questions about simple types [addendum]
Date: Thu, 04 Nov 93 18:01:59 EST
From: Andrzej_Filinski@JEROME.TIP.CS.CMU.EDU
I wrote:
> For your first question, at least as currently stated, the answer is
> probably no.
Actually, what I answered here was the negation of your question,
i.e., "are all admissible rules in the second system also derivable?".
What I should have written was, "YES, there exist rules that are
admissible but not derivable (as shown by the example given)".
> For the second question, the answer is, perhaps surprisingly, also no.
This "no", however, should be correct, i.e., (*) is NOT derivable.
-- Andrzej
----- End Included Message -----