Re: [TYPES] What are congruence rules called?

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