[TYPES] What are congruence rules called?

[Beta Ziliani]

I second Andrew.

Don't ask me where, but I've seen also "App-L" and "App-R", and "@_l" and
"@_r" (the later for a system with an explicit app operator @).

My 1ct.

On Tue, Jul 4, 2017 at 2:44 PM, Andrew Myers <andru at cs.cornell.edu> wrote:

> [ 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 <wadler at inf.ed.ac.uk>
> Date: 7/4/17  11:15  (GMT-05:00)
> To: "J. R. Hindley" <hindley at waitrose.com>
> Cc: Types list <types-list at LISTS.SEAS.UPENN.EDU>
> 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 <hindley at waitrose.com> 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 <wadler at inf.ed.ac.uk> 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.
>