[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Having a consistent way to name congruence rules is appealing, but since they
are generated from the structure of terms, wouldn't it be better to index their
names by the name of the syntactic form and the location of the relevant
subterm rather than by types? E.g., App-1, App-2. That approach seems to scale
more easily and clearly once you get beyond the lambda calculus.
-- Andrew
-------- Original message --------
From: Philip Wadler <[email protected]>
Date: 7/4/17 11:15 (GMT-05:00)
To: "J. R. Hindley" <[email protected]>
Cc: Types list <[email protected]>
Subject: Re: [TYPES] What are congruence rules called?
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Darn. Just as there are (possibly many) \beta rules at each type (e.g.,
\beta\arrow, \beta\times, \beta+_1, \beta+_2), I was hoping to have a
single greek letter for congruence rules, possibly with more than one at
each type. I was going to use \gamma\arrow_1, \gamma\arrow_2 for the two
congruence rules I gave, but wondered if there was a more traditional
choice than \gamma. Using either \mu or \nu seems problematic, since (like
\lambda) these often appear as binding operators in terms. Thank you for
the information! Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science
. /\ School of Informatics, University of Edinburgh
. / \ http://homepages.inf.ed.ac.uk/wadler/
On 4 July 2017 at 15:28, J. R. Hindley <[email protected]> wrote:
> Hi Phil, Francesco and Filippo,
>
> Yes, as Filippo and Francesco say, Greek names were first proposed for
> these two rules by Curry. He proposed
> $\nu$ for the first rule and $\mu$ for the second. ("Combinatory Logic"
> Volume 1 p. 59.)
>
> (Perhaps Curry also used them in one of his pre-1940 papers; I forget now.)
>
> Happy summer!
> Yours, Roger Hindley
>
> ----------------
> On 3 Jul 2017, at 19:04, Philip Wadler <[email protected]> wrote:
>
> > [ The Types Forum, http://lists.seas.upenn.edu/
> mailman/listinfo/types-list ]
> >
> > Reduction for the simply-typed call-by-value lambda calculus consists of
> > the β rule,
> >
> > (λx.N)V ⟹ N[x:=V]
> >
> > and the congruence rules
> >
> > L ⟹ L′
> > ------------
> > L M ⟹ L′ M
> >
> > M ⟹ M′
> > ------------
> > V M ⟹ V M′
> >
> > Question: Is there a standard greek letter for naming the congruence
> rules,
> > such as κ or γ? Or any other relevant naming convention?
> >
> > Cheers, -- P
> >
> >
> > . \ Philip Wadler, Professor of Theoretical Computer Science
> > . /\ School of Informatics, University of Edinburgh
> > . / \ http://homepages.inf.ed.ac.uk/wadler/
> > The University of Edinburgh is a charitable body, registered in
> > Scotland, with registration number SC005336.
>
>
>
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
