headers
Stefano Berardi | 7 Oct 2008 15:13
Picon
Favicon

[TYPES/announce] FINAL CALL for Types 2008 Post-Proceedings - Deadline: October 15, 2008

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

FINAL CALL for papers: TYPES 2008 Post-Proceedings

[As usual for the post-proceedings of the TYPES workshops,
submissions are not restricted to works presented at the workshop,
nor then authors are expected to be formally involved in the Types project.]

****************************************************************************

ABSTRACT AND PAPER SUBMISSION DEADLINE:  Wednesaday, October 15, 2008
NOTIFICATION OF ACCEPTANCE: Monday, December 15, 2008
FINAL VERSION DUE: Monday, January 19, 2009

****************************************************************************

The Post-Proceedings of the TYPES 2008 Annual Workshop (see 
http://types2008.di.unito.it/)
will be published, after a formal referee process,
as a volume of the Lecture Notes in Computer Science (LNCS) series.
Previous TYPES Post-Proceedings include
LNCS volumes 4941, 4502, 3895, 3085, 2646, 2277, 1657, 1512, 1158, 996 
and 806.
We hope this volume will give a good account of the papers presented at 
the workshop
and of recent research in the field in general.

TOPICS
(Continue reading)

Permalink | Reply | 0 comments |
headers
Andrei Popescu | 14 Oct 2008 06:24
Picon
Favicon

questiuon about strong normalization in untyped lambda-calculus

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

Apologies for asking an untyped question on a typed forum. :)

Assume (pure) untyped lambda calculus under beta reduction (and the infix notation for application
associates to the left as usual).   

I would like to know if there exists a set A of strongly normalizing terms such that the following holds:

For all terms T, 
  [T is in A]
 iff 
  [the term T T_1 ... T_n is strongly normalizing 
   for all natural numbers n and terms T_1,...,T_n in A]

I do not even know where to start for trying to construct such a set (a greatest fixed point definition is not
possible, since the property is contravariant).  Or is there any obvious (or known) reason for why such
a set could not exist?

Thank you in advance for any hint on this, 
   Andrei Popescu
Permalink | Reply | 11 comments |
headers
Robin Adams | 15 Oct 2008 17:01
Picon
Favicon

Re: questiuon about strong normalization in untyped lambda-calculus

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

On Tuesday 14 October 2008 05:24:03 Andrei Popescu wrote:
>
> I would like to know if there exists a set A of strongly normalizing terms
> such that the following holds:
>
> For all terms T,
>   [T is in A]
>  iff
>   [the term T T_1 ... T_n is strongly normalizing
>    for all natural numbers n and terms T_1,...,T_n in A]

There cannot be such a set.

Proof: Suppose A satisfies the conditions above.  For any T_1, ..., T_n in A, 
we have

T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A).
Hence (\x.xx)T_1 T_2 ... T_n is strongly normalizing.
Therefore, \x.xx is in A.
Therefore, (\x.xx)(\x.xx) is strongly normalizing.

This is a contradiction.

--
Robin Adams <robin@...>
Royal Holloway, University of London
(Continue reading)

Permalink | Reply | 9 comments |
headers
Mariangiola Dezani | 16 Oct 2008 10:00
Picon
Favicon

Re: questiuon about strong normalization in untyped lambda-calculus

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

> For all terms T,
>  [T is in A]
> iff
>  [the term T T_1 ... T_n is strongly normalizing
>   for all natural numbers n and terms T_1,...,T_n in A]

a strict subset of A is the set PSN of persistently strongly  
normalizing terms defined by

[T is in PSN]
iff
  [the term T T_1 ... T_n is strongly normalizing
   for all natural numbers n and strongly normalizing terms T_1,...,T_n]

The set PSN has been characterised (also with types) in:

M. Tatsuta and M. Dezani-Ciancaglini.  Normalisation is Insensible to  
Lambda-term Identity or Difference,   LICS'06.  In Rajeev Alur  
ed(s).,  pages 327-336,  2006,  IEEE Computer Society. http://www.di.unito.it/ 
˜dezani/papers/td.pdf

Characterisations of other sets of lambda terms related to  
normalization properties can be found in:

M. Dezani-Ciancaglini, F. Honsell and Y. Motohama.  Compositional  
Characterization of λ-terms using Intersection Types,   Theoretical  
Computer Science,  340(3):459-495,  2005. http://www.di.unito.it/~dezani/papers/tcsf.pdf
(Continue reading)

Permalink | Reply | 0 comments |
headers
Luigi.Liquori@work | 16 Oct 2008 15:43
Picon
Picon
Favicon

Reference to typed first class pattern matching

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

Dear Michael,

The Typed Rewriting calculus can be one possible reference.

http://rho.loria.fr/

Best
Luigi

-----------------
  Luigi Liquori, H.d.R., Ph.D.
  INRIA Researcher, Sophia Antipolis Méditerranée
  LogNet Research Team
  Vox	: +33 4 92 38 71 93
  Fax		: +33 4 92 38 50 29
  Hom	: +33 4 93 67 09 72
  GsmWork	: +33 6 78 35 80 88
  GsmPerso1	: +33 6 65 39 51 32
  GsmPerso2	: +39 3 49 16 56 45 1
  SIP		: luigi_liquori@...
  Url		: www-sop.inria.fr/members/Luigi.Liquori
  Url		: www.inria.fr/recherche/equipes/lognet.en.html
  Email	: Let (*,#)=(., <at> ) in Luigi*Liquori#inria*fr
  Snailm	: INRIA, 2004 Route des Lucioles - BP 93
		  FR-06902 Sophia Antipolis, France
ü
	Pensez à la planète et n'imprimez ce message que si nécessaire !
	Earth will kind ask you to print this message only if really needed!
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jonathan Seldin | 16 Oct 2008 21:32
Picon

Re: questiuon about strong normalization in untyped lambda-calculus

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

I think this proof is invalid.  The inference

> T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A).
> Hence (\x.xx)T_1 T_2 ... T_n is strongly normalizing.

