Skip to content

noamz/linlam

master
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
 
 
src
 
 
 
 
 
 
 
 
 
 
 
 

LinLam: a Haskell library for experimental linear lambda calculus

A collection of Haskell routines for generating, normalizing, typing, diagrammifying, and otherwise playing with linear lambda terms.

Installation

cabal configure
cabal build
cabal install --lib

The library has a few dependencies, which (hopefully!) should be automatically taken care of by cabal.

Quick start

Begin by opening the Haskell interpreter and importing the LinLam library:

$ ghci
GHCi, version 8.8.4: https://www.haskell.org/ghc/  :? for help
Prelude> import LinLam
Prelude LinLam> 

Then try some of the example sessions below, which illustrate how to use the library to do experimental lambda calculus.

Afterwards, you can also have a look in the experiments directory, which contains some standalone compilable experiments.

Example interactive sessions

Enumerating some terms, printing and normalizing them

Prelude LinLam> allLT 5 0
[A (L 0 (V 0)) (L 1 (V 1)),L 0 (A (V 0) (L 1 (V 1))),L 1 (A (L 0 (V 0)) (V 1)),L 0 (L 1 (A (V 0) (V 1))),L 1 (L 0 (A (V 0) (V 1)))]
Prelude LinLam> printLTs (allLT 5 0)
(\a.a)(\b.b)
\a.a(\b.b)
\b.(\a.a)(b)
\a.\b.a(b)
\b.\a.a(b)
Prelude LinLam> printLTs (allPT 5 0)
(\a.a)(\b.b)
\a.a(\b.b)
\b.(\a.a)(b)
\a.\b.a(b)
Prelude LinLam> printLTs (allBPT 7 1)
\b.a(\c.b(c))
\c.(\b.a(b))(c)
\b.\c.a(b(c))
\b.\c.a(b)(c)
Prelude LinLam> [length (allLT (3*n+2) 0) | n <- [0..4]]
[1,5,60,1105,27120]
Prelude LinLam> [length (allPT (3*n+2) 0) | n <- [0..6]]
[1,4,32,336,4096,54912,786432]
Prelude LinLam> [length (allBPT (3*n+1) 1) | n <- [0..6]]
[1,1,4,24,176,1456,13056]
Prelude LinLam> normalize (L 0 $ A (L 1 $ V 1) (V 0))
L 0 (V 0)
Prelude LinLam> printLTs $ filter (betaEq (L 0 $ V 0)) (allLT 5 0)
(\a.a)(\b.b)
\b.(\a.a)(b)
Prelude LinLam> 

Generating a random closed term and making some observations, or running a repeated experiment to generate a histogram

Prelude LinLam> t <- randomLT (3*100+2)
Prelude LinLam> printLT t
\a.\b.\c.\d.\e.\f.\g.\h.\i.\j.\k.\l.\m.\n.\o.\p.\q.\r.\s.\t.\u.(\v.\w.\x.\y.\z.\X0.\X1.\X2.\X3.\X4.\X5.\X6.\X7.\X8.\X9.X6(\X10.\X11.\X12.e(p(\X13.\X14.\X15.\X16.\X17.(\X18.\X19.\X20.j(\X21.\X22.\X23.\X24.\X25.\X26.\X27.\X28.\X29.\X30.\X31.\X32.\X33.\X34.g((\X35.X33(\X36.\X37.\X38.\X39.\X40.\X41.\X42.\X43.d(\X44.\X45.\X46.(\X47.\X48.\X49.X32(r)(\X50.X41(X20(\X51.\X52.\X53.(\X54.\X55.\X56.X23(\X57.\X58.\X59.\X60.(\X61.X61(v))(X42)(X60(n))(X36(X58)(X55)(o)(\X62.X13(\X63.\X64.y(X38(X49(X57)(X26(X48)(h(\X65.X5(X34)(a(\X66.X43(X29(X10))(q)(X65)((\X67.(\X68.w(X37)(c(X56(X3(X15))(X18)(X67)(X39((\X69.(\X70.\X71.X59(X63((\X72.\X73.(\X74.X35(X74)(X68))(X54)(X73(X44)(X22(X19))(X72)(X27(X0))(X47)))(X52(X50)(m)(X25)(f(X2(X4)(X69)(k)(x(X45(z))(X21)(X24)))(X62(X46(X1)))(X12))(X70))))(X8(X71)))(i(X53)))(u))))))(X64))(X14(X66)))))))))(X16(X51)))))(X9))(X31)(X40)))(l)(X11)))))(t(s(X30))))(X28)))(X17))))(X7)))))(b)
Prelude LinLam> size (normalize t)
263
Prelude LinLam> size t - size (normalize t)
39
Prelude LinLam> histogram <$> experimentLT (\t -> size t - size(normalize t)) 302 100
[(18,1),(21,2),(24,5),(27,3),(30,1),(33,7),(36,8),(39,14),(42,11),(45,7),(48,11),(51,6),(54,11),(57,5),(60,2),(63,1),(66,2),(69,1),(75,1),(78,1)]

