/
nbe.hs
69 lines (48 loc) · 1.48 KB
/
nbe.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
data Lambda = Var Int |
App Lambda Lambda |
Λ Lambda
deriving Show
k = Λ (Λ (Var 1))
s = Λ (Λ (Λ (App
(App (Var 2) (Var 0))
(App (Var 1) (Var 0)))))
c n = Λ (Λ
(iterate (App (Var 1))
(Var 0) !! n))
ctype = Arrow itype itype
cplus = Λ (Λ (Λ (Λ (App (App (Var 3)
(Var 1))
(App (App (Var 2)
(Var 1))
(Var 0))))))
type Syn = Int -> Lambda
data Sem = Base Syn | Fun (Sem -> Sem)
type Valuation = [Sem]
data Type = Mu | Arrow Type Type
itype = Arrow Mu Mu
modify ξ a = a : ξ
evaluate :: Lambda -> Valuation -> Sem
evaluate (Var i) ξ = ξ !! i -- ξ(i)
evaluate (App m₁ m₂) ξ =
f (evaluate m₂ ξ)
where Fun f = evaluate m₁ ξ
evaluate (Λ n) ξ =
Fun (\a -> evaluate n (modify ξ a))
x :: Int -> Syn
x k l = Var (l - k)
app :: Syn -> Syn -> Syn
app m₁ m₂ k = App (m₁ k) (m₂ k)
(⇑) :: Type -> Syn -> Sem
Mu ⇑ m = Base m
(Arrow ρ σ) ⇑ m =
Fun (\a -> σ ⇑ (app m (ρ ⇓ a)))
(⇓) :: Type -> Sem -> Syn
Mu ⇓ (Base m) = m
(Arrow ρ σ) ⇓ (Fun f) =
\n -> Λ ((σ ⇓ (f (ρ ⇑ x (n+1)))) (n+1))
-- ще нормализираме само затворени термове
nbe :: Type -> Lambda -> Lambda
nbe τ m = (τ ⇓ (evaluate m [])) 0
i = nbe itype (App (App s k) k)
c8 = nbe ctype (App (App cplus (c 3))
(c 5))