[Haskell-cafe] memoizing with a default

[Li-yao Xia]

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.