ハスケルで糖度の高いλ項を表現するには？

Question

この文法を使用して、糖化λ-計算のデータ定義を設定します。

Λ → v 
Λ → (λ v Λ) 
Λ → (Λ Λ) 
Λ → (L Λ) 
L → (LET (LL) Λ) 
LL → (v Λ) 

ここに私がしたいことがあります。だから私はDrRacketのためにこれをしました。どのように私はハスケルのためにこれを行うことができますか？ここで

はDrRacketで私のコードです：

;; λ-expression grammar 
;; λ-calc -> v 
;; λ-calc -> (λ-calc λ-calc) 
;; λ-calc -> (λ v λ-calc) 

(define-type λ-calc 
    (λ-sym (v : symbol)) 
    (λ-app (l : λ-calc)(r : λ-calc)) 
    (λ-def (v : symbol)(expr : λ-calc)) 
) 


;; Tests;; 
(λ-sym 'x) 
(λ-app (λ-sym 'x)(λ-sym 'y)) 
(λ-def 'v (λ-app (λ-sym 'x)(λ-sym 'y))) 


;; parse : s-expression -> λ 
;; Examples 
;; 'x -> (λ-sym 'x) 
;; '(x y) -> (λ-app (λ-sym 'x) (λ-sym 'y)) 
;; '(λ x y) -> (λ-def 'x (λ-sym 'y)) 
;; '((λ x y) (x y)) -> (λ-app (λ-def 'x (λ-sym 'y)) (λ-app (λ-sym 'x) (λ-sym 'y))) 
;; Template 
;; (define (parse [expr : s-expression]) : λ 
;; (cond 
;;  [(s-exp-symbol? expr) (λ-var (... expr))] 
;;  [(s-exp-list? expr) 
;;  (let ([sl (...expr)]) 
;;  (cond 
;;   [(> (length sl) 2) (...) (parse ...))] 
;;   [else (parse ...)) (parse ...)))]) 
;;  )] 
;;  [else (error 'parse ...)])) 


(define (parse (ex : s-expression)) : λ-calc 
    (cond 
    [(s-exp-symbol? ex)(λ-sym (s-exp->symbol ex))] 
    [(s-exp-list? ex) 
    (let ([ex-list (s-exp->list ex)]) 
     (cond 
     [(= 2 (length ex-list)) (λ-app (parse (first ex-list))(parse (second ex-list)))] 
     [(= 3 (length ex-list)) (if (and (symbol=? 'λ (s-exp->symbol (first ex-list))) (s-exp-symbol? (second ex-list))) 
           (λ-def (s-exp->symbol(second ex-list)) 
           (parse (third ex-list))) 
       (error 'parse "Wrong lambda calc") 
      )] 
     [else (error 'parse "List length is unexpectedly big")] 
     ))] 
    [else (error 'parse "This is not lambda")] 
    )) 

;; Examples 
;; (λ-sym 'x) -> 'x 
;; (λ-app (λ-def 'x) (λ-sym 'y)) -> '(x y) 
;; Template 
;;(define (unparse (le : λ-calc)) : s-expression 
;; (type-case λ-calc le 
;; (λ-sym (v) (v)) 
;; (λ-app (l r)(... (unparse l)(unparse r)))) 
;; (λ-def (v expr)(... 
;;     v)(unparse expr)))) 

(define (unparse (le : λ-calc)) : s-expression 
    (type-case λ-calc le 
    (λ-sym (v) (symbol->s-exp v)) 
    (λ-app (l r)(list->s-exp (list (unparse l)(unparse r)))) 
    (λ-def (v expr)(list->s-exp 
       (list (symbol->s-exp 'λ)(symbol->s-exp v)(unparse expr)))) 
    )) 


;; λ-calc symbol λ-calc -> λ-calc 
;;Template 
;;(define (substituter [what : λ-calc] [for : symbol] [in : λ-calc]) : λ-calc 
;; (type-case λ-calc in 
;; (λ-sym (v) (if (symbol=? ...) 
;;     what 
;;     in)) 
;; (λ-app (l r) (λ-app (....) (.....))) 
;; (λ-def (v expr)(λ-def v (substituter what for expr)))) 

(define (substituter [what : λ-calc] [for : symbol] [in : λ-calc]) : λ-calc 
    (type-case λ-calc in 
    (λ-sym (v) (if (symbol=? v for) 
        what 
        in)) 
    (λ-app (l r) (λ-app (substituter what for l) 
         (substituter what for r))) 
    (λ-def (v expr)(λ-def v (substituter what for expr))) 
    ) 
) 


;; beta-transformer : ((λ x M) N) --> [M:x=N] 
;;;; (λx x) y -> (y) 
;; (((λx x) (λy y)) ((λx x) (y y))) -> ((λy y) ((λx x) (y y))) 
;; Template 
;;(define (beta-transformer (le : λ-calc)) : λ-calc;; 
;;(type-case λ-calc le 
;; (λ-sym (v)) 
;; (λ-app (l r) (if (λ-def? l) (...)) 
;;      (λ-app (beta-transformer l) (beta-transformer r)))) 
;; (λ-def (v expr) (λ-def ....))))) 

(define (beta-transformer (le : λ-calc)) : λ-calc 
    (type-case λ-calc le 
    (λ-sym (v) le) 
    (λ-app (l r) (if (λ-def? l) 
        (substituter r (λ-def-v l) (λ-def-expr l)) 
        (λ-app (beta-transformer l) (beta-transformer r)))) 
    (λ-def (v expr) (λ-def v (beta-transformer expr))))) 





;; A set represented as a list. 
;; union : (listof symbol) (listof symbol) -> (listof symbol) 
;; finding the union of two sets. 
(define (union (s1 : (listof symbol)) (s2 : (listof symbol))) : (listof symbol) 
    (foldr (lambda (x y) 
      (if (member x y) 
       y 
       (cons x y))) 
     empty 
     (append s1 s2))) 


;; set-difference : (listof symbol) (listof symbol) -> (listof symbol) 
;; To find the set difference of two sets. 
(define (set-difference (s1 : (listof symbol)) (s2 : (listof symbol))) : (listof symbol) 
    (filter (lambda (x) 
      (not (member x s2))) 
      s1)) 

;; Tests: 
(test (union empty empty) empty) 
(test (union empty (list 'x)) (list 'x)) 
(test (union (list 'x)(list 'x 'y)) (list 'x 'y)) 

(test (parse (symbol->s-exp 'y))(λ-sym 'y)) 
(test (parse '(λ x x))(λ-def 'x (λ-sym 'x))) 
(test (parse '((λ x x) y))(λ-app (λ-def 'x (λ-sym 'x)) (λ-sym 'y))) 

(test (unparse (λ-sym 'y))(symbol->s-exp 'y)) 
(test (unparse (λ-def 'x (λ-sym 'x))) '(λ x x)) 
(test (unparse (λ-app (λ-def 'x (λ-sym 'x)) (λ-sym 'y))) 
     '((λ x x) y)) 

(test (beta-transformer (parse '((λ x x) a))) 
     (parse (symbol->s-exp 'a))) 

(test (beta-transformer (parse '((λ x y) a))) 
     (parse (symbol->s-exp 'y))) 

(test (beta-transformer (parse '((λ x (a b)) k))) 
     (parse '(a b))) 

(test (beta-transformer (parse '((λ x (λ x y)) k))) 
     (parse '(λ x y))) 

(test (beta-transformer (parse '((λ x (λ y x)) k))) 
     (parse '(λ y k))) 

(test (beta-transformer (parse '((λ x (λ y (x y))) k))) 
     (parse '(λ y (k y)))) 



    ;; Redex, lambda calculus leftmost inner form 
    ;; Template 
    ;; (define (leftReduction x) : s-exp 
    ;; (type-case λ-calc 
    ;; [λ-sym (v) (v)] 
    ;; [λ-def (v expr) (unparse)] 
    ;; [λ-app (l r) (unparse)])) 
    ;;(test (leftReduction (λ-def (λ-sym 'a) (λ-(λ-def 'x (λ-sym 'x))) '(λ x x)) 'b)) 
    ;(test (leftReduction (λ-sym '3)) '3) 

    (define (leftReduction la) : s-expression 
     (type-case λ-calc la 
     [λ-sym (v) (symbol->s-exp v)] 
     [λ-def (v expr) (unparse la)] 
     [λ-app (l r) (unparse l)])) 

Answer 1

これは長いですので、私はちょうどそれを開始します。また、ハスケルのラムダインタプリタがすでにネットのどこかに書かれていると確信しています。

Haskellで

(define-type λ-calc 
    (λ-sym (v : symbol)) 
    (λ-app (l : λ-calc)(r : λ-calc)) 
    (λ-def (v : symbol)(expr : λ-calc)) 
) 

、あなたは私たちが

test1, test2, test3 :: Lcalc 
test1 = Lsym "x" 
test2 = Lapp (Lsym "x") (Lsym "y") 
test3 = Ldef "v" (Lapp (Lsym "x") (Lsym "y")) 

はラムダ項を操作するために使用することができ、対応する代数的データ型テスト

;; Tests;; 
(λ-sym 'x) 
(λ-app (λ-sym 'x)(λ-sym 'y)) 
(λ-def 'v (λ-app (λ-sym 'x)(λ-sym 'y))) 

については

type Symbol = String 
data Lcalc 
    = Lsym Symbol 
    | Lapp Lcalc Lcalc 
    | Ldef Symbol Lcalc 
    deriving (Show) -- and possibly Eq, Ord 

を定義することができ、あなたはパターンが必要ですマッチング例えば。

-- free variables 
free :: Lcalc -> [Symbol] 
free (Lsym x) = [x] 
free (Lapp s t) = nub (free s ++ free t) -- we remove duplicates here 
free (Ldef x t) = delete x (free t)