diff options
| -rw-r--r-- | app/Web.hs | 2 | ||||
| -rw-r--r-- | src/Lib.hs | 4 |
2 files changed, 4 insertions, 2 deletions
@@ -97,7 +97,7 @@ examples = [ ("1+1=2", "one plus one equals two."), ("Ax.Ay.x+y=y+x", "addition is commutative."), ("Ex.Ay.x>y", "there exists a largest natural."), - ("Ee.Ax.(x+e=x & Ay.(x+y=x -> e=y))", "the additive identity exists and is unique."), + ("Ee.Ae'.(Ax.e'+x=x <-> e=e')", "the additive identity exists and is unique."), ("Ax.Ey.2y=x", "every natural is even."), ("Ax.Ey.(2y=x | 2y+1=x)", "every natural is either even or odd."), ("Ax.Ay.Az.((x=y & y=z) -> x=z)", "equality is transitive."), @@ -209,6 +209,8 @@ chars n = in map (1 :) r ++ map (0 :) r minimize :: (Ord a) => Integer -> NFA [Int] a -> NFA [Int] a -minimize n nfa@(NFA _ starts accepts f) = NFA states' starts accepts f +minimize n nfa@(NFA _ starts accepts f) = NFA states' starts' accepts' f where states' = closure nfa (chars n) starts + starts' = starts `L.intersect` states' + accepts' = accepts `L.intersect` states' |