www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

lambda.mlish (2149B)

      1 #lang s-exp "../../../mlish.rkt"
      2 (require "../../rackunit-typechecking.rkt")
      3 
      4 ;; Lambda Calculus interpreter
      5 
      6 
      7 ;; Problems:
      8 ;; - Cannot use variable in head position of match (gotta exhaust constructors)
      9 
     10 ;; -----------------------------------------------------------------------------
     11 
     12 (define-type Λ
     13   (Var Int)
     14   (Lambda Int Λ)
     15   (App Λ Λ))
     16 
     17 (define (fresh [e : Λ] → Int)
     18   (match e with
     19    [Var i -> (+ i 1)]
     20    [Lambda i e -> (+ i (fresh e))]
     21    [App e1 e2 -> (+ 1 (+ (fresh e1) (fresh e2)))]))
     22 
     23 (define (subst [e : Λ] [i : Int] [v : Λ] → Λ)
     24   (match e with
     25    [Var j ->
     26     (if (= i j)
     27       v
     28       e)]
     29    [Lambda j e2 ->
     30     (if (= i j)
     31       e
     32       (Lambda j (subst e2 i v)))]
     33    [App e1 e2 ->
     34     (App (subst e1 i v) (subst e2 i v))]))
     35 
     36 (define (simpl-aux [e : Λ] [i : Int] → (× Int Λ))
     37   (match e with
     38    [Var j -> (tup i (Var j))]
     39    [Lambda j e ->
     40     (match (simpl-aux (subst e j (Var i)) (+ i 1)) with
     41      [k e2 ->
     42       (tup k (Lambda i e2))])]
     43    [App e1 e2 ->
     44     (match (simpl-aux e1 i) with
     45      [j e1 ->
     46       (match (simpl-aux e2 j) with
     47        [k e2 ->
     48         (tup k (App e1 e2))])])]))
     49 
     50 (define (simpl [e : Λ] → Λ)
     51   (match (simpl-aux e 0) with
     52    [i e2 -> e2]))
     53 
     54 (define (eval [e : Λ] → Λ)
     55   (match e with
     56    [Var i -> (Var i)]
     57    [Lambda i e1 -> e]
     58    [App e1 e2 ->
     59     (match (eval e1) with
     60      [Var i -> (Var -1)]
     61      [App e1 e2 -> (Var -2)]
     62      [Lambda i e ->
     63       (match (tup 0 (eval e2)) with
     64        [zero v2 ->
     65         (eval (subst e i (subst v2 i (Var (+ (fresh e) (fresh v2))))))])])]))
     66 
     67 ;; -----------------------------------------------------------------------------
     68 
     69 (define I (Lambda 0 (Var 0)))
     70 (define K (Lambda 0 (Lambda 1 (Var 0))))
     71 (define S (Lambda 0 (Lambda 1 (Lambda 2 (App (App (Var 0) (Var 2)) (App (Var 1) (Var 2)))))))
     72 (define false (App S K))
     73 
     74 ;; -----------------------------------------------------------------------------
     75 
     76 (check-type
     77   (eval I)
     78   : Λ
     79   ⇒ I)
     80 
     81 (check-type
     82   (eval (App I I))
     83   : Λ
     84   ⇒ I)
     85 
     86 (check-type
     87   (eval (App (App K (Var 2)) (Var 3)))
     88   : Λ
     89   ⇒ (Var 2))
     90 
     91 (check-type
     92   (eval (App (App false (Var 2)) (Var 3)))
     93   : Λ
     94   ⇒ (Var 3))
     95