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 <hindley-k881bfVVboVWk0Htik3J/[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.