Форум программистов, компьютерный форум, киберфорум
Наши страницы
Haskell
Войти
Регистрация
Восстановить пароль
 
hardentoo
127 / 26 / 1
Регистрация: 10.10.2017
Сообщений: 32
1

Лямбда-исчисление

03.05.2018, 10:58. Просмотров 442. Ответов 7

Продолжаю учить haskell, пробую написать парсер + вычислитель бестипового лямбда-исчисления. Парсер получился такой

Haskell
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
module LambdaParser where
 
import Text.Parsec
import Text.Parsec.Combinator
import Text.Parsec.String
 
type Name = String
 
-- Определение M,N ::= x | (О»x.M) | (MN)
-- пробелы не допускаются, переменные односимвольные
data Term
  = Var Name
  | App Term
        Term
  | Lam Name
        Term
  deriving (Eq, Ord)
 
-- Красиво показываем термы
opbr = "("
clbr = ")"
dot = "."
lambda = "О»"
 
instance Show Term where
  show (Var name) = name
  show (Lam name exp) = concat [opbr, lambda, name, dot, show exp, clbr]
  show (App exp exp') = concat [opbr, show exp, show exp', clbr]
 
-- Комбинаторы
parseTerm :: Parser Term
parseTerm = parseLam <|> parseApp <|> parseVar <|> bracket
 
parseLam :: Parser Term
parseLam = do
  char 'О»' <|> char '\\'
  var <- letter
  char '.'
  body <- parseTerm
  return (Lam [var] body)
 
parseApp :: Parser Term
parseApp = do
  apps <- many1 (parseVar <|> bracket)
  return (foldl1 App apps)
 
parseVar :: Parser Term
parseVar = do
  var <- letter
  return (Var [var])
 
bracket :: Parser Term
bracket = do
  char '('
  term <- parseTerm
  char ')'
  return term
 
-- Парсер
parseExp :: String -> Term
parseExp str =
  case parse parseTerm "" str of
    Left msg -> error $ show msg
    Right term -> term
 
-- Примеры комбинаторов
scc = parseExp "О»n.О»s.О»z.s(nsz)"
plus = parseExp "О»m.О»n.О»s.О»z.ms(nsz)"
i = parseExp "О»x.x"
Не получается пока написать evaluator, не меняя определение data Term. Насколько я понимаю, можно написать его 2 способами, используя операционную семантику (tapl, глава 5) и используя денотационную (reynolds, глава 10). Пробую начать с

Haskell
1
2
3
4
eval :: Term -> Term
eval (Var name) = Var name
eval (Lam name exp) = Lam name (eval exp)
eval (App exp1 exp2) = App (eval exp1) (eval exp2)
Если кто-нибудь писал, поделитесь мыслями.

P.S Почему-то lambda символ в редакторе сообщения отображается, а при отправке заменяется на "О»".
1
QA
Эксперт
41792 / 34177 / 6122
Регистрация: 12.04.2006
Сообщений: 57,940
03.05.2018, 10:58
Ответы с готовыми решениями:

Лямбда-исчисление
Здравствуйте! В следующем выражении мне нужно выделить свободные и связанные переменные в термах и...

Лямбда-функции и формулы
Добрый день/вечер. Недавно пришлось начать копаться в применимости лямбда функций к доказательству...

Сравнительный анализ стандартных порядков редукции в лямбда-исчислении
Столкнулась с такой проблемой - на днях экзамен по Функциональному программированию. Дошла до...

λ-исчисление: Определите тип комбинатора: S = λfgx.fx(gx)
Здравствуйте! Хотел поинтересоваться а правильно ли я сделал задания. 2) Используя Y -...

Выполнить редукцию выражения лямбда-исчисление
Выплнить редукцию в аппликативном порядке. До форм NF и WHNF. Верно ли ход ? step_0\ \ \...

7
_Ivana
4111 / 1900 / 238
Регистрация: 01.03.2013
Сообщений: 5,152
Записей в блоге: 22
03.05.2018, 11:17 2
Цитата Сообщение от hardentoo Посмотреть сообщение
Если кто-нибудь писал, поделитесь мыслями.
А какие мысли вам интересны? Писал, на джаве, шарпе и своем лиспе. С выбором типа редукции - нормальным или аппликативным порядком. Самая сложность была - провести альфа-редукцию чтобы свободные переменные не становились связанными при подстановке. Вплоть до того, что имеет смысл рассмотреть нотацию Де-Брейна - ради упрощения этой задачи.
1
hardentoo
127 / 26 / 1
Регистрация: 10.10.2017
Сообщений: 32
03.05.2018, 16:58  [ТС] 3
Вроде получилось (сомневаюсь в правильности),

