lambda-evaluator.rkt

#lang racket
(require racket/set)

; exp := ('var "var")
;     |  ('app exp exp)
;     |  ('abs "param" exp)

; var := '(var "x")
; abs := '(abs "x" (var "x"))
; app := '(app (abs "a" (var "a")) (var "x"))


(define condition
  '(app (app (abs "t" (abs "f" (var "t"))) (var "then")) (var "else")))


(define (show expr)
  (match expr
    [(list 'var id) id]
    [(list 'abs id body) (string-append "(λ " id " . " (show body) ")")]
    [(list 'app left right) (string-append "(" (show left) " " (show right) ")")]))

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

(define (normalize tree)
  (if (not (normalForm tree))
      (normalize (normalStep tree))
      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
|#

(define (normalForm tree)
  (match tree
    [(list 'var _) #t]
    [(list 'abs _ body) (normalForm body)]
    [(list 'app (list 'abs _ _) _) #f]
    [(list 'app left right) (and (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
|#

(define (normalStep tree)
  (match tree
    [(list 'abs id body) '(abs ,id ,(normalStep body))]
    [(list 'app (list 'abs par body) right) (beta par right (alpha par (free right) body))]
    [(list 'app left right) (if (normalForm left)
                                (list 'app left (normalStep right))
                                (list 'app (normalStep left) right))]))

#|
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
|#

(define (free tree)
  (define (free2 bound freeVars tree)
    (match tree
      [(list 'var id) (if (set-member? bound id)
                          freeVars
                          (set-add freeVars id))]
      [(list 'abs par body) (free2 (set-add bound par) freeVars body)]
      [(list 'app left right) (let ([leftFree (free2 bound freeVars left)]
                                    [rightFree (free2 bound freeVars right)])
                                (set-union leftFree rightFree))]))

  (free2 (set) (set) tree))


#|
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
|#

(define cntr 0)
(define (getNewName oldName)
  (let ([name (string-append oldName (number->string cntr))])
    (set! cntr (+ cntr 1))
    name))

(define (alpha par freeArg tree)
  (match tree
    [(list 'abs param body) (if (equal? param par)
                              tree
                              (if (and (set-member? (free body) par)
                                       (set-member? freeArg param))
                                  (let ([newName (getNewName param)]
                                        [replac '(var ,newName)])
                                    (list 'abs newName (alpha param freeArg (beta param replac body))))
                                  tree))]
    [(list 'app left right) (list 'app (alpha par freeArg left) (alpha par freeArg right))]
    [else 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)
|#

(define (beta par value target)
  (match target
    [(list 'var id) (if (equal? par id)
                        value
                        target)]
    [(list 'abs parName body) (if (equal? par parName)
                                  target
                                  (list 'abs parName (beta par value body)))]
    [(list 'app left right) (list 'app (beta par value left) (beta par value right))]))