Skip to content

Commit

Permalink
Initial commit
Browse files Browse the repository at this point in the history
  • Loading branch information
cpubot committed Dec 5, 2020
0 parents commit b383686
Show file tree
Hide file tree
Showing 15 changed files with 543 additions and 0 deletions.
2 changes: 2 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
.stack-work/
*~
3 changes: 3 additions & 0 deletions ChangeLog.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
# Changelog for lambda-calculus

## Unreleased changes
30 changes: 30 additions & 0 deletions LICENSE
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
Copyright zbrown (c) 2020

All rights reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:

* Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.

* Redistributions in binary form must reproduce the above
copyright notice, this list of conditions and the following
disclaimer in the documentation and/or other materials provided
with the distribution.

* Neither the name of Author name here nor the names of other
contributors may be used to endorse or promote products derived
from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
1 change: 1 addition & 0 deletions README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
# Untyped lambda calculus
2 changes: 2 additions & 0 deletions Setup.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
import Distribution.Simple
main = defaultMain
4 changes: 4 additions & 0 deletions app/Main.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
module Main where

main :: IO ()
main = putStrLn "open the repl"
72 changes: 72 additions & 0 deletions lambda-calculus.cabal
Original file line number Diff line number Diff line change
@@ -0,0 +1,72 @@
cabal-version: 1.12

-- This file has been generated from package.yaml by hpack version 0.33.0.
--
-- see: https://github.com/sol/hpack
--
-- hash: 8920238fd0ca4ab5a45d87bf3e3d4ecba81deebee5fedb15a63e3f8d16e4dff1

name: lambda-calculus
version: 0.1.0.0
description: Please see the README on GitHub at <https://github.com/githubuser/lambda-calculus#readme>
homepage: https://github.com/githubuser/lambda-calculus#readme
bug-reports: https://github.com/githubuser/lambda-calculus/issues
author: Zachary Brown
maintainer: [email protected]
copyright: 2020 Zachary Brown
license: BSD3
license-file: LICENSE
build-type: Simple
extra-source-files:
README.md
ChangeLog.md

source-repository head
type: git
location: https://github.com/githubuser/lambda-calculus

library
exposed-modules:
Evaluator
Parser
PrettyPrinter
Term
other-modules:
Paths_lambda_calculus
hs-source-dirs:
src
build-depends:
base >=4.7 && <5
, containers
, parsec
default-language: Haskell2010

executable lambda-calculus-exe
main-is: Main.hs
other-modules:
Paths_lambda_calculus
hs-source-dirs:
app
ghc-options: -threaded -rtsopts -with-rtsopts=-N
build-depends:
base >=4.7 && <5
, containers
, lambda-calculus
, parsec
default-language: Haskell2010

test-suite lambda-calculus-test
type: exitcode-stdio-1.0
main-is: Spec.hs
other-modules:
Paths_lambda_calculus
hs-source-dirs:
test
ghc-options: -threaded -rtsopts -with-rtsopts=-N
build-depends:
base >=4.7 && <5
, containers
, hspec
, lambda-calculus
, parsec
default-language: Haskell2010
51 changes: 51 additions & 0 deletions package.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
name: lambda-calculus
version: 0.1.0.0
github: "githubuser/lambda-calculus"
license: BSD3
author: "Zachary Brown"
maintainer: "[email protected]"
copyright: "2020 Zachary Brown"

extra-source-files:
- README.md
- ChangeLog.md

# Metadata used when publishing your package
# synopsis: Short description of your package
# category: Web

# To avoid duplicated efforts in documentation and dealing with the
# complications of embedding Haddock markup inside cabal files, it is
# common to point users to the README.md file.
description: Please see the README on GitHub at <https://github.com/githubuser/lambda-calculus#readme>

dependencies:
- base >= 4.7 && < 5
- parsec
- containers

library:
source-dirs: src

executables:
lambda-calculus-exe:
main: Main.hs
source-dirs: app
ghc-options:
- -threaded
- -rtsopts
- -with-rtsopts=-N
dependencies:
- lambda-calculus

tests:
lambda-calculus-test:
main: Spec.hs
source-dirs: test
ghc-options:
- -threaded
- -rtsopts
- -with-rtsopts=-N
dependencies:
- lambda-calculus
- hspec
89 changes: 89 additions & 0 deletions src/Evaluator.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,89 @@
module Evaluator where

import qualified Data.Set as S

import Term (Term(..))

(∈) :: Ord a => a -> S.Set a -> Bool
(∈) = S.member

(∉):: Ord a => a -> S.Set a -> Bool
(∉) = (not . ) . (∈)

(∅) :: Monoid a => a
(∅) = mempty

(∪) :: Ord a => S.Set a -> S.Set a -> S.Set a
(∪) = S.union

fv :: S.Set Char -> Term -> S.Set Char
fv s (Var c) = if c s then S.fromList [c] else (∅)
fv s (App x y) = fv s x fv s y
fv s (Lambda x y) = fv (S.insert x s) y

fv' :: Term -> S.Set Char
fv' = fv (∅)

