[TYPES] What are congruence rules called?

[Philip Wadler]

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/
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-list/attachments/20170703/974310a9/attachment.ksh>