lambda-evaluator.elm

module Lambdulus exposing (..)

import Set exposing (Set)

type Expression
  = Variable String
  | Abstraction String Expression
  | Application Expression Expression


show : Expression -> String
show tree =
  case tree of
    Variable name -> name
    Abstraction arg body -> "(λ " ++ arg ++ " . " ++ show body ++ ")"
    Application left right -> "(" ++ show left ++ " " ++ show right ++ ")"


normalize : Expression -> Expression
normalize tree =
  if not (normalForm tree)
  then
    normalize (normalStep tree)
  else
    tree


normalForm : Expression -> Bool
normalForm tree =
  case tree of
    Variable _ -> True
    Abstraction _ body -> normalForm body
    Application (Abstraction _ _) _ -> False
    Application left right -> normalForm left && normalForm right


normalStep : Expression -> Expression
normalStep tree =
  case tree of
    Abstraction arg body -> Abstraction arg (normalStep body)
    Application (Abstraction arg body) right -> beta arg right (alpha arg (free right) body)
    Application left right ->
      if normalForm left
      then Application left (normalStep right)
      else Application (normalStep left) right
    _ -> tree


free : Expression -> Set String
free = free2 Set.empty Set.empty

free2 : Set String -> Set String -> Expression -> Set String
free2 bound freeVars tree =
  case tree of
    Variable name ->
      if Set.member name bound
      then
        freeVars
      else
        Set.insert name freeVars
    Abstraction arg body -> free2 (Set.insert arg bound) freeVars body
    Application left right ->
      let
        leftFree = free2 bound freeVars left
        rightFree = free2 bound freeVars right
      in
        Set.union leftFree rightFree


alpha : String -> Set String -> Expression -> Expression
alpha arg freeArg tree =
  let
    alphaCurr = alpha arg freeArg
  in
  case tree of
    Abstraction argument body ->
      if argument == arg -- shadowing
      then tree
      else if Set.member arg (free body) && Set.member argument freeArg then
      -- free original Argument in Body && current Argument in conflict with free Vars from Right Value
        let
          newName = "_" ++ argument ++ "_"
          replacement = Variable ("_" ++ argument ++ "_")
        in
        Abstraction newName (alphaCurr (beta argument replacement body))
      else tree
    Application left right -> Application (alphaCurr left) (alphaCurr right)
    _ -> tree


beta : String -> Expression -> Expression -> Expression
beta arg value target =
  let
    betaCurr = beta arg value
  in
  case target of
    Variable name ->
      if arg == name
      then
        value
      else
        target
    Abstraction argName body ->
      if arg == argName
      then
        target
      else
        Abstraction argName (betaCurr body)
    Application left right -> Application (betaCurr left) (betaCurr right)


x = Variable "x"

y = Variable "y"

z = Variable "z"

s = Variable "s"

-- (x (x y))
app = Application x (Application x y)

-- (\ x . x (x y))
l = Abstraction "x" app

-- (\ y . (\ x . x (x y)))
l2 = Abstraction "y" l

app2 = Application x y

-- (\ y . (\ x . x (x y))) (x y) ::: conflict with free x in argument
eXp = Application l2 app2


-- (\ z . (\ y . (\ x . x (x z)))) (x y)

-- (x (y z))
app23 = Application x (Application y z)

-- (\ x . x (y z))
l23 = Abstraction "x" app23

-- (\ y . (\ x . x (y z)))
l223 = Abstraction "y" l23

app223 = Application x y

eXp23 = Abstraction "z" l223

eXP23 = Application eXp23 app223


-- (\ x . f (x x))
fxx = Abstraction "x" (Application (Variable "f") (Application (Variable "x") (Variable "x")))
-- (\ f . (\ x . f (x x)) (\ x . f (x x)) )
yComb = Abstraction "f" (Application fxx fxx)

-- true : (λ t f . t)
ttrue = Abstraction "t" (Abstraction "f" (Variable "t"))

-- false
ffalse = Abstraction "t" (Abstraction "f" (Variable "f"))

-- zero : (λ n . n (λ x . (λ t f . f)) (λ t f . t))
zero = Abstraction "n" (Application (Application (Variable "n") (Abstraction "x" ffalse) ) ttrue)
-- one
one = Abstraction "s" (Abstraction "z" (Application (Variable "s") (Variable "z") ))

-- PRED : (λ x s z . x (λ f g . g (f s)) (λ g . z) (λ u . u))
pred = (Abstraction "x" (Abstraction "s" (Abstraction "z" (Application (Application (Application (Variable "x") (Abstraction "f" (Abstraction "g" (Application (Variable "g") (Application (Variable "f") (Variable "s") ) ) ) ) ) (Abstraction "g" (Variable "z") ) ) (Abstraction "u" (Variable "u") ) ))))
-- minus : (λ m n . (n PRED) m)
minus = Abstraction "m" (Abstraction "n" (Application (Application (Variable "n") pred) (Variable "m")))
-- times : (λ x y z . x (y z))
times = Abstraction "x" (Abstraction "y" (Abstraction "s" (Application (x) (Application (y) (s) ) ) ))

nminus1 = Application (Application minus (Variable "n") ) one
multipl = Application (Application times (Variable "n") ) (Application (Variable "f") nminus1) 

-- factorial : (\ f n . zero n 1 (* n (f (- n 1))) )
fact = Abstraction "f" (Abstraction "n" (Application (Application (Application zero (Variable "n")) one ) (multipl) ))

-- 3
three = Abstraction "s" (Abstraction "z" (Application (Variable "s") (Application (Variable "s") (Application (Variable "s") (Variable "z") ) )))
-- 6
six = Abstraction "s" (Abstraction "z" (Application (Variable "s") (Application (Variable "s") (Application (Variable "s") (Application (Variable "s") (Application (Variable "s") (Application (Variable "s") (Variable "z") ) ) ) ))))

-- Y fact 3
factOfThree = Application (Application (yComb) (fact)) (three)
factOfSix = Application (Application yComb fact) six

threeMinusOne = Application (Application minus three ) (one)

-- plus : (λ x y s z . x s (y s z))
pPart = Application (Variable "x") (Variable "s")
ppPart = Application (Application (Variable "y") (Variable "s")) (Variable "z")
plus = Abstraction "x" (Abstraction "y" (Abstraction "s" (Abstraction "z" (Application pPart ppPart) )))

onePlusOne = Application (Application plus one) (one)

-- test of something very weird - it works because of the order in multiplication (* n .... ) - once the n is zero then the neverending recursion ends and 0 is returned
fooo = Abstraction "f" (Abstraction "n" (multipl))
fooTest = Application (Application (yComb) (fooo)) (three)