newVar :: S.Set Char -> Char
newVar s = head [x | x <- reverse ['a'..'z'], x s]

-- substitute Λ for free Vx in another Λ
σ :: Term -> Char -> Term -> Term
σ n x y@(Var x')
| x == x' = n -- x[x := N] ≡ N
| otherwise = y -- y[x := N] ≡ y

σ n x (App p q) = -- PQ[x := N] ≡ (P[x := N])(Q[x := N])
App
(σ n x p) -- P[x := N]
(σ n x q) -- Q[x := N]

σ n x (Lambda y p)
| x fvP = -- (λy.P)[x := N] ≡ λy.P where x ∉ FV(P)
Lambda y p
| y fvN = -- (λy.P)[x := N] ≡ λy.(P[x := N]) where y ∉ FV(N)
Lambda y (σ n x p)
| otherwise = -- (λy.P)[x := N] ≡ λz.(Pʸ→ᶻ[x := N]) where z ∉ FV(N)
Lambda z (σ n x (αCon y z p))
where
fvN = fv' n
fvP = fv' p
z = newVar fvN

-- Rename Vx to Vy in Λ
-- α-conversion is a special case of substitution
αCon :: Char -> Char -> Term -> Term
αCon x y = σ (Var y) x

isRedex :: Term -> Bool
isRedex (Var _) = False
isRedex (App (Lambda _ _) _) = True
isRedex (App x y) = isRedex x || isRedex y
isRedex (Lambda _ y) = isRedex y

-- Zero or one step β-reduction
β :: Term -> Term
β (Var x) = Var x
β (App (Lambda x y) n) = σ n x y
β (App x y)
| isRedex x = App (β x) y
| isRedex y = App x (β y)
| otherwise = App x y
β (Lambda x y) = Lambda x (β y)

-- Zero or more step β-reduction
-- Reduces to β-normal-form (βnf)
βnf :: Term -> Term
βnf t
| isRedex t = βnf (β t)
| otherwise = t

-- α-equivalence
αEquiv :: Term -> Term -> Bool
αEquiv (Var x) (Var y) = x == y
αEquiv (App w x) (App y z) = αEquiv w y && αEquiv x z
αEquiv m@(Lambda w _) (Lambda y z) = Lambda w (αCon y w z) == m
αEquiv _ _ = False

(≡) :: Term -> Term -> Bool
(≡) m n = αEquiv (βnf m) (βnf n)
51 changes: 51 additions & 0 deletions src/Parser.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
module Parser where

import Text.ParserCombinators.Parsec

import Term (Term(..))

asciiAlpha = oneOf ['a'..'z']

parseVar :: Parser Term
parseVar = Var <$> asciiAlpha

handleCurry :: [Char] -> Term -> Term
handleCurry [x] body = Lambda x body
handleCurry (x:xs) body = foldl (flip Lambda) (Lambda x body) xs

parseLambda :: Parser Term
parseLambda = do
char 'λ'
bindings <- many1 asciiAlpha
char '.'
handleCurry (reverse bindings) <$> parseTerms

parseApp :: Parser Term
parseApp = App <$> simple <*> simple

simple :: Parser Term
simple = try parseVar <|> try parens

parens :: Parser Term
parens = char '(' *> parseTerms <* char ')'

parseTerm :: Parser Term
parseTerm = try parseLambda <|> try parseApp <|> simple

termsToApps :: [Term] -> Term
termsToApps [x] = x
termsToApps (x:xs) = foldl App x xs

parseTerms :: Parser Term
parseTerms = termsToApps <$> many1 parseTerm

p :: Parser Term
p = termsToApps <$> (try (many1 simple) <|> many1 parseTerm)

runParse :: String -> Either ParseError Term
runParse = parse p "Lambda-Calc"

unsafeRunParse :: String -> Term
unsafeRunParse s = case parse p "Lambda-Calc" s of
(Left e) -> error (show e)
(Right x) -> x
16 changes: 16 additions & 0 deletions src/PrettyPrinter.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
module PrettyPrinter where

import Term (Term(..))

termToString :: Term -> String
termToString (Var x) = [x]
termToString (App x@(Var _) y@(App _ _)) = termToString x <> "(" <> termToString y <> ")"
termToString (App x@(Lambda _ _) y@(Lambda _ _)) = "(" <> termToString x <> ")" <> "(" <> termToString y <> ")"
termToString (App x@(Lambda _ _) y) = "(" <> termToString x <> ")" <> termToString y
termToString (App x y@(Lambda _ _)) = termToString x <> "(" <> termToString y <> ")"
termToString (App x y) = termToString x <> termToString y
termToString (Lambda head body) = "λ" <> [head] <> "." <> termToString body

pp :: Term -> IO ()
pp = putStrLn . termToString

7 changes: 7 additions & 0 deletions src/Term.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
module Term where

-- Λ = V | (Λ Λ) | (λV.Λ)
data Term = Var Char
| Lambda Char Term
| App Term Term
deriving (Show, Eq)
Loading

0 comments on commit b383686

Please sign in to comment.