Skip to content

Commit dc686f5

Browse files
MAnyKeyMAnyKey
committed
pull from jan repo
1 parent 44549f7 commit dc686f5

File tree

1 file changed

+114
-105
lines changed

1 file changed

+114
-105
lines changed

‎UnTyLambda/Interpreter.hs

Lines changed: 114 additions & 105 deletions
Original file line numberDiff line numberDiff line change
@@ -1,153 +1,162 @@
1+
{-# LANGUAGE ScopedTypeVariables #-}
2+
--------------------------------------------------------------------------------
3+
-- В данном задании требуется реализовать интерпретатор для
4+
-- нетипизированной лямбды
5+
--------------------------------------------------------------------------------
6+
17
module UnTyLambda.Interpreter where
28

9+
-- Какие-то импорты. Заметьте, что в этом задании надо
10+
-- использовать обычную Prelude
11+
import Prelude hiding (catch)
12+
import Control.Exception
13+
14+
------------------------------------------------------------
15+
-- Определение дататайпа для нетипизированной лямбды
316
type Variable = String
17+
data Term = Var Variable | Lam Variable Term | App Term Term deriving (Show,Read)
418

5-
-- Лямбда-терм
6-
data Term = Var Variable
7-
| Abs Variable Term
8-
| App Term Term
9-
deriving (Show)
19+
------------------------------------------------------------
20+
-- Дальше всё на ваше усмотрение
1021

11-
-- Тип [ a ] == Типу List a
12-
-- значение [] == значению Nil
13-
-- значение [ a ] == значению Cons a Nil
14-
-- конструктор (:) == конструктору Cons
22+
-- Если внутри будете использовать именованное представление, то
23+
-- я тут решил немного вам помочь
24+
-- (иначе говоря, код из этого раздела можно совсем выкинуть,
25+
-- если хочется)
1526

16-
-- Свободные переменные терма
17-
free (Var v) = [v]
18-
free (Abs v t) = filter (/= v) . free $ t -- /= это <<не равно>>
27+
free (Var v) = [ v ]
28+
free (Lam v t) = filter (/= v) . free $ t
1929
free (App t t') = (free t) ++ (free t')
2030

21-
binded (Var v) = []
22-
binded (Abs v t) = v : binded t
23-
binded (App t t') = binded t ++ binded t'
31+
-- subst :: Term -> Variable -> Term -> Term
32+
-- subst t@(Var v) var what = if v == var then what else t
33+
-- subst t@(Lam v b) var what = if v == var then t else Lam v (subst b var what)
34+
-- subst (App t t') var what = App (subst t var what) (subst t' var what)
2435

25-
-- Заменить все свободные вхождения переменной var на what в терме term
2636
subst var what term = case term of
2737
Var v -> if v == var then what else term
28-
Abs v t -> if v == var then term else Abs v (subst var what t)
38+
Lam v t -> if v == var then term else Lam v (subst var what t)
2939
App t t' -> App (subst var what t) (subst var what t')
3040

31-
-- Генерирует список имён, производных от v, не входящих в fv
32-
newname fv v = head . filter (\x -> not . elem x $ fv) . iterate ('_':) $ v
41+
newname fv = head . filter (not . flip elem fv) . iterate ('_':)
42+
43+
--- ...
3344

3445
-- Обычная бета-редукция, хендлящая переименования переменных
3546
betaReduct :: Variable -> Term -> Term -> Term
3647
betaReduct var what term = subst var what $ renameBindings (free what) term
3748
where renameBindings vars subterm = case subterm of
3849
Var _ -> subterm
3950
App t t' -> App (renameBindings vars t) (renameBindings vars t')
40-
Abs n t -> Abs nn newt
51+
Lam n t -> Lam nn newt
4152
where nameUsed = elem n vars
4253
nn = if nameUsed then newname (vars ++ free t) n else n
4354
newt = if nameUsed then subst n (Var nn) t else t
4455

