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