15 Nov 2007 21:38

### Permutation of beta-redexes in lambda-calculus

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear all,

I have recently found it necessary to prove the following theorem (by a
series of adjournment properties), and was wondering if it rings a bell
to anyone.

Definition: Let gamma be a new reduction rule of lambda-calculus defined as
(lambda x.M) ((lambda y.N) P) ---> (lambda y.(lambda x.M) N) P
(avoiding capture of y in M, obviously)

Theorem: If M is SN for beta, then M is SN for beta+gamma.

The rule comes up in my framework for a call-by-value evaluation similar
to Moggi's lambdaC.
I'm sure that its termination (together with beta-reduction) must have
already come up in someone else's work...

Stephane Lengrand
lengrand@...


16 Nov 2007 00:48

### Re: Permutation of beta-redexes in lambda-calculus

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Stéphane,

Although not exactly what you are looking for and at the risk
that you may very well have heard of it already, I thought I might
mention a "mirror image" notion of permutation to the one you suggest.

<at>
/ \
<at>
/ \

you permute this other one

<at>
/ \
<at>
/ \

This has been developed by Laurent Regnier in 1990 [1]. He calls
it \sigma reduction and is formulated as follows:

((\x.U) V) W  --> (\x.(U W)) V    (x\notin W)
(\x.\y.U) V   --> \y.(\x.U) V     (y\notin V)

He proves that all \sigma-equivalent terms have the same longest
(beta) reduction to normal form. As a consequence \sigma-reduction is
perpetual. Also, you get a result corresponding to your theorem as a


16 Nov 2007 16:33

### Re: Permutation of beta-redexes in lambda-calculus

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello,

>      This [notion of redex permutation] has been developed by
> Laurent Regnier in 1990 [1]. He calls it \sigma reduction and is
> formulated as follows:
>
>      ((\x.U) V) W  --> (\x.(U W)) V    (x\notin W)
>      (\x.\y.U) V   --> \y.(\x.U) V     (y\notin V)

Thanks to Eduardo for mentioning this work. I should say that other
people had already some work on it, eg it is used (and maybe defined
for the first time) in an 87 de Vrijer paper (Exactly estimating
functionals and strong normalization).

On the other hand I have never heard of the CBV version that Stéphane
proposes.

Bests,
Laurent


29 Nov 2007 09:03

### Re: Permutation of beta-redexes in lambda-calculus

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

"Stéphane Lengrand (Work)" <Lengrand <at> LIX.Polytechnique.fr> writes:

> I have recently found it necessary to prove the following theorem (by a
> series of adjournment properties), and was wondering if it rings a bell
> to anyone.
>
> Definition: Let gamma be a new reduction rule of lambda-calculus defined as
> (lambda x.M) ((lambda y.N) P) ---> (lambda y.(lambda x.M) N) P
> (avoiding capture of y in M, obviously)
>
> Theorem: If M is SN for beta, then M is SN for beta+gamma.

Dear Stéphane,

A extremely similar theorem is proven in:

A. J. Kfoury, J. B. Wells.
New Notions of Reduction and Non-Semantic Proofs of β-Strong Normalization in Typed λ-Calculi.
LICS 1995.

For discussion of and pointers to related work (the original
“reduction with memory” method from Klop's 1980 Ph.D. thesis, de
technical report:

A. J. Kfoury, J. B. Wells.
Addendum to “New Notions of Reduction and Non-Semantic Proofs of β-Strong Normalization in Typed λ-Calculi”.
Computer Science Department, Boston University, Technical Report 95-007, 1995.


29 Nov 2007 18:18

### Re: Permutation of beta-redexes in lambda-calculus

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]


Hello,

Regarding the enclosed message, the following two references may also
be relevant:

1.   Hassan Ait-Kaci and Jacques Garrigue
Label-selective lambda-calculus: Syntax and confluence
Theoretical Computer Science, 151:353--383, 1995
URL: http://citeseer.ist.psu.edu/174691.html

2.   Jacques Garrigue and Hassan Ait-Kaci
The typed polymorphic label-lelective lambda calculus
in Proc. 21st ACM Symp. on Principles of Programming Languages
pp.35--47, ACM Press, 1994
URL: http://citeseer.ist.psu.edu/garrigue94typed.html

Regards,

-hak
--

--
Hassan Aït-Kaci  *  ILOG, Inc. - Product Division R&D
http://koala.ilog.fr/wiki/bin/view/Main/HassanAitKaci

30 Nov 2007 10:52

### [TYPES/announce] Small Workshop: DEPENDENTLY TYPED PROGRAMMING

[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Hi everybody,

as promised, we (Peter Morris, Tarmo Uustalu,  & myself) are
organizing a
small workshop on Dependently Typed Programming. This is a worskhop in
the tradition of previous workshops on "Dependent Types in
Programming" and "Dependently Typed Programming" which cover the use
of dependent types in programming in languages like Agda,Cayenne,Coq's
CIC, DML,Epigram, Omega,...

The workshop is taking place 18-20 February in Nottingham at the NCSL
conference centre. This is on campus but much nicer than the usual
student accomodation!

Currently we have one confirmed invited speaker: Lennart Augustsson.

For more details see the webpage: http://sneezy.cs.nott.ac.uk/darcs/
DTP08/

The deadline for talks and registration will be in January. However, if
you know you would like to come we would appreciate it if you could
email
us (dtpnott08@...) as soon as possible to register your
intentions. We have to promise a certain number of rooms and you will
also ensure you get accomodation at the NCSL.

Cheers,