[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <[email protected]> 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 <[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. >
