[TYPES] What are congruence rules called?

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