The main program for Lambdascope
> {-# LANGUAGE RecursiveDo,CPP #-}
> module Main where
> import INet
> import Diagram hiding (S)
> import Lambda
> import Graphics.Rendering.OpenGL (($=), GLfloat)
> import qualified Graphics.Rendering.OpenGL as GL
> import qualified Graphics.UI.GLFW as GLFW
> import Control.Monad.Fix
> import Control.Monad (when, unless)
> import Data.IORef
> import Data.IntMap hiding (lookup, mapMaybe)
> import Data.Maybe (mapMaybe, fromMaybe)
> import Prelude hiding (map)
> import System.IO.Unsafe
An interactive net is a mapping from node IDs to their connected (node ID,
port No) pairs.
Main Program
#ifdef _EnableGUI_
> import EnableGUI
> main = enableGUI >> do
#else
> main = do
#endif
> GLFW.initialize
> initWindow w h
> showHelp <- newIORef False
> GLFW.charCallback $= \c b -> when ((c == 'H' || c == 'h') && b == GLFW.Release)
> (modifyIORef showHelp not)
> factor <- newIORef (0, 0, 1.0)
> netRef <- newIORef net
> loop showHelp factor (handleUserAction factor (keyHandle netRef) (reduce netRef) d)
> GLFW.closeWindow
> GLFW.terminate
> where
> -- prepare an initial diagram to load
> net = nodeToNet (mkNode (termToNode t2')) --(App cube (VInt 3))))
> d = netToDiagram net
> w = 800
> h = 600
> loop showHelp factor handle = do
> (UserAction handle', render) <- handle
> GL.clear [GL.ColorBuffer]
> (cx, cy, s) <- readIORef factor
> GL.preservingMatrix (do
> GL.translate (vector3 (cx / unit) (cy / unit) 0)
> GL.scale s s 1
> render)
> help <- readIORef showHelp
> GL.preservingMatrix (do
> GL.color $ color3 0.2 0.3 0.8
> GL.translate (vector3 (- fromIntegral w / unit / 2) (fromIntegral h / unit / 2 - 1.25) 0)
> GL.scale 0.8 0.8 (1::GLfloat)
> renderString "H toggles help, ESC quits"
> GL.translate $ vector3 0 (-1.25) 0
> when help $ renderText helpText)
> GLFW.swapBuffers
> GLFW.sleep 0.01
> exit <- GLFW.getKey GLFW.ESC
> unless (exit == GLFW.Press) $ loop showHelp factor handle'
> helpText = unlines
> [ "CTRL+ mouse pan"
> , "ALT + mouse zoom"
> , "Left click rotate node"
> , "Right click apply any rule to node"
> , "Drag mouse move node"
> , "1 .. 9 load presets"
> , "Space auto zoom"
> , "L auto layout all nodes"
> , "R reduce to head normal form"
> , "X repeat outermost cross rule"
> , "B repeat beta rule everywhere"
> , "E repeat erase rule everywhere"
> , "U apply unwind rule everywhere"
> , "S apply scope rule everywhere"
> , "C apply loopcut rule everywhere"
> , "T unwind, cross, scope, cross, loopcut, cross"
> , "M repeat meta rule everywhere"
> , "P prune all none root tree"
> , "O apply outermost reduction rules once"
> , "V print beta, meta, size couter on console"
> , "D zap duplicator's value (become call-by-need)"]
>
>
> keyHandle netRef = (fst $ unzip ks, handle)
> where
> -- change the following line to load different programs for 1..9
> -- It currently loads the (opt N) lambda expression.
> ks = [(c, load $ opt $ fromEnum c - 48) | c <- ['1'..'9']] ++
> [('R', reduceAll),
> ('X', crossAll),
> ('B', betaAll),
> ('E', eraseAll),
> ('U', unwindAll),
> ('S', scopeAll),
> ('C', loopcutAll),
> ('T', toTerm),
> ('M', metaAll),
> ('P', pruneAll),
> ('O', outer),
> ('V', viewCounter),
> ('L', reLayout),
> ('D', demoteDup)]
> handle k d r = do
> net <- readIORef netRef
> let (net', d', r') = maybe (net, d, r) (\f -> f net d r) (lookup k ks)
> writeIORef netRef net'
> return (d', r')
> demoteDup net d r@((posMap, _), _) =
> let net' = map (\a -> case a of
> (Duplicator, cp, cv) -> (Duplicator, cp, Nothing)
> _ -> a) net
> d' = netToDiagram net'
> ids = keys net'
> posMap' = filterWithKey (\i _ -> elem i ids) posMap
> r' = renderDiagram posMap' d'
> in (net', d', r')
> load x n _ _ =
> let net = nodeToNet (mkNode (termToNode x))
> d = netToDiagram net
> in resetCounters n `seq` (net, d, renderDiagram empty d)
> reLayout net d r@((posMap, _), _) = (net, d, renderDiagram empty d)
activates a local rule to a node, and apply it once.
> reduce :: IORef INet -> Int -> IO ([Int], Diagram)
> reduce netRef i = do
> net <- readIORef netRef
> let a@(at, ap, av) = net ! i
> (j, n) = head ap
> b@(bt, bp, bv) = net ! j
> net' = debug1 ("reduced from\n " ++ show net ++ "\nto ") $ if ap == []
> then error "here!" -- delete i net
> else fromMaybe net $ localAll net (i, a) (j, b)
> ids = keys net'
> writeIORef netRef net'
> return (ids, netToDiagram net')
> localAll = meta_ ->- beta_ ->- cross_ ->- erase
Note that in optimal reduction, the erase is a global rule rather than an
outermost one because it'll otherwise results in redudant beta or meta
reduction.
> reduceAll = wrapRule (repeatRule (outermost localAll +>+ applyRule erase_))
> crossAll = wrapRule (repeatRule (outermost cross))
> betaAll = wrapRule (repeatRule (applyRule beta_))
> eraseAll = wrapRule (repeatRule (applyRule erase))
> unwindAll = wrapRule (applyRule unwind)
> scopeAll = wrapRule (applyRule scope)
> loopcutAll = wrapRule (applyRule loopcut)
> metaAll = wrapRule (repeatRule (applyRule meta_))
> outer = wrapRule (outermost localAll)
> pruneAll = wrapRule prune
> toTerm net =
> let r@(net', d') = readback net
> t = netToTerm net'
> in debug ("toTerm=" ++ show t) $ wrapRule (const r) net
> wrapRule f net d r@((posMap, _), _) =
> let (net', _) = f net
> d' = netToDiagram net'
> ids = keys net'
> posMap' = filterWithKey (\i _ -> elem i ids) posMap
> r' = renderDiagram posMap' d'
> in (net', d', r')
Counters are hacks. Though our rules are already return the counting,
they are not used.
> crossCounter = unsafePerformIO (newIORef 0)
> betaCounter = unsafePerformIO (newIORef 0)
> metaCounter = unsafePerformIO (newIORef 0)
> sizeTracker = unsafePerformIO (newIORef (1000000,0))
> trackSize net = unsafePerformIO $ do
> m <- readIORef sizeTracker
> let s = size net
> m' = (min (fst m) s, max (snd m) s)
> s `seq` fst m' `seq` snd m' `seq` writeIORef sizeTracker m'
> --putStrLn $ show m'
> return net
> resetCounters n = unsafePerformIO $ do
> writeIORef crossCounter 0
> writeIORef betaCounter 0
> writeIORef metaCounter 0
> writeIORef sizeTracker (1000000, 0)
> viewCounter n d r =
> let view n c = do
> m <- readIORef c
> putStrLn $ n ++ " = " ++ show m
> viewAll n = do
> view "cross" crossCounter
> view "beta" betaCounter
> view "meta" metaCounter
> view "size" sizeTracker
> in unsafePerformIO (viewAll n) `seq` (n, d, r)
> incCounter c x y z = do
> m <- readIORef c
> let m' = m + 1
> m' `seq` writeIORef c m'
> mkCounter c f x y z =
> let r = f x y z
> in if r == Nothing
> then r
> else unsafePerformIO (incCounter c x y z) `seq` r
> mkCounter' c f x y@(_, (t,_,_)) z@(_, (t', _, _)) =
> let r = f x y z
> tup = case (t, t') of
> (Constructor _, _) -> True
> (_, Constructor _) -> True
> _ -> False
> in if r == Nothing || tup
> then r
> else unsafePerformIO (incCounter c x y z) `seq` r
Customizd beta, meta and erase rules that track statistics.
> cross_ = mkCounter crossCounter cross
> beta_ = mkCounter betaCounter beta
> meta_ = mkCounter metaCounter meta -- don't track tuple projection
> erase_ net a b =
> let net' = trackSize net
> in (trackSize net `seq`) $
> maybe Nothing (Just . (\net -> trackSize net `seq` net)) $
> erase net' a b
Testing
=======
We can compose INet nodes by wiring them
> two s = mdo
> a <- abstractor s b e
> b <- abstractor a c m
> c <- applicator d f b
> d <- delimiter e c 0
> e <- duplicator a k d 0
> f <- applicator g l c
> g <- delimiter k f 0
> h <- eraser m
> i <- eraser l
> j <- eraser k
> k <- duplicator e g j 0
> l <- duplicator m i f 0
> m <- duplicator b l h 0
> return a
> four = mdo
> s <- eraser a
> a <- applicator b b s
> b <- duplicator t a a 0
> t <- two b
> return s
or we can write a Generalized Lambda term, and convert it to INet.
> x = VStr "x"
> f = Abs (VFunc 1 "f" Z)
> t2 = church 2
> t2' = App (App (church 2) f) x --App (App (Abs (Abs (App (S Z) (App (S Z) Z)))) f) x
> t4 = App (Abs (App Z Z)) t2
> t4' = App (App t4 f) x
> church n = Abs (Abs (app n (S Z) Z))
> app 0 f x = x
> app n f x = App f (app (n - 1) f x)
> double = Abs (App (VFunc 2 "+" (App id Z)) Z)
> where id = Abs Z
> testDouble n = app n double (VInt 1)
Test substitution
> testSub = App f (VInt 7)
> where
> s = Abs (App (VFunc 2 "*" Z) Z)
> f = Abs (App (Abs (App (VFunc 2 ":" Z) (App (VFunc 2 "*" Z) (S Z))))
> (App (VFunc 2 "*" Z) Z))
Test for meta level fuction with arity
> d1 = App (Abs (App (VFunc 2 "g" Z) Z)) t2'
Test for handling disconnected graph, rather than tree
> test :: INet
> test = fromList [
> (0, (Eraser, [(1, 0)], Nothing)),
> (1, (Eraser, [(0, 0)], Nothing)),
> (2, (Eraser, [(3, 0)], Nothing)),
> (3, (Eraser, [(2, 0)], Nothing)) ]
Test for tuples
> p0 = App (Abs (Fst Z)) (Tup t0 t1)
> t0 = Abs (Abs Z)
> t1 = Abs (Abs (App (S Z) Z))
> ones = Y (Abs (Tup (VInt 1) Z))
> one = Fst ones
Tests for cross rule with self-loop
for annihilate:
two duplicators wiring to each other on one side
> testL0 :: INet
> testL0 = fromList [
> (0, (Eraser, [(2, 1)], Nothing)),
> (1, (Eraser, [(2, 2)], Nothing)),
> (2, (Duplicator, [(3, 0), (0, 0), (1, 0)], Just 0)),
> (3, (Duplicator, [(2, 0), (3, 2), (3, 1)], Just 0))]
two duplicators wiring to each other on both sides
> testL1 :: INet
> testL1 = fromList [
> (2, (Duplicator, [(3, 0), (2, 2), (2, 1)], Just 0)),
> (3, (Duplicator, [(2, 0), (3, 2), (3, 1)], Just 0))]
for commute:
similar to testL0
> testL2 :: INet
> testL2 = fromList [
> (0, (Eraser, [(2, 1)], Nothing)),
> (1, (Eraser, [(2, 2)], Nothing)),
> (2, (Duplicator, [(3, 0), (0, 0), (1, 0)], Just 1)),
> (3, (Duplicator, [(2, 0), (3, 2), (3, 1)], Just 0))]
similar to testL1
> testL3 :: INet
> testL3 = fromList [
> (2, (Duplicator, [(3, 0), (2, 2), (2, 1)], Just 1)),
> (3, (Duplicator, [(2, 0), (3, 2), (3, 1)], Just 0))]
when a single duplicator loops its two ports
> testL4 :: INet
> testL4 = fromList [
> (0, (Eraser, [(1, 1)], Nothing)),
> (1, (Delimiter, [(2, 0), (0,0)], Just 0)),
> (2, (Duplicator, [(1, 0), (2, 2), (2, 1)], Just 0))]
These are tests for optimality. With church numbers, (n 2 i x)
takes exponential time in call-by-need, but only linear to n
in optimal reduction.
> i = Abs Z
> opt n = App (App (App (church n) (church 2)) i) i
Chart for opt 1 .. 7
Optimal
cross, beta, size(min, max)
47 6 (2, 27)
84 9 (2, 40)
128 12 (2, 54)
179 15 (2, 69)
237 18 (2, 85)
302 21 (2, 102)
374 24 (2, 120)
Lazy
beta, size(min, max)
6 (2, 14)
11 (2, 18)
20 (2, 32)
37 (2, 52)
70 (2, 84)
135 (2, 152)
264 (2, 284)
392
Compare Lazy, Completely Lazy (M. J. Thyer's thesis: http://thyer.name/phd-thesis/)
and Optimal using number of beta reduction, steps, interactions (excluding garbage
collection) as metrics respectively.
n Lazy C.Lazy Optimal
--------------------------
1 6 8 53
2 11 15 93
3 20 25 140
4 37 40 194
5 70 66 255
6 135 114 323
7 264 204 398
8 392 377 453
9 644 719 539
It's easy to tell that they are of O(n * 2^n), O(n^7) and O(n^2)
respectively. It's also worth mentioning that if we only count the number of
betas, optimal is O(n), and completely lazy is O(n^3), lazy is O(n^4).
Test for integral function
==========================
integral i x = (i, \dt -> integral (next dt i (fst x)) (snd x dt))
also make tuple construction involve beta reduction.
> tup x y = App (App (Abs (Abs (Tup (S Z) Z))) x) y
> next = VFunc 3 "next"
> integral =
> Y (Abs -- \integral ->
> (Abs -- \i ->
> (Abs -- \s ->
> (tup (S Z) -- i,
> (Abs -- \dt ->
> (App (App (S (S (S Z))) -- integral
> (App (App (next Z) -- next dt
> (S (S Z))) -- i
> (Fst (S Z)))) -- fst x
> (App (Snd (S Z)) Z))))))) -- snd x dt
> e = Y (App integral (VInt 1))
> unfold = Abs (App (Snd Z) (VStr "dt"))
> expN n = Fst (app n unfold e)
Chart of computing expN 1 to expN 7
Optimal
cross, beta, meta (total, include projection), meta (arith), size (min, max)
199 11 6 3 (41, 104)
472 16 12 6 (44, 155)
820 21 18 9 (47, 211)
1254 26 24 12 (50, 272)
1818 31 30 15 (53, 338)
2570 36 36 18 (56, 409)
3580 41 42 21 (59, 485)
Call-by-need
13 3 (41, 134)
28 9 (44, 277)
50 18 (47, 516)
79 30 (50, 843)
115 45 (53, 1267)
158 63 (56, 2800)
208 84 (59, 2454)
It indeed shows that call-by-need incurs recomputation at the meta
arithmetic level:
cbn(n) = optimal(n) + cbn(n - 1)
Tests for traversing circular structure using cursor.
A cursor is a tuple
Data Cursor a = (a, List a -> List a)
List is nested tuple, a circular structure
Data List a = (a, List a)
> c1 = tup (VInt 1) (Abs Z) -- c1 = (1, \x -> (2, (3, x)))
> c2 = tup (VInt 1) (Abs (tup (VInt 2) Z)) -- c2 = (1, \x -> (2, (3, x)))
> c3 = tup (VInt 1) (Abs (tup (VInt 2) (tup (VInt 3) Z))) -- c3 = (1, \x -> (2, (3, x)))
adv (Cursor u@(Elem i v) f) =
let f' x = next (f (Cons u x))
u' = this (fix (f . Cons u))
in Cursor u' f'
(u', f'
> nextc =
> Abs
> (tup
> (Fst (Y (Abs (App (Snd (S Z)) (tup (Fst (S Z)) Z)))))
> (Abs (Snd (App (Snd (S Z)) (tup (Fst (S Z)) Z))))
> )
> c n = Fst (app n nextc c2)
3 0 (31, 50)
5 0 (53, 93)
7 0 (77,130)
11 0 (..)
13
15
19
9 3
15 5
21 8
29 12
35 14
41 17
49 21
9 3
15 6
23 10
29 13
37 17
43 20
51 24
9 3
15 6
25 10
34 15
47 21
59 28
75 36
Power Cube Example
==================
> cons x xs = App (VFunc 2 ":" x) xs
> cond c t f = App (App (VFunc 3 "cond" c) t) f
> eq x y = App (VFunc 2 "==" x) y
> times x y = App (VFunc 2 "*" x) y
> minus x y = App (VFunc 2 "-" x) y
> power = Y (Abs (Abs (Abs (
> cond (eq (S Z) (VInt 1))
> (VInt 1)
> (times Z (App (S (S Z)) (minus (S Z) (VInt 1))))))))
> cube = App power (VInt 3)
> powerCube = cons power (cons cube (App cube (VInt 5)))