Haskell
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
module Lambda where
 
import Text.Parsec
import Text.Parsec.Combinator
import Text.Parsec.String
 
type Name = String
 
-- Определение M,N ::= x | (О»x.M) | (MN)
-- пробелы не допускаются, переменные односимвольные
data Term
  = Var Name
  | App Term
        Term
  | Lam Name
        Term
  deriving (Eq, Ord)
 
-- Красиво показываем термы
opbr = "("
clbr = ")"
dot = "."
lambda = "О»"
 
instance Show Term where
  show (Var name) = name
  show (Lam name exp) = concat [opbr, lambda, name, dot, show exp, clbr]
  show (App exp exp') = concat [opbr, show exp, show exp', clbr]
 
-- Комбинаторы
parseTerm :: Parser Term
parseTerm = parseLam <|> parseApp <|> parseVar <|> bracket
 
parseLam :: Parser Term
parseLam = do
  char 'О»' <|> char '\\'
  var <- letter
  char '.'
  body <- parseTerm
  return (Lam [var] body)
 
parseApp :: Parser Term
parseApp = do
  apps <- many1 (parseVar <|> bracket)
  return (foldl1 App apps)
 
parseVar :: Parser Term
parseVar = do
  var <- letter
  return (Var [var])
 
bracket :: Parser Term
bracket = do
  char '('
  term <- parseTerm
  char ')'
  return term
 
-- Парсер
parseExp :: String -> Term
parseExp str =
  case parse parseTerm "" str of
    Left msg -> error $ show msg
    Right term -> term
 
-- Примеры комбинаторов, остальные комбинаторы получаются из этих
i = parseExp "О»x.x"
k = parseExp "О»x.О»y.x"
s = parseExp "О»x.О»y.О»z.(xz)(yz)"
 
-- Вычислитель - операционная семантика, вызов по имени
type Context = [(String, Term)]
 
eval :: Context -> Term -> Term
eval context e@(Var a) = maybe e id (lookup a context)
eval context (Lam x e) = Lam x (eval context e)
eval context (App e1 e2) = apply context (eval context e1) (eval context e2)
 
apply :: Context -> Term -> Term -> Term
apply context (Lam x e) e2 = eval ((x, e2):context) e
apply context e1 e2 = App e1 e2
Берем, например, комбинатор App k (App s (App k k)) = ((λx.(λy.x))((λx.(λy.(λz.((xz)(yz)))))((λx.(λy.x))(λx.(λy.x))))) и вычисляем eval [] $ App k (App s (App k k)), получаем (λy.(λy.(λz.(λy.(λy.(λx.(λy.(yz)))))))).

Добавлено через 31 минуту
Хм, похоже неверно, так как с таким eval свободные переменные могут стать связанными, так как нет конверсий.
1
Mysterious Light
Эксперт по математике/физике
4096 / 2005 / 410
Регистрация: 19.07.2009
Сообщений: 3,025
Записей в блоге: 22
03.05.2018, 18:20 4
Цитата Сообщение от hardentoo Посмотреть сообщение
денотационную (reynolds, глава 10)
Можно ссылку?
Цитата Сообщение от hardentoo Посмотреть сообщение
Haskell
1
eval context (Lam x e) = Lam x (eval context e)
Если вычисляете до головной нормальной формы, то входить внутрь тела лямбды не нужно. Сравните: в мейнстримовых языках тело функции вычисляется только после применения этой функции к конкретному аргументу.
Если же хотите-таки войти внутрь и редуцировать тело лямбды, то стоит исключить связывание свободной переменной из контекста и связанной переменной x. Способы:
1. переименовать x в e на другую переменную.
2. удалить пару (x,_) из контекста
3. добавить в контекст (x,x) на верх. lookup в качестве значения возьмём первое значение.

Добавлено через 13 минут
Вариант не входить в тело лямбды отпадает, разве только мы готовы таскать по контексту при каждой функции.
Остальные два эквивалентны.

Не по теме:

Ваш вариант лямбда-исчисления не тьюринг-полный.

1
03.05.2018, 18:20
hardentoo
127 / 26 / 1
Регистрация: 10.10.2017
Сообщений: 32
03.05.2018, 19:35  [ТС] 5
Цитата Сообщение от Mysterious Light Посмотреть сообщение
Можно ссылку?
книга, курс, лекции, реализация (ссылка внизу страницы)

