[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <[email protected]>
Date: 7/4/17 11:15 (GMT-05:00)
To: "J. R. Hindley" <[email protected]>
Cc: Types list <[email protected]>
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 <[email protected]> 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 <[email protected]> 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
[email protected]
http://www.cse.chalmers.se/~abela/