4556
hasRedexes (Var _) = False
46-
hasRedexes (Abs v t) = hasRedexes t
47-
hasRedexes (App (Abs _ t) t') = True
57+
hasRedexes (Lam v t) = hasRedexes t
58+
hasRedexes (App (Lam _ t) t') = True
4859
hasRedexes (App t t') = hasRedexes t || hasRedexes t'
4960

50-
-- Нормализация нормальным порядком терма term
51-
normal' :: Term -> Term
52-
normal' term = if (hasRedexes term) then normal' $ normalReduce term else term
53-
5461
normalReduce term = case term of
5562
Var _ -> term
56-
Abs var subterm -> Abs var $ normalReduce subterm
57-
App (Abs var subterm) term' -> betaReduct var term' subterm
63+
Lam var subterm -> Lam var $ normalReduce subterm
64+
App (Lam var subterm) term' -> betaReduct var term' subterm
5865
App term term' -> if hasRedexes term
5966
then App (normalReduce term) term'
6067
else App term $ normalReduce term'
6168

62-
-- Нормализация аппликативным порядком терма term
63-
applicative' :: Term -> Term
64-
applicative' term = if (hasRedexes term) then applicative' $ applicativeReduce term else term
65-
6669
applicativeReduce term = case term of
6770
Var _ -> term
68-
Abs var subterm -> Abs var $ applicativeReduce subterm
71+
Lam var subterm -> Lam var $ applicativeReduce subterm
6972
App term term' -> if hasRedexes term'
7073
then App term $ applicativeReduce term'
7174
else case term of
72-
Abs v subt -> betaReduct v term' subt
75+
Lam v subt -> betaReduct v term' subt
7376
_ -> App (applicativeReduce term) term'
7477

78+
inWeakHeadForm (Var _) = True
79+
inWeakHeadForm (Lam _ _) = True
80+
inWeakHeadForm (App (Lam _ t) t') = False
81+
inWeakHeadForm (App t t') = inWeakHeadForm t
7582

76-
-- Маркер конца ресурсов
77-
data TooLoong = TooLoong deriving Show
83+
weakHeadReduce term = case term of
84+
App (Lam v t) t2 -> subst v t2 t
85+
App t1 t2 | not (inWeakHeadForm t1) -> App (weakHeadReduce t1) t2
86+
_ -> term
7887

79-
-- (*) Нормализация нормальным порядком терма term за неболее чем n шагов.
80-
-- Результат: Или числа итераций недостаточно, чтобы достичь нормальной
81-
-- формы. Или (число нерастраченных итераций, терм в нормальной форме).
82-
--
83-
normal :: Int -> Term -> Either TooLoong (Int, Term)
84-
normal n term
85-
| n < 0 = Left TooLoong
86-
| otherwise = if (hasRedexes term)
87-
then normal (n - 1) $ normalReduce term
88-
else Right (n, term)
88+
------------------------------------------------------------
89+
-- За исключением того, что требуется реализовать следующие
90+
-- стратегии нормализации (они все принимают максимальное
91+
-- число шагов интерпретатора в качестве первого
92+
-- параметра (n); если за n шагов нормализовать не удаётся,
93+
-- то следует бросать error, тестер его поймает):
8994

90-
-- (*) Аналогичная нормализация аппликативным порядком.
91-
applicative :: Int -> Term -> Either TooLoong (Int, Term)
92-
applicative n term
93-
| n < 0 = Left TooLoong
94-
| otherwise = if (hasRedexes term)
95-
then applicative (n - 1) $ applicativeReduce term
96-
else Right (n, term)
97-
98-
-- (***) Придумайте и реализуйте обобщённую функцию, выражающую некоторое
99-
-- семейство стратегий редуцирования. В том смысле, что номальная, нормальная
100-
-- головная, нормальная слабо-головная и аппликативная стратегии
101-
-- при помощи этой функции будут выражаться некоторым элементарным образом.
102-
-- Аргумент n можно отбросить, а можно оставить.
103-
--
104-
-- strategy = ?
105-
--
106-
-- normal = strategy ?
107-
-- hnf = strategy ?
108-
-- whnf = strategy ?
109-
-- applicative = strategy ?
110-
--
111-
-- Какие ещё стратегии редуцирования вы знаете? Можно ли их выразить
112-
-- при помощи этой стратегии? Если да, то как?
113-
-- Если нет, то можно ли реализовать аналогичную функцию для _всех_
114-
-- возможных стратегий редуцирования, а не только для такого семейства?
115-
-- Если да, то как? Если нет, то почему?
95+
wh, no, wa, sa :: Integer -> Term -> Term
11696

117-
--------------------------------------------------------
118-
119-
-- Область тестирования
120-
121-
loop' = Abs "x" $ App (Var "x") (Var "x")
122-
loop = App loop' loop'
123-
124-
u = Abs "a" $ Abs "b" $ App (Var "a") $ App (Var "b") (Var "_b")
125-
v = Abs "a" $ Abs "b" $ App (App (Var "a") (Var "b")) (Var "_b")
126-
w = Abs "a" $ Abs "b" $ Abs "c" $ Abs "d" $ App (App (Var "a") (Var "b")) (App (Var "c") (Var "d"))
97+
-- Редукция аппликативным порядком
98+
sa n term
99+
| n < 0 = error $ "Too long sequence at [" ++ show term ++ "]"
100+
| otherwise = if (hasRedexes term)
101+
then sa (n - 1) $ applicativeReduce term
102+
else term
127103

128-
main = test 100
129-
[ ("no", normal)
130-
, ("ap", applicative) ]
104+
-- Нормализация нормальным порядком
105+
no n term
106+
| n < 0 = error $ "Too long sequence at [" ++ show term ++ "]"
107+
| otherwise = if (hasRedexes term)
108+
then no (n - 1) $ normalReduce term
109+
else term
110+
111+
-- Редукция в слабую головную нормальную форму
112+
wh n term
113+
| n < 0 = error $ "Too long sequence at [" ++ show term ++ "]"
114+
| otherwise = if (inWeakHeadForm term)
115+
then term
116+
else wh (n - 1) $ weakHeadReduce term
117+
118+
119+
-- (*) (не обязательно) Редукция "слабым" аппликативным порядком.
120+
-- Отличается от обычного аппликативного тем, что не лезет внутрь
121+
-- лямбд и правые части аппликаций, когда это возможно.
122+
wa = undefined
123+
124+
-- Замечание: cкорость работы вашего интерпретатора специально не оценивается,
125+
-- потому можно использовать свой изоморфный (с точностью до альфа-конверсии)
126+
-- тип для представления термов и преобразовывать Term в него и обратно.
127+
128+
-- Перечисление всех этих порядков (в порядке отличном от
129+
-- определения, да)
130+
orders =
131+
[ ("wh", wh)
132+
, ("no", no)
133+
-- , ("wa", wa) -- Можно раскоментировать, да
134+
, ("sa", sa) ]
135+
136+
------------------------------------------------------------
137+
-- Игнорируйте это, если выглядит непонятно
138+
pall term = mapM_ $ \(d, x) -> putStr (d ++ ": ") >> catch (let t = x 1000 term in seq t (print t)) (\(e :: SomeException) -> print e)
139+
testfuncs funcs = mapM_ $ \t -> putStr "===== " >> print t >> pall t funcs
140+
141+
------------------------------------------------------------
142+
-- Сюда можно добавлять тесты
143+
lamxx = Lam "x" $ App (Var "x") (Var "x")
144+
omega = App lamxx lamxx
145+
146+
test = testfuncs orders
131147
[ Var "a"
132-
, u
133-
, v
134-
, loop'
135-
, u `App` Var "a"
136-
, v `App` Var "a"
137-
, u `App` Var "b"
138-
, v `App` Var "b"
139-
, u `App` Var "_b"
140-
, v `App` Var "_b"
141-
, (u `App` Var "_b") `App` Var "_b"
142-
, (v `App` Var "_b") `App` Var "_b"
143-
, w
144-
, w `App` (Abs "a" (Var "a") `App` (Abs "b" $ Var "b"))
145-
, (w `App` Abs "a" (Var "b")) `App` loop
146-
, loop
148+
, Lam "x" $ (Lam "y" $ Var "y") `App` (Var "x")
149+
, (Lam "x" $ Lam "y" $ Var "x") `App` (Var "y")
150+
, omega
147151
]
148152

149-
-- Если вы не понимаете как это работает, то пока и не надо
150-
pall n term = mapM_ (\(desc, reduce) -> putStr (desc ++ ": ") >> print (reduce n term))
151-
152-
test :: Show a => Int -> [(String, Int -> Term -> a)] -> [Term] -> IO ()
153-
test n funcs = mapM_ (\term -> print term >> pall n term funcs)
153+
------------------------------------------------------------
154+
-- Немного теоретических замечаний, если они вас волнуют
155+
--
156+
-- Следует специально отметить, что поскольку в конце теста
157+
-- результат вычисления печатают, то ленивость Haskell не
158+
-- влияет на семантику интерпретируемого исчисления.
159+
--
160+
-- Чтобы это особенно подчеркнуть в тестере выше я написал
161+
-- seq в интересном месте (хотя конкретно это там ничего не
162+
-- гарантирует, на самом-то деле).

0 commit comments

Comments
 (0)