Добавлено через 8 минут
Цитата Сообщение от Mysterious Light Посмотреть сообщение
Не по теме:
Ваш вариант лямбда-исчисления не тьюринг-полный.
А чем мой вариант M,N ::= x | (λx.M) | (MN) отличается от обычного untyped lambda caluclus?

Добавлено через 36 минут
Цитата Сообщение от _Ivana Посмотреть сообщение
Самая сложность была - провести альфа-редукцию чтобы свободные переменные не становились связанными при подстановке.
Пока застрял на этом.
0
Mysterious Light
Эксперт по математике/физике
4096 / 2005 / 410
Регистрация: 19.07.2009
Сообщений: 3,025
Записей в блоге: 22
03.05.2018, 21:25 6
Забудьте прошлое сообщение: там я три раза сказал чушь.
Цитата Сообщение от hardentoo Посмотреть сообщение
А чем мой вариант M,N ::= x | (λx.M) | (MN) отличается от обычного untyped lambda caluclus?
Беру свои слова обратно, поспешно высказался.
У Вас алфавит переменных конечный, а в обычном untyped lambda caluclus счётный, поэтому я и решил, что в какой-то момент упрётесь в это ограничение.
Если присмотреться, достаточно 3 переменных, чтобы состряпать комбинаторный базис SKI, поэтому вроде бы не должно быть ограничений на вычислительные возможности.
С другой стороны, результат вычисления K(K(K(K(...(K(I)))) просто не может быть записан, если количество K больше числа символов в алфавите. Да и нормальные формы CL отличаются от лямбды.
0
hardentoo
127 / 26 / 1
Регистрация: 10.10.2017
Сообщений: 32
29.05.2018, 12:23  [ТС] 7
Парсер в первом посте не совсем верен (например он парсит "\\z.z.z") как (\\z.z) (так как остальная часть строки просто отбрасывается), так что я переписал парсер. Написал вычислитель, вроде на тестовых примерах дает верные ответы, вот что получилось, причем мне вообще не понадобился список значений переменных context, как в коде выше в функции eval.

Haskell
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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
module LambdaCalculusNaive where
 
import Control.Monad
import Data.Either
import Data.List
import Data.Maybe
import Text.ParserCombinators.Parsec
import Text.ParserCombinators.Parsec.Prim
 
-- | Определяем типы
type Name = String
 
data Term
  = Var Name
  | App Term
        Term
  | Lam Name
        Term
  deriving (Eq, Ord, Show)
 
-- | Вспомогательные выражения
wrap = replicate 1
arrow = " -> "
delimiter = " "
[dot, lambda, lambda', brLeft, brRight] = ['.', '\\', 'О»', '(', ')']
 
-- | Красиво показываем термы (вариант 1)
ppTerm1 :: Term -> String
ppTerm1 (Var s) = s
ppTerm1 (Lam x e) = concat [[brLeft], [lambda'], x, [dot], ppTerm1 e, [brRight]]
ppTerm1 (App e1 e2) = concat [[brLeft], ppTerm1 e1, ppTerm1 e2, [brRight]]
 
-- | Красиво показываем термы (вариант 2) 
ppTerm2 :: Term -> String
ppTerm2 (Var s) = s
ppTerm2 (Lam x e) = concat [[brLeft], [lambda], x, arrow, ppTerm2 e, [brRight]]
ppTerm2 (App e1 e2) = concat [[brLeft], ppTerm2 e1, ppTerm2 e2, [brRight]]
 
-- | Красиво показываем термы (вариант 3) (меньше скобок) 
ppTerm3 :: Term -> String
ppTerm3 (Var s) = s
ppTerm3 (Lam x e) = concat [[lambda'], x, arrow, ppTerm3 e]
ppTerm3 (App e1 e2) = concat [pp e1, delimiter, pp e2]
  where
    pp term@(Var s) = ppTerm3 term
    pp term@(Lam x e) = parens $ ppTerm3 term
    pp term@(App e1 e2) = parens $ ppTerm3 term
    parens term = concat [[brLeft], term, [brRight]]
 
-- | Парсер комбинаторы 
term :: Parser Term
term = lam <|> app <|> var <|> bracket
 
var :: Parser Term
var = Var . wrap <$> letter
 
lam :: Parser Term
lam = Lam <$> (char lambda *> (wrap <$> letter) <* char dot) <*> term
 
bracket :: Parser Term
bracket = char brLeft *> term <* char brRight
 
app :: Parser Term
app = foldl1 App <$> many1 (var <|> bracket)
 
chunk :: Parser String
chunk = term >> getInput
 
-- | Парсер
parseTerm :: String -> Term
parseTerm str =
  case parse chunk "" str of
    Left msg -> error $ show msg
    Right str' ->
      if not (null str')
        then error $ show "Left some input"
        else case parse term "" str of
               Left msg' -> error $ show msg'
               Right term -> term
 
-- | Ищем все свободные переменные в терме
freeVars :: Term -> [Name]
freeVars (Var s) = [s]
freeVars (App e1 e2) = freeVars e1 `union` freeVars e2
freeVars (Lam x e) = freeVars e \\ [x]
 
-- Бесконечный список имен для альфа конверсий
allNames :: [String]
allNames = [1 ..] >>= (`replicateM` ['a' .. 'z'])
 
allNames' :: [String]
allNames' = [2 ..] >>= (`replicateM` ['a' .. 'z'])
 
--  Альфа конверсия, все связанные переменные получают новые имена
renames :: [String] -> Term -> Term
renames source (Lam x e) = Lam newName $ renames (tail updateSource) e2
  where
    newName = head updateSource
    updateSource = source \\ freeVars e
    e2 = subst x (Var newName) e
renames source (App e1 e2) = App (renames source e1) (renames source e2)
renames _ x = x
 
-- | Бетта редукция
--   subst v e1 e2 подставляет терм e1 вместо переменной v в терме e2 
subst :: Name -> Term -> Term -> Term
subst v t f@(Var s)
  | s == v = t
  | otherwise = f
subst v t (App e1 e2) = App (subst v t e1) (subst v t e2)
subst v t f@(Lam x e)
  | x == v = f
  | otherwise =
    if x `notElem` freeVars t
      then Lam x (subst v t e)
      else let f' = renames allNames f -- альфа конверсия всех связанных перменных в f
            in subst v t f'
 
-- | Наивный вычислитель (медленный из-за альфа-конверсий)
--   операционная семантика, вызов по имени, нормальная стратегия
eval :: Term -> Term
eval (Var s) = Var s
eval (App e1 e2) =
  case eval e1 of
    Lam x e -> eval (subst x e2 e)
    _ -> App e1 (eval e2)
eval (Lam x e) = Lam x (eval e)
 
-- | Канонические имена для тестирования (используем то, что переменные
--   односимвольные и именуем начиная с 'a')
evalCan = (renames allNames) . (renames allNames') . eval
Пробовать например так --- вычисление 2 в 3 степени
Haskell
1
evalCan (parseTerm "((\\a.(\\b.(a(a(ab)))))(\\c.(\\d.(c(cd)))))")
(пробелы в терме не допускаются).

Добавлено через 2 часа 47 минут
Попробую теперь реализовать используя weak HOAS с таким типом данных

Haskell
1
2
3
4
5
6
7
8
9
-- | Определяем типы
type Name = String
 
data Term
  = Var Name
  | App Term
        Term
  | Lam (Name -> Term)
  deriving (Eq, Ord, Show)
0
XRuZzz
Антикодер
1683 / 786 / 46
Регистрация: 15.09.2012
Сообщений: 2,898
29.05.2018, 13:23 8
По-моему код достоин загрузке на github, чтобы не постить каждое изменение в коде на форум достаточно будет сделать:
Bash
1
2
$ git commit
$ git push
0
29.05.2018, 13:23
Answers
Эксперт
37091 / 29110 / 5898
Регистрация: 17.06.2006
Сообщений: 43,301
29.05.2018, 13:23

Лямбда исчисление - формализация понятия алгоритм
Подскажите, пожалуйста, является ли лямбда исчисление одной из формализаций понятия алгоритм?

Применить лямбда-исчисление и выполнить подстановку
Доброго времени суток, не могли бы вы показать как решать такие вещи? я вроде бы что-то написал, но...

Лямбда-выражения. Как описать лямбда-процедуру и передать в нее файловую переменную?
Погуглив не смогла найти ответов на свои вопросы. Есть следующая процедура, которая находит...


Искать еще темы с ответами

Или воспользуйтесь поиском по форуму:
8
Ответ Создать тему
Опции темы

КиберФорум - форум программистов, компьютерный форум, программирование
Powered by vBulletin® Version 3.8.9
Copyright ©2000 - 2019, vBulletin Solutions, Inc.