[Haskell-cafe] beginner's problem about lists

[Nicolas Frisby]

For my own edification (experts: please remark if I stray from any
conventional notions--be as picky as possible) and perhaps for anyone
who didn't quite grok Ross Paterson's punchline, I'm going to try to
answer the question "How does seq affect the definedness CPO?"

At the heart of these two recursive definitions

q = 3 : q                  (1)
r = r `seq` (3 : r)       (2)

we find these two functions f and g

f x = 3 : x
g x = x `seq` (3 : x)

such that

q = lfp f
r = lfp g

This is the least fixed point approach to recursive definitions. (From
Scott and Strachey? I'm not sure of the origins...)

In the CPO of definedness, x < y means that "x is less-defined than
y". Since _|_ is "undefined": forall x . _|_ <= x.  For a more meaty
case, consider

l1 = Cons 3 Nil
l2 = Cons 3 _|_

l2 > l1 because l1 is more defined. If values don't share the same
structure, (a tree and a list for instance) I don't think their
comparison is meaningful (experts?).

The intuition behind the lfp as a definition principle is that of
refinement/approximation. When constructing a value for the
recursively definition, we begin with _|_ which represents no
information. Finding the lfp of function means that we apply the
function as many times as is necessary to define the value. Each
application of the function refines the value a bit more until we have
the sufficient approximation of the full value. What constitutes
"sufficient" is determined by how the value is used: consider ((head .
tail) q) versus (length q).

Intuitively

q = lfp f = f(f(f(f(f(f .... (f(f(f _|_)))...)))))            (*)
r = lfg g = g(g(g(g(g(g .... (g(g(g _|_)))...)))))     (**)

q is infinite 3s because f is non-strict. Operationaly, when f is
applied to the thunk representing the final q value, it contributes
the (3:) constructor to the definition of q, making q more defined.
Note that it does not need to force the evaluation of q in order to
make this contribution. Thus, the intuitive (f _|_) of (*) is never
evaluated.

r is _|_ because g is strict. When g is applied to the thunk
representing the final q value, it forces its evaluation which
operationaly leads us to g again being applied to the final q value
thunk without making any contribution to the definition. Thus, the
intuitive (g _|_) of (**) is always evaluated. Since g is strict, g
_|_ = _|_ and this reduction trickles all the way out until r = _|_.

As Robert Dockins showed, any recursive definition of a Fin value
unfolds to an equation like (2) because of the strictness annotation
in the datatype. We just discussed that the lfp semantics of an
equation of (2)'s form will always result in _|_. On the other hand,
any finite definition of a Fin value works fine. So ihope's Fin data
type is either a finite list or _|_, as was purposed.

Was that all square? Dotted i's and such?

Nick

On 10/11/06, Ross Paterson <ross at soi.city.ac.uk> wrote:
> On Wed, Oct 11, 2006 at 11:04:49AM -0400, Robert Dockins wrote:
> > let q = seq q (FinCons 3 q) in q                    (beta)
> >
> > We have (from section 6.2):
> >    seq _|_ y = _|_
> >    seq x y = y    iff x /= _|_
> >
> > Now, here we have an interesting dilemma.
>
> The meaning of a recursive definition is the least fixed point of
> the equation, in this case _|_.  Same as let x = x in x.
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>