UTLC.agda

module UTLC where

open import Data.String

Var : Set
Var = String

-- Untyped Lambda Calculus:

-- Terms:
-- * Variables (identified by a `Var`)
-- * Abstraction (Lambdas)
-- * Application
data Term : Set where
  -- var "x" ==> x
  var : Var -> Term
  -- abs "x" t ==> λx.t
  abs : Var -> Term -> Term
  -- app t1 t2 ==> t1 t2
  app : Term -> Term -> Term

-- Values: (Defined as a predicate)
-- * Lambdas are values
data Value : (t : Term) -> Set where
  lamv : {x : Var}{t1 : Term} -> Value (abs x t1)

-- Substitution: (Defined as a relation, not a function)
-- `Sub x s t1 t1'` roughly means that if you substitute x for s in t1, you get t1'
data Sub : Var -> Term -> Term -> Term -> Set where
     -- [x → s]x = s // substituting variable x for `s` in `x`, gives `s`
     s1 : {x : Var}{s : Term}
        -> Sub x s (var x) s
     -- [x → s]y = y // substituting variable x for `s` in `y`, gives `y`
     s2 : {x y : Var}{s : Term}
        -> Sub x s (var y) (var y)

     -- Some missing cases that I'm yet to formalise, because I left TAPL at home

     -- [x → s](t1 t2) = [x → s]t1 [x → s]t2
     -- // substituting x for `s` in `t1 t2` performs the substitution recursively to
     --    t1 and t2.
     s4 : {x : Var}{s t1 t1' t2 t2' : Term}
        -> Sub x s t1 t1'
        -> Sub x s t2 t2'
        -> Sub x s (app t1 t2) (app t1' t2')

-- Evaluation: (Again, a relation)
-- * evaluate the thing on the left in an application
-- * evaluate the thing on the right in an application,
--   but only if the thing on the left is a value
-- * If you're applying a value to a lambda, then perform substitution (beta-reduction)
data Eval : (t1 : Term) -> (t2 : Term) -> Set where

  -- if `t1` evaluates to `t1'` then `t1 t2` evaluates to `t1' t2`
  eapp1 : {t1 t1' t2 : Term}
        -> Eval t1 t1'
        -> Eval (app t1 t2) (app t1' t2)

  -- if `t1` is a value, and `t2` evaluates to `t2'` then `t1 t2` evaluates to `t1 t2'`
  eapp2 : {t1 t2 t2' : Term}{v1 : Value t1}
        -> Eval t2 t2'
        -> Eval (app t1 t2) (app t1 t2')

  -- if substituting x for t2 in t12 gives t1', then `(λx.t12) t2` gives t1'
  eappabs : {x : Var}{t12 t1' t2 : Term}{v2 : Value t2}
          -> Sub x t2 t12 t1'
          -> Eval (app (abs x t12) t2) t1'

-- Identity function: λx.x
ut_id : Term
ut_id = abs "x" (var "x")

-- Identity function applied to itself: (λx.x) (λx.x)
ut_id_app_id : Term
ut_id_app_id = app ut_id ut_id

-- A Proof that `ut_id_app_id` evaluates to `ut_id` (using substitution)
ut_id_app_id_eq_ut_id : Eval ut_id_app_id ut_id
ut_id_app_id_eq_ut_id = eappabs s1