Бета-преобразование для лямбда-исчисления Haskell - PullRequest
Новая
       8

Бета-преобразование для лямбда-исчисления Haskell

0 голосов
/ 06 декабря 2018

Я хочу реализовать функцию, которая выполняет бета-преобразование до лямбда-выражения, где мое лямбда-выражение имеет тип: 

data Expr = App Expr Expr | Abs Int Expr | Var Int deriving (Show,Eq)

Моя функция оценки на данный момент: 

eval1cbv :: Expr -> Expr
eval1cbv (Var x) = (Var x)
eval1cbv (Abs x e) = (Abs x e)
eval1cbv (App (Abs x e1) e@(Abs y e2)) = eval1cbv (subst e1 x e)
eval1cbv (App e@(Abs x e1) e2) =  eval1cbv (subst e2 x e)  
eval1cbv (App e1 e2) = (App (eval1cbv e1) e2)

где subst - функция, используемая для определения замещения.

Однако, когда я пытаюсь уменьшить выражение с помощью бета-сокращения, я получаю ошибку неисчерпывающего паттерна и не могу понять, почему.Что я могу сделать, чтобы это исправить, так это добавить дополнительный регистр внизу, например так: 

eval :: Expr -> Expr
eval (Abs x e) = (Abs x e)
eval (App (Abs x e1) e@(Abs y e2)) = subst e1 x e
eval (App e@(Abs x e1) e2) = App e (eval e2)
eval (App e1 e2) = App (eval e1) e2
eval (Var x) = Var x

Однако, если я это сделаю, то лямбда-выражение вообще не будет уменьшаться, а это означает, что вводтакой же, как вывод функции.

Итак, если я попытаюсь оценить простой случай, такой как:

eval (App (Abs 2 (Var 2)) (Abs 3 (Var 3))), он работает нормально, давая ->Abs 3 (Var 3)

, но когда я запускаю его для более крупного теста, например:

eval (App (Abs 1 (Abs 2 (Var 1)))) (Var 3))я получаю:

  1. неисчерпывающие шаблоны, если я использую первую функцию без добавления последнего регистра
  2. или точно такое же выражение App (Abs 1 (Abs 2 (Var 1))) (Вариант 3), который, очевидно, не уменьшается, если я добавлю последний случай

Может кто-нибудь помочь мне разобраться, пожалуйста?:)

1 Ответ

0 голосов
/ 06 декабря 2018

, но когда я запускаю его для более крупного теста, например: 

eval (App (Abs 1 (Abs 2 (Var 1))) (Var 3))

Когда вы пытаетесь применить что-то вида Abs x e к Var y, выв этой ветке 

eval (App e@(Abs x e1) e2) = App e (eval e2)

, то есть, 

  App (Abs x e) (Var y)
= App (Abs x e) (eval (Var y))
= App (Abs x e) (Var y)

Это не то, что вы хотите сделать.И (Abs x e), и (Var y) находятся в нормальной форме (т.е. оценены), поэтому вы должны были заменить.Похоже, вы рассматриваете только лямбды, а не переменные, как оцененные.

С вашим кодом больше проблем.Рассмотрим эту ветку, 

eval (App e1 e2) = App (eval e1) e2

Результат всегда равен App.Например, если eval e1 = Abs x e, то результат будет App (Abs x e) e2.На этом он останавливается, дальнейшая оценка не выполняется.

И рассмотрите эту ветвь: 

eval (App (Abs x e1) e@(Abs y e2)) = subst e1 x e

Что произойдет, если результатом подстановки будет термин приложения?Будет ли результат оценен?

РЕДАКТИРОВАТЬ

Что касается ваших изменений, учитывая, что LamApp e1 e2 ранее вы придерживались стратегии оценки по запросу (т.е. вы оценивали e2перед заменой).Вот и все,

Вот оно e2 - лямбда, поэтому не нужно оценивать, 

eval1cbv (LamApp (LamAbs x e1) e@(LamAbs y e2)) = eval1cbv (subst e1 x e)

Здесь вы в любом случае подставляете вне зависимости от того, что является e2так что вы делаете то же самое, что и раньше.Тогда вам не нужен предыдущий случай, и теперь вы следуете стратегии оценки по имени.Я не знаю, если вы этого хотите.Также вы звоните subst с неправильными аргументами здесь.Я предполагаю, что вы имеете в виду subst e1 x e2, и вам это не нужно @e. 

eval1cbv (LamApp e@(LamAbs x e1) e2) =  eval1cbv (subst e2 x e)

Здесь вы просто оцениваете первый аргумент, который согласуется с вызовом поНазвание стратегии.Но опять же я не знаю, если это ваше намерение.

eval1cbv (LamApp e1 e2) = (LamApp (eval1cbv e1) e2)
...