[TYPES] What are congruence rules called?
Philip Wadler
wadler at inf.ed.ac.uk
Fri Jul 7 13:02:07 EDT 2017
Thank you to all for the many suggestions, and to Vincent for pointing out
that 'congruence' should perhaps be called 'compatibility'. Yours, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science
. /\ School of Informatics, University of Edinburgh
. / \ http://homepages.inf.ed.ac.uk/wadler/
On 3 July 2017 at 19:04, Philip Wadler <wadler at inf.ed.ac.uk> wrote:
> 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/20170707/d1611c90/attachment.ksh>
More information about the Types-list
mailing list