[Prev][Next][Index][Thread]
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:
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