Termination of substitution

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

Termination of substitution

Neil Mitchell
Hi

I'm trying to show that a system of rules for manipulating Haskell
expressions is terminating. The rules can be applied in any order, to
any subexpression - and there is a problem if there is any possible
infinite sequence.

The rule that is giving me particular problems is:

(\v -> x) y   =>   x[v/y]

(I realise this rule may duplicate the computation of y, but that is
not relevant for this purpose.)

In particular, given the expression

(\x -> x x) (\x -> x x)

we can keep applying this rule infinitely.

However, I don't believe this expression is type safe in Haskell. Are
any such expressions that would cause this to non-terminate not type
safe? What are the necessary conditions for this to be safe? Does GHC
perform lambda reduction, probably by introducing a let binding? Does
the combination of reducing lambdas and creating let bindings give
similar problems, particularly if bindings are inlined?

I'm wondering if this rule is genuinely unsafe in Haskell. If it is,
why isn't it an issue in real simplifiers. If it isn't, what makes it
safe.

Thanks for any help,

Neil
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Termination of substitution

Taral
On 3/12/08, Neil Mitchell <[hidden email]> wrote:
>  However, I don't believe this expression is type safe in Haskell.

Using higher-order polymorphism:

f (x :: forall a. a -> a) = x x

--
Taral <[hidden email]>
"Please let me know if there's any further trouble I can give you."
    -- Unknown
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Termination of substitution

Stefan O'Rear
In reply to this post by Neil Mitchell
On Wed, Mar 12, 2008 at 09:05:03PM +0000, Neil Mitchell wrote:

> Hi
>
> I'm trying to show that a system of rules for manipulating Haskell
> expressions is terminating. The rules can be applied in any order, to
> any subexpression - and there is a problem if there is any possible
> infinite sequence.
>
> The rule that is giving me particular problems is:
>
> (\v -> x) y   =>   x[v/y]
>
> (I realise this rule may duplicate the computation of y, but that is
> not relevant for this purpose.)
>
> In particular, given the expression
>
> (\x -> x x) (\x -> x x)
>
> we can keep applying this rule infinitely.
>
> However, I don't believe this expression is type safe in Haskell. Are
> any such expressions that would cause this to non-terminate not type
> safe?
I think you mean all, and the answer is "no, but".  (Very interesting
topic here, for me at least.)

Haskell's core type system (let, lambda, and application) can be mapped
into the simply-typed lambda calculus by macro-expanding lets, and (by
the construction of the Hindley-Milner type system) this mapping is
typability-preserving.  The simply-typed lambda calculus is not only
terminating, it is strongly normalizing - ALL possible reduction
sequences stop eventually.   (There is a very elegant proof of this).

The addition of data types in full generality breaks this:

newtype Curry o = Curry { unCurry :: Curry o -> o }

loop :: o
loop = (\c -> unCurry c c) (Curry (\c -> unCurry c c))

Systems like Coq, which need to preserve strong normalization for
logical soundness, adopt a variety of syntactic restrictions.  Coq
specifically forbids contravariant recursion in types.


> What are the necessary conditions for this to be safe? Does GHC
> perform lambda reduction, probably by introducing a let binding? Does
> the combination of reducing lambdas and creating let bindings give
> similar problems, particularly if bindings are inlined?

Yes.  If you feed that example into GHC, GHC will crash (even with the
optimizer off).  Works fine in Hugs/Yhc.

http://www.haskell.org/ghc/docs/latest/html/users_guide/bugs.html#bugs-ghc

> I'm wondering if this rule is genuinely unsafe in Haskell. If it is,
> why isn't it an issue in real simplifiers. If it isn't, what makes it
> safe.

Nobody but us logic fans actually writes encodings of Curry's Paradox.

Stefan

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (196 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Termination of substitution

Stefan O'Rear
In reply to this post by Taral
On Wed, Mar 12, 2008 at 02:30:41PM -0700, Taral wrote:
> On 3/12/08, Neil Mitchell <[hidden email]> wrote:
> >  However, I don't believe this expression is type safe in Haskell.
>
> Using higher-order polymorphism:
>
> f (x :: forall a. a -> a) = x x

Interestingly, this doesn't work - f is a self-application function, but
it does not have a type that can be made to look like forall a. a -> a.
Indeed, higher-order polymorphism as implemented in GHC can be
implemented in System F-omega, a strongly normalizing calculus.  (The
usual datatype caveats apply).

Stefan

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

signature.asc (196 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

RE: Termination of substitution

Simon Peyton Jones
In reply to this post by Neil Mitchell
As Stefan says, System Fw is strongly normalising.  This is a remarkable result because (as you observe) it's very non-obvious how to prove it.

However GHC goes beyond Fw by adding
        data types
        letrec
This blows strong normalisation out of the water.  (Assuming you have reasonable rules for case and letrec.)  But perhaps if you restrict data types a bit, and place draconian restrictions on letrec (e.g. never inline one) you could retain strong normalisation. It depends how much you want your rules to do.

GHC's simplifier deals with the letrec problem by cutting each recursive loop -- see the paper "Secrets of the GHC inliner".  GHC doesn't solve the data type problem at all -- you can make the Simplifier loop if you try.

Simon


| -----Original Message-----
| From: [hidden email] [mailto:[hidden email]] On Behalf Of Neil Mitchell
| Sent: 12 March 2008 21:05
| To: Haskell Cafe
| Subject: [Haskell-cafe] Termination of substitution
|
| Hi
|
| I'm trying to show that a system of rules for manipulating Haskell
| expressions is terminating. The rules can be applied in any order, to
| any subexpression - and there is a problem if there is any possible
| infinite sequence.
|
| The rule that is giving me particular problems is:
|
| (\v -> x) y   =>   x[v/y]
|
| (I realise this rule may duplicate the computation of y, but that is
| not relevant for this purpose.)
|
| In particular, given the expression
|
| (\x -> x x) (\x -> x x)
|
| we can keep applying this rule infinitely.
|
| However, I don't believe this expression is type safe in Haskell. Are
| any such expressions that would cause this to non-terminate not type
| safe? What are the necessary conditions for this to be safe? Does GHC
| perform lambda reduction, probably by introducing a let binding? Does
| the combination of reducing lambdas and creating let bindings give
| similar problems, particularly if bindings are inlined?
|
| I'm wondering if this rule is genuinely unsafe in Haskell. If it is,
| why isn't it an issue in real simplifiers. If it isn't, what makes it
| safe.
|
| Thanks for any help,
|
| Neil
| _______________________________________________
| Haskell-Cafe mailing list
| [hidden email]
| http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Termination of substitution

Neil Mitchell
Hi

Thanks for the interesting comments. Its looks like learning some of
the basics about System Fw is probably the way forward.

>  However GHC goes beyond Fw by adding
>         data types
>         letrec
>  This blows strong normalisation out of the water.  (Assuming you have reasonable rules for case and letrec.)  But perhaps if you restrict data types a bit, and place draconian restrictions on letrec (e.g. never inline one) you could retain strong normalisation. It depends how much you want your rules to do.

I have restricted letrec appropriately. I haven't looked at the data
type problem, but given that GHC manages to ignore it, I think its
probably fair for me to ignore it for the time being.

Thanks very much for the helpful comments,

Neil
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe