From b66ac09af03b69d409df27ef32c90fa38924af2f Mon Sep 17 00:00:00 2001 From: cyfraeviolae Date: Tue, 18 May 2021 19:35:59 -0400 Subject: fix additive identity example --- app/Web.hs | 2 +- src/Lib.hs | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/app/Web.hs b/app/Web.hs index ba54f85..89b6ac5 100644 --- a/app/Web.hs +++ b/app/Web.hs @@ -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."), diff --git a/src/Lib.hs b/src/Lib.hs index 13dc4ac..e8bc698 100644 --- a/src/Lib.hs +++ b/src/Lib.hs @@ -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' -- cgit v1.2.3