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