Type inference

Prelude LinLam> mapM_ (\t -> putStrLn (prettyLT t ++ " : " ++ prettyType (synthClosed t))) (allNLT 8 0)
\a.a(\b.b(\c.c)) : (((((γ -> γ) -> β) -> β) -> α) -> α)
\a.a(\b.\c.b(c)) : ((((γ -> β) ->-> β)) -> α) -> α)
\a.a(\c.\b.b(c)) : (((γ -> ((γ -> β) -> β)) -> α) -> α)
\a.a(\b.b)(\c.c) : (((γ -> γ) -> ((β -> β) -> α)) -> α)
\a.\b.a(b(\c.c)) : ((β -> α) -> (((γ -> γ) -> β) -> α))
\b.\a.a(b(\c.c)) : (((γ -> γ) -> β) -> ((β -> α) -> α))
\a.\b.a(\c.b(c)) : (((γ -> β) -> α) -> ((γ -> β) -> α))
\b.\a.a(\c.b(c)) : ((γ -> β) -> (((γ -> β) -> α) -> α))
\a.\c.a(\b.b(c)) : ((((γ -> β) -> β) -> α) ->-> α))
\c.\a.a(\b.b(c)) :-> ((((γ -> β) -> β) -> α) -> α))
\a.\b.a(b)(\c.c) : ((γ -> ((β -> β) -> α)) ->-> α))
\b.\a.a(b)(\c.c) :-> ((γ -> ((β -> β) -> α)) -> α))
\a.\c.a(\b.b)(c) : (((γ -> γ) ->-> α)) ->-> α))
\c.\a.a(\b.b)(c) :-> (((γ -> γ) ->-> α)) -> α))
\a.\b.\c.a(b(c)) : ((β -> α) -> ((γ -> β) ->-> α)))
\b.\a.\c.a(b(c)) : ((γ -> β) -> ((β -> α) ->-> α)))
\a.\c.\b.a(b(c)) : ((β -> α) ->-> ((γ -> β) -> α)))
\c.\a.\b.a(b(c)) :-> ((β -> α) -> ((γ -> β) -> α)))
\b.\c.\a.a(b(c)) : ((γ -> β) ->-> ((β -> α) -> α)))
\c.\b.\a.a(b(c)) :-> ((γ -> β) -> ((β -> α) -> α)))
\a.\b.\c.a(b)(c) : ((γ ->-> α)) ->->-> α)))
\b.\a.\c.a(b)(c) :-> ((γ ->-> α)) ->-> α)))
\a.\c.\b.a(b)(c) : ((γ ->-> α)) ->->-> α)))
\c.\a.\b.a(b)(c) :-> ((γ ->-> α)) ->-> α)))
\b.\c.\a.a(b)(c) :->-> ((γ ->-> α)) -> α)))
\c.\b.\a.a(b)(c) :->-> ((γ ->-> α)) -> α)))

Loading lambda terms from a file

(See example files bckwi.lam and ski.lam.)

Prelude LinLam> ts <- readLTsFromFile "terms/bckwi.lam"
Prelude LinLam> printLTs ts
\a.\b.\c.a(b(c))
\a.\b.\c.a(c)(b)
\a.\b.a
\a.\b.a(b)(b)
\a.a
Prelude LinLam> [s,k,i] <- readLTsFromFile "terms/ski.lam"
Prelude LinLam> t = k
Prelude LinLam> f = A s k
Prelude LinLam> not = A (A s (A (A s i) (A k f))) (A k t)
Prelude LinLam> or = A (A s i) (A k t)
Prelude LinLam> betaEq (A not t) f
True
Prelude LinLam> betaEq (A not f) t
True
Prelude LinLam> betaEq (foldl A or [f,f]) f
True
Prelude LinLam> betaEq (foldl A or [f,t]) t
True
Prelude LinLam> betaEq (foldl A or [t,f]) t
True
Prelude LinLam> betaEq (foldl A or [t,t]) t
True

Making diagrams

Generate a table of string diagrams (λ-graphs) representing the term structure of all closed planar terms of size 8 (in a file named diagrams/pt8,0.svg):

Prelude LinLam> renderLTs' (allPT 8 0) "diagrams/pt8,0"

pt8,0

Generate a table of string diagrams (proof-nets) representing the type structure of all one-variable-open normal bridgeless terms of size 7:

Prelude LinLam> trenderNLTs' (allNBLT 7 1) "diagrams/nblt7,1"

nblt7,1

Generate a random one-variable-open bridgeless term of size 451, normalize it, and diagram its type structure (just the pure graphical diagram, without any Greek annotations):

Prelude LinLam> t <- randomBLT (3*150+1)
Prelude LinLam> trenderNLT (normalize t) "diagrams/randomnlt"

randomnlt

Background

Some papers:

Some talks:

Some related tools:

License

Free to use under an MIT License.

About

a library for experimental linear lambda calculus

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published