[TYPES] What are congruence rules called?

[Andreas Abel]

On 04.07.2017 18:44, Andrew Myers wrote:
> Having a consistent way to name congruence rules is appealing, but since they are generated from the structure of terms, wouldn't it be better to index their names by the name of the syntactic form and the location of the relevant subterm rather than by types? E.g., App-1, App-2. That approach seems to scale more easily and clearly once you get beyond the lambda calculus.
> -- Andrew

+1. That sounds most reasonable.

> -------- Original message --------
> From: Philip Wadler <wadler at inf.ed.ac.uk>
> Date: 7/4/17  11:15  (GMT-05:00)
> To: "J. R. Hindley" <hindley at waitrose.com>
> Cc: Types list <types-list at LISTS.SEAS.UPENN.EDU>
> Subject: Re: [TYPES] What are congruence rules called?
> 
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 
> Darn. Just as there are (possibly many) \beta rules at each type (e.g.,
> \beta\arrow, \beta\times, \beta+_1, \beta+_2), I was hoping to have a
> single greek letter for congruence rules, possibly with more than one at
> each type. I was going to use \gamma\arrow_1, \gamma\arrow_2 for the two
> congruence rules I gave, but wondered if there was a more traditional
> choice than \gamma. Using either \mu or \nu seems problematic, since (like
> \lambda) these often appear as binding operators in terms. Thank you for
> the information! Cheers, -- P
> 
> .   \ Philip Wadler, Professor of Theoretical Computer Science
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ http://homepages.inf.ed.ac.uk/wadler/
> 
> On 4 July 2017 at 15:28, J. R. Hindley <hindley at waitrose.com> wrote:
> 
>> Hi Phil, Francesco and Filippo,
>>
>> Yes, as Filippo and Francesco say, Greek names were first proposed for
>> these two rules by Curry. He proposed
>> $\nu$ for the first rule and $\mu$ for the second.  ("Combinatory Logic"
>> Volume 1 p. 59.)
>>
>> (Perhaps Curry also used them in one of his pre-1940 papers; I forget now.)
>>
>> Happy summer!
>>    Yours, Roger Hindley
>>
>> ----------------
>> On 3 Jul 2017, at 19:04, 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.
>>
>>
>>
> 
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/