seems to use the inference

If M reduces to N and N is SN, so is M.

This is false.  Consider

(\uv.u)(\x.x)((\z.zz)(\z.zz)).

This term is clearly not SN, but it reduces to (\x.x), which is SN  
(and is, in fact, in normal form).

On 15-Oct-08, at 9:01 AM, Robin Adams wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list 
>  ]
>
> On Tuesday 14 October 2008 05:24:03 Andrei Popescu wrote:
>>
>> I would like to know if there exists a set A of strongly  
>> normalizing terms
>> such that the following holds:
>>
>> For all terms T,
(Continue reading)

Permalink | Reply | 8 comments |
headers
Tillmann Rendel | 17 Oct 2008 00:01
Picon
Picon
Favicon

Re: questiuon about strong normalization in untyped lambda-calculus

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

Jonathan Seldin wrote:
> I think this proof is invalid.  The inference
> 
>> T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A).
>> Hence (\x.xx)T_1 T_2 ... T_n is strongly normalizing.
> 
> seems to use the inference
> 
> If M reduces to N and N is SN, so is M.
> 
> This is false.  Consider
> 
> (\uv.u)(\x.x)((\z.zz)(\z.zz)).
> 
> This term is clearly not SN, but it reduces to (\x.x), which is SN  
> (and is, in fact, in normal form).

I don't think this is a problem here. Since T_1, T_2 ... T_n are SN, 
every reduction strategy will reduce

   (1)    (\x.xx) T_1 T_2 ... T_n

in a finite number of steps to a term of the form

   (2)    U_1 U_1 U_2 ... U_n

with T_i reduces to U_i. On the other hand, the SN term
(Continue reading)

Permalink | Reply | 1 comment |
headers
Derek Dreyer | 17 Oct 2008 09:29
Picon

Re: questiuon about strong normalization in untyped lambda-calculus

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

Actually, Jonathan, I'm pretty sure this proof step is perfectly
valid, but the lemma you were assuming it depended on is too strong.
The appropriate one to use is the "head expansion" lemma:

If P[Q/x] T_2 ... T_n is SN, and Q is SN, then (\x.P) Q T_2 ... T_n is SN.

Instantiate P = xx, and Q = T_1.

Derek

On Thu, Oct 16, 2008 at 9:32 PM, Jonathan Seldin
<jonathan.seldin@...> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> I think this proof is invalid.  The inference
>
>> T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A).
>> Hence (\x.xx)T_1 T_2 ... T_n is strongly normalizing.
>
> seems to use the inference
>
> If M reduces to N and N is SN, so is M.
>
> This is false.  Consider
>
> (\uv.u)(\x.x)((\z.zz)(\z.zz)).
>
> This term is clearly not SN, but it reduces to (\x.x), which is SN
(Continue reading)

Permalink | Reply | 0 comments |
headers
Laurent Regnier | 17 Oct 2008 14:29
Picon
Favicon

Re: questiuon about strong normalization in untyped lambda-calculus

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

Hello,

> The inference
> 
>> > T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A).
>> > Hence (\x.xx)T_1 T_2 ... T_n is strongly normalizing.
> 
> seems to use the inference
> 
> If M reduces to N and N is SN, so is M.
> 
> This is false.

Actually this is false in general but true in the case investigated here. More
precisely Adams implicitely uses a standard result in lambda-calculus theory,
sometimes known as the strict lemma, that states that:

   If M reduces to N by a *strict* reduction (involving no K-redex) and if N is
   SN then so is M.

This is proved in a form or another by various authors (Barendregt, Danos, De
Vrijer, Tortora, ...); I have a proof of it in my 1994 TCS paper "Une
équivalence sur les lambda-termes" (the paper is in french). I can't find
another precise reference at the moment but certainly somebody on this list
may provide one.

I therefore believe Adam's argument is correct; I furthermore found it elegant
and concise, I wish I had found it myself!
(Continue reading)

Permalink | Reply | 1 comment |
headers
Pierre Hyvernat | 17 Oct 2008 14:37
Picon
Favicon

Re: questiuon about strong normalization in untyped lambda-calculus

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

Hello.

Someone else is bound to have answered before my message gets through,
but here we go:

> I think this proof is invalid.  The inference
>
> > T_1 T_1 T_2 ... T_n is strongly normalizing (using T_1 in A).  Hence
> > (\x.xx)T_1 T_2 ... T_n is strongly normalizing.
>
> seems to use the inference
>
> If M reduces to N and N is SN, so is M.
>
>
As you pointed out, this is false; but the proof doesn't use this.
It relies on the following general observation:

  if M[x:=N] N1 ... Nk is SN   and   if N is SN
  then (\x.M) N N1 ... Nk is also SN

(This is true.)

Pierre
--

-- 
Real programmers don't comment their code.  It was hard
to write, it should be hard to understand.
(Continue reading)

Permalink | Reply | 2 comments |

Gmane