[ 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.
