[Haskell-cafe] memoizing with a default
Li-yao Xia
li-yao.xia at ens.fr
Sat Dec 10 22:40:32 UTC 2016
Hello Michael,
As indicated by its name, memoFix defines a fixed point of its argument.
In particular it defines the least defined fixed point,
which is unique, and can formally be obtained by iteration starting from
bottom.
You want a function which is defined everywhere, so it is maximal for
the ordering of definedness.
In general there is no unique greatest fixed point for that ordering
(e.g., id makes everything a fixed point), which explains why there is
no standard way to build one.
In your case different' also doesn't have a unique fixed point if your
automaton is not minimal. There are at least the one you're looking for,
and the function corresponding to the total relation (State × State):
const (const True)
Since different' is defined with disjunctions and no negations, it is
monotonic with the ordering (False < True) lifted to total functions.
Thus iterating from the bottom value (const (const False)) gets you the
least fixed point... Interesting.
By the way
> Where (memoFixWithDefault default f) is like (memoFix f) except that if
> (memoFix f a) would loop, then (memoFixWithDefault default f a) =
> default a.
That will not produce the correct result. For instance, assume there are
two non-final states A and B which point to themselves with the same
letter C, (A -C-> A, B -C-> B) but are actually not equivalent, so
different A B should be True. Yet
different (step A C) (step B C) = different A B
so memoFix may still loop.
Shortcircuiting when a loop is detected works to compute a *least
defined* fixed point (i.e., Haskell's fix, or memoFix) because
definedness is "conjunctive" (expanding the parallel between bottom and
False): all values which are needed must be defined, so encountering
bottom kills the whole computation.
On the contrary, the function "different" is "disjunctive", it
shortcircuits on True. When you encounter a loop, the result (which you
are in the middle of computing) could still be either True or False. So
you could *temporarily* return False from such a recursive call in order
to continue searching, but must not mark the value as having been
computed, because you're still doing that.
Regards,
Li-yao
On 12/10/2016 04:50 PM, Michael George wrote:
> I've come across a slight variant of memoization and I'm curious if
> either there is a better way to think about (I have yet to reach Haskell
> Enlightement), or if it's been thought about before.
>
> I'm writing a program that does DFA minimization, as described here:
> https://www.tutorialspoint.com/automata_theory/dfa_minimization.htm.
>
> For me, the simplest way to understand the algorithm is we form an
> equivalence relation, where two states are different if either one is
> final and the other isn't, or if there are transitions from them to
> states that are different.
>
> different a b = isFinal a && not (isFinal b) || isFinal b && not
> (isFinal a) || exists chars (\c -> different (step a c) (step b c))
>
> This definition diverges; it never decides that two states are the same.
> The standard algorithm builds a table, starting with the assumption
> that all states are the same, and iteratively applying this definition
> until it converges.
>
> I'm thinking of that algorithm as a memoized version of the
> implementation of different above. But it's not quite:
>
> different = memoFix2 different' where
> different' different'' a b = isFinal a && not (isFinal b) || isFinal
> b && not (isFinal a) || exists chars (\c -> different'' (step a c) (step
> b c))
>
>
> In general, I think what I want is
>
> memoFixWithDefault :: (a -> b) -> ((a->b) -> (a -> b)) -> (a -> b)
>
>
>
> I suspect there's a nice denotational way of describing this, but my
> denotational semantics is rusty (maybe it's the least fixed point of f
> that is greater than g or something, but that's not it). I suspect that
> there needs to be a nice relationship between f and g for
> memoFixWithDefault f g to be sensible. I also suspect that there's a
> cute 3-line implementation like all the other implementations of memoize
> out there, but I don't see it. I also suspect that depth-first search
> has a cute implementation using this combinator.
>
> So I was wondering if other people had thoughts or references before I
> went off and thought about it.
>
> Thanks!
>
> -M
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
More information about the Haskell-Cafe
mailing list