Re: [TYPES] What are congruence rules called?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear Philip,

In Curry's Combinatory Logic, Volume I (section 2D)  congruence rules are
labeled with greek letters. I do not know whether this is the satandard
notation, but I am sure I occasionally met the same notation in other
books/papers.

All the best,
Francesco Gavazzo

2017-07-03 20:04 GMT+02:00 Philip Wadler <[email protected]>:

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