[TYPES] What are congruence rules called?
Filippo Sestini
sestini.filippo at gmail.com
Tue Jul 4 05:59:29 EDT 2017
Hello,
Not really that common in literature, but in Hindley and Selding’s book,
Lambda Calculus and Combinators, they use respectively ν and μ
to name those congruence rules, both in the untyped and the typed case.
They claim to have taken that from Curry & Feys.
Best regards
--
Filippo Sestini
sestini.filippo at gmail.com
(+39) 333 6757668
> On Jul 3, 2017, at 8:04 PM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:
>
> [ 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.
More information about the Types-list
mailing list