Skip to content
/ pLam Public
forked from slovnicki/pLam

command line interpreter for learning and exploring pure λ-calculus

License

Notifications You must be signed in to change notification settings

typelogic/pLam

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

This programming language (pLam - a pure Lambda calculus interpreter) is used to explore, test and implement various λ-expressions. Code written in pLam can be executed interactively within pLam's shell or stored in a file with .plam extension and run anytime.

Inside import/ directory, some useful λ-expressions are already implemented.
Inside examples/ directory, there are many examples of λ-expressions demonstrating pLam's capabilities.


Prerequisites

This project builds using Haskell tool stack documented at https://docs.haskellstack.org/en/stable/README/.

Install

On most Unix systems, you can get stack by typing:

curl -sSL https://get.haskellstack.org/ | sh

or:

wget -qO- https://get.haskellstack.org/ | sh

On Windows, you can download 64-bit installer given at https://docs.haskellstack.org/en/stable/README/.

Build & Run

First time setup

  1. clone project repository
git clone https://github.com/sandrolovnicki/pLam.git
  1. go to project directory
cd pLam
  1. setup stack on isolated location
stack setup

Building

  1. use stack to build project
stack build

Running (locally)

5.a) use stack to run project executable from project's directory

stack exec plam

Running (globally (Unix systems))

5.b) use make_global.sh script to create a global command 'plam' that can be used to start pLam from anywhere in your system. The script will also change your import path in src/Config.hs so you need to build the project again.

sudo ./make_global.sh
stack build

Now, (and anytime in the future!), you can start pLam from anywhere in your system by just typing

plam

Examples:

NOTE: Output might be slightly different due to constant fixes and changes. Fully updated examples will be put each time they diverge too far from current.
All the examples can be found in examples/ directory.

Fun with booleans

         _
        | |
    ____| |   ___  __  __
    | _ \ |__| _ \|  \/  |
    |  _/____|____\_\__/_| v1.3.1
    |_| pure λ-calculus interpreter
   =================================

pLam> :import booleans
pLam> 
pLam> and (or F (not F)) (xor T F)
> reductions count              : 18
> uncurried β-normal form       : (λxy. x)
> curried (partial) α-equivalent: T
pLam>

Redex coloring

redex_coloring.png

Fun with arithmetic

pLam> :import std
pLam> 
pLam> mul (add 2 (Sc 2)) (sub (exp 2 3) (Pc 8))
> reductions count              : 762
> uncurried β-normal form       : (λfx. f (f (f (f (f x)))))
> curried (partial) α-equivalent: 5
pLam> 

Factorial

pLam> :import std
pLam> :import comp
pLam>
pLam> fact = PR0 1 (C22 mul (C2 S I12) I22)
pLam> fact 3
> reductions count              : 898
> uncurried β-normal form       : (λfx. f (f (f (f (f (f x))))))
> curried (partial) α-equivalent: 6
pLam> 

Minimization

interactive coding:

pLam> :import std
pLam> :import comp
pLam> 
pLam> fun = \x. mul (sub 2 x) (sub 3 x)
pLam> MIN1 fun
> reductions count              : 114
> uncurried β-normal form       : (λfx. f (f x))
> curried (partial) α-equivalent: 2
pLam> 

running the existing program:

pLam> :run examples/2.5.2
=================================
< zero
=================================
> reductions count              : 114
> uncurried β-normal form       : (λfx. f (f x))
> curried (partial) α-equivalent: 2
pLam>

running the existing program (without entering pLam's shell):

plam ~/Projects/pLam/examples/2.5.2.plam
=================================
< zero
=================================
> reductions count              : 114
> uncurried β-normal form       : (λfx. f (f x))
> curried (partial) α-equivalent: 2
Done.

Binary numerals

         _
        | |
    ____| |   ___  __  __
    | _ \ |__| _ \|  \/  |
    |  _/____|____\_\__/_| v1.3.1
    |_| pure λ-calculus interpreter
   =================================

pLam> :import binary
pLam>
pLam> 0b
> reductions count              : 2
> uncurried β-normal form       : (λp.((p (λxy. y)) (λexy.x)))
> curried (partial) α-equivalent: 0b
pLam> 
pLam> 2048b
> reductions count              : 24
> uncurried β-normal form       : (λp.((p (λxy. y)) (λp.((p (λxy. y)) (λp.((p (λxy. y)) (λp.((p (λxy. y)) (λp.((p (λxy. y)) (λp.((p (λxy. y)) (λp.((p (λxy. y)) (λp.((p (λxy. y)) (λp.((p (λxy. y)) (λp.((p (λxy. y)) (λp.((p (λxy. y)) (λp.((p (λxy. x)) (λexy.x)))))))))))))))))))))))))
> curried (partial) α-equivalent: (λp. ((p F) 1024b))
pLam>
pLam>
pLam> addB 7b (subBs 2b 3b)
> reductions count              : 9458
> uncurried β-normal form       : (λp.((p (λxy. x)) (λp.((p (λxy. x)) (λp.((p (λxy. x)) (λexy.x)))))))
> curried (partial) α-equivalent: 7b
pLam>
pLam> :quit
Goodbye!

About

command line interpreter for learning and exploring pure λ-calculus

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Haskell 97.4%
  • Shell 2.6%