-
Notifications
You must be signed in to change notification settings - Fork 1
/
nbe.hs
102 lines (77 loc) · 2.3 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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
data Type = Base | Arrow Type Type
deriving (Eq, Show)
idType :: Type
idType = Arrow Base Base
kType :: Type
kType = Arrow Base idType
data Term = Var Int | App Term Term | Lam Term
deriving (Eq, Show)
i :: Term
i = Lam (Var 0)
k :: Term
k = Lam (Lam (Var 1))
s :: Term
s = Lam (Lam (Lam (App (App (Var 2) (Var 0)) (App (Var 1) (Var 0)))))
type TermFamily = Int -> Term
data Value = Object TermFamily | Function (Value -> Value)
deriving Eq
x :: Int -> TermFamily
x n k = Var (k - n) -- би трябвало max(k - n, 0), но при коректно използване винаги k ≥ n
vf :: Value -> Value
vf (Object a) = Object a
vf (Function g) = g (Object (x 4))
v :: Value
v = Function vf
type Valuation = [Value]
δ :: Valuation
δ = map (\i -> Object (x i)) [0 .. 5]
value :: Term -> Valuation -> Value
value (Var i) ξ = ξ !! i
value (App m n) ξ = g (value n ξ)
where Function g = value m ξ
value (Lam m) ξ = Function (\a -> value m (a:ξ))
kv :: Value
kv = value k δ
app :: TermFamily -> TermFamily -> TermFamily
app f1 f2 k = App (f1 k) (f2 k)
reify :: Type -> TermFamily -> Value
reify Base f = Object f
reify (Arrow ρ σ) f = Function (\a -> reify σ (app f (reflect ρ a)))
reflect :: Type -> Value -> TermFamily
reflect Base (Object f) = f
reflect (Arrow ρ σ) (Function g) =
\k -> Lam ((reflect σ (g (reify ρ (x (k + 1))))) (k + 1))
nbe :: Type -> Term -> Term
nbe τ m = reflect τ (value m []) 0
iter :: Int -> Int -> Int -> Term
iter 0 f x = Var x
iter n f x = App (Var f) (iter (n - 1) f x)
c :: Int -> Term
c n = Lam (Lam (iter n 1 0))
c5 :: Term
c5 = c 5
numType :: Type
-- (α => α) => α => α
numType = Arrow (Arrow Base Base) (Arrow Base Base)
plus :: Term
-- plus = \n m f x -> n f (m f x)
plus = Lam (Lam (Lam (Lam (App (App (Var 3) (Var 1))
(App (App (Var 2) (Var 1)) (Var 0))))))
-- nbe idType (App (App s k) k)
-- Lam (Var 0) ≡ i
-- nbe numType (App (App plus (c 5)) (c 8))
{- Lam (Lam (App (Var 1)
(App (Var 1)
(App (Var 1)
(App (Var 1)
(App (Var 1)
(App (Var 1)
(App (Var 1)
(App (Var 1)
(App (Var 1)
(App (Var 1)
(App (Var 1)
(App (Var 1)
(App (Var 1) (Var 0)))))))))))))))
≡ c 13
-}