Сел на выходных побаловаться с комбинаторной логикой, повыражать одни комбинаторы в базисе других. Быстро достался пользоваться бумажками и ручкой, написал такую штуку (наверняка велосипед):
module Cmb where
data Cmb = Cmb String-- комбинатор
| (:#) Cmb Cmb -- применение есть комбинатор (инфиксный конструктор)deriving Eq
instance Show Cmb where
show (Cmb x) = x
show (ts :# t) = case t of _ :# _ -> show ts ++ "(" ++ show t ++ ")"
_ -> show ts ++ show t
-- лень писать instance Read Cmb, поэтому делаю инфиксный конструктор применения левоассоциативным,
-- чтобы записывать (SK)K==SKK как s:#k:#k (без лишних скобок)infixl 5 :#
-- Основные комбинаторы
b = Cmb "B"-- композитор
w = Cmb "W"-- дубликатор
k = Cmb "K"-- канцелятор
i = Cmb "I"-- бездельник
s = Cmb "S"-- коннектор
c = Cmb "C"-- пермутатор
-- Неспецифицированные комбинаторы
x = Cmb "x"
y = Cmb "y"
z = Cmb "z"
t = Cmb "t"
u = Cmb "u"
v = Cmb "v"-- Пошагово выводит в строку применение комбинаторов, до тех пор пока что-то меняется
modN :: Cmb -> String
modN cmb = let res = mod1 cmb
in if res == cmb then (show cmb)
else ((show cmb) ++ " ~> " ++ modN res)
-- Применяет самый левый из годных к применению комбинаторов
mod1 :: Cmb -> Cmb
mod1 (Cmb c) = (Cmb c)
mod1 ((Cmb c) :# t)
| c == "I" = t -- применяем I
| otherwise = (Cmb c) :# mod1 t
mod1 ((Cmb c) :# t :# s)
| c == "W" = t :# s :# s -- применяем W
| c == "K" = t -- применяем K
| otherwise = mod1' ((Cmb c) :# t) s
mod1 ((Cmb c) :#t :# s :# u)
| c == "B" = t :# (s :# u) -- применяем B
| c == "S" = t :# u :# (s :# u) -- применяем S
| c == "C" = t :# u :# s -- применяем C
| otherwise = mod1' ((Cmb c) :# t :# s) u
mod1 (ts :#t :# s :# u) = mod1' (ts :#t :# s) u
-- Пробует организовать применение в первом, если не удаётся - пробует второй и склеивает результат в один
mod1' :: Cmb -> Cmb -> Cmb
mod1' c1 c2 = let res = mod1 c1
in if res == c1 then c1 :# mod1 c2
else res :# c2
-----------------------------------------------------------------------------
-- для тестирований
-- B в базисе SK
b_sk = s:#(k:#s):#k :#x:#y:#z
-- W в базисе SK
w_sk = s:#s:#(k:#(s:#k:#k)) :#x:#y:#z
-- C в базисе SK
c_sk = s:#((s:#(k:#s):#k):#(s:#(k:#s):#k):#s):#(k:#k) :#x:#y:#z
-- I в базисе SK
i_sk = s:#k:#k :#x
-- комбинатор неподвижной точки Y (Карри)
yCurry = s:#(b:#w:#b):#(b:#w:#b) :#x
-- комбинатор неподвижной точки Y (Тромпа)
yTromp = s:#s:#k:#(s:#(k:#(s:#s:#(s:#(s:#s:#k)))):#k) :#x
-- не имеет нормальной формы
noNF = s:#i:#i:#(s:#i:#i) :#x:#y
Здравствуйте, deniok, Вы писали:
D>И что-то не нравится мне, что в mod1 нужен такой перебор по арностям комбинаторв. Есть идеи, как это сделать поэлегантнее?
mod1 :: Cmb -> Cmb
mod1 (Cmb c) = (Cmb c)
mod1 ((Cmb "I") :# t) = t
mod1 ((Cmb c) :# t) = (Cmb c) :# mod1 t
mod1 ((Cmb "W") :# t :# s) = t :# s :# s
mod1 ((Cmb "K") :# t :# s) = t
...
или
data Cmb = Cmb String
| Cmb :# Cmb
| Apply String (Cmb -> Cmb)
cmbI = Apply "I" id
cmdK = Apply "K" (\c -> Apply "" (\_ -> c))
mod1 ((Apply _ ap) :# c) = ap c
Правда, вывод применения будет не такое очевидный, как у тебя. Можно сделать фильтр вывода, например по имени того, что apply-им, т.е. если имя "", то не выводить. Можно навернуть mod1 так, что если самый левый в цепочке :# будет Apply, то применять пока имя не будет непустым, как то так (пишу сходу, не проверяю)
L>mod1 :: Cmb -> Cmb
L>mod1 (Cmb c) = (Cmb c)
L>mod1 ((Cmb "I") :# t) = t
L>mod1 ((Cmb c) :# t) = (Cmb c) :# mod1 t
L>mod1 ((Cmb "W") :# t :# s) = t :# s :# s
L>mod1 ((Cmb "K") :# t :# s) = t
L>...
L>
Да, действительно, зачем там предохранители ...
L>или
L>
L>Правда, вывод применения будет не такое очевидный, как у тебя. Можно сделать фильтр вывода, например по имени того, что apply-им, т.е. если имя "", то не выводить.
Здравствуйте, chudo19, Вы писали:
C>Ребята! Скажите пожалуйста, а вы о чем ?
Ключевые слова — Комбинаторы, Лямбда счисление.
Хорошее введение в тему — книга Филдса и ко. "Функциональное программирование" есть в свободном доступе на lib.ru
C>На самом деле — нельзя ли немножко разъяснить для ламера о чем идет речь и где применимо?
Или это к вопросу о странных конструкциях наподобие
module Cmb where
data Cmb = Cmb String-- комбинатор
| (:#) Cmb Cmb -- применение есть комбинатор (инфиксный конструктор)deriving Eq
instance Show Cmb where
show (Cmb x) = x
show (ts :# t) = case t of _ :# _ -> show ts ++ "(" ++ show t ++ ")"
_ -> show ts ++ show t
?
Тогда искать по этому форуму и гуглу по ключевому слову Haskell.
Хорошее введение — Yet Another Haskell Tutorial.
Есть такая наука — комбинаторная логика. Её придумали Мозес Шонфинкель и Хаскелл Карри. Основная идея — нет переменных, есть только комбинаторы. Фундамент таков: если A и B — комбинаторы, то AB — тоже комбинатор (применение A к B).
Возьмём цепочку
ABCDEF
и будем трактовать каждый её элемент (символ) как комбинатор, то есть некоторое правило, по которому он действует на следующие элементы. Есть наборы основных комбинаторов (так называемые базисы), например базис из комбинаторов S и K, которые определены так
Sxyz = xz(yz)
Kxy = x
Здесь x, y и z — произвольные комбинаторы. Есть и другие комбинаторы, например
Bxyz=x(yz)
Доказано, что комбинаторная логика с некоторым базисом равномощна машине Тьюринга, т о есть всё, что в принципе вычислимо, может быть записано на её языке.
Собственно программа (на Хаскелле) занимается комбинаторной редукцией — последовательно применяет самый левый (из специфицированных) комбинатор в цепочке, получает следующую цепочку и т.д.
Например, вывод
Решил дописать instance Read Cmb и столкнулся с некоторой не совсем понятной сложностью.
Нам нужно разбирать строчки вроде
AB(CD)E
монтируя из них комбинаторы
a:#b:#(c:#d):#e
Наивная идея такова – читаем символ или группу в скобках (функция readsOne) и рекурсивно подклеиваем (с помощью :#, функция readsCmb') к прочтённому ранее до наступления терминирующего условия (аргумент termPred у функции readsCmb'). Терминирующим условием разбора всего выражения пусть пока служит пустая оставшаяся строка (соответствующий предикат – checkTerminate). Терминирующим условием разбора выражения в скобках служит символ “)” в начале оставшейся строки (соответствующий предикат – checkTerminate').
instance Read Cmb where
readsPrec _ = readsCmb
-- ЭТА НАИВНАЯ ВЕРСИЯ РАБОТАЕТ НЕВЕРНО!
readsCmb :: ReadS Cmb -- то есть String -> [(Cmb, String)]
readsCmb = readsCmb' checkTerminate
where-- читает и склеивает комбинаторы
-- до выполнения терминирующего предиката
readsCmb' :: (String -> Bool) -> String -> [(Cmb, String)]
readsCmb' termPred s = [(a :# b, s2) | (a, s1) <- readsOne s,
(b, s2) <- readsCmb' termPred s1]
++
[(a, s1) | (a, s1) <- readsOne s, termPred s1]
-- читает один комбинатор (возможно упакованный в скобки)
readsOne :: String -> [(Cmb, String)]
readsOne s = [(Cmb x, t) | (x, t) <- lexLitChar s, isAlpha $ head x]
++
[(a, s3) | ("(", s1) <- lex s,
(a , s2) <- readsCmb' checkTerminate' s1,
(")", s3) <- lex s2]
-- разбор основной строки терминируется концом ввода
checkTerminate :: String -> Bool
checkTerminate s = s == ""-- разбор строки в скобках терминируется закрывающей скобкой
checkTerminate' :: String -> Bool
checkTerminate' s = head s == ')'
К сожалению, это работает неверно. В результате разбора
ABCD
получится дерево
a:#(b:#(c:#d))
вместо нужного
((a:#b):#c):#d
Собственно, ничего удивительного; таков уж механизм рекурсии в readsCmb'.
Первая пришедшая в голову идея относительно исправления такого поведения – перевернуть входящую строчку, то есть вместо разбора
ABCD
разбирать
DCBA
и менять аргументы местами в процессе склейки для восстановления правильного порядка:
-- РАБОТАЮЩАЯ, НО ОГРАНИЧЕННАЯ ВЕРСИЯ
-- разбираем справа налево
-- для этого с самого начала делаем входящей строке reverse
readsCmb = (readsCmb' checkTerminate) . reverse
where-- читает и склеивает в обратном порядке комбинаторы: b:#a вместо a:#b
readsCmb' termPred s = [(b :# a, s2) | (a, s1) <- readsOne s,
(b, s2) <- readsCmb' termPred s1]
++
[(a, s1) | (a, s1) <- readsOne s, termPred s1]
-- читает один комбинатор (возможно упакованный в скобки)
readsOne s = [(Cmb x, t) | (x, t) <- lexLitChar s, isAlpha $ head x]
++
[(a, s3) | (")", s1) <- lex s, -- скобки наоборот!
(a , s2) <- readsCmb' checkTerminate' s1,
("(", s3) <- lex s2] -- скобки наоборот!
-- разбор основной строки терминируется концом ввода
checkTerminate s = s == ""-- разбор строки в скобках терминируется
-- открывающей скобкой (поскольку идет справа налево)
checkTerminate' s = head s == '('
Это уже работает правильно, но, к сожалению, не удовлетворяет всем требованиям reads. Полноценный reads должен терминироваться не только концом строки, но и любым посторонним символом, например, пробелом Cmb> readsCmb "AB(CD)E Hello"
[(AB(CD)E," Hello")]
выдавая разобранную часть и оставшуюся строку. При разборе в обратном порядке добиться такого поведения непросто (по крайней мере, мне никаких мыслей в голову не приходит).
Следующая, лучшая на настоящий момент идея – заставить readsCmb' монтировать не комбинатор, а список отдельно читаемых комбинаторов, а потом foldlить результат с помощью (:#), генерируя правильный комбинатор. Обзовём теперь readsCmb' именем reads2List:
readsCmb s = [(foldl1 (:#) cs, s1) | (cs, s1) <- reads2List checkTerminate s]
where-- читает комбинаторы в список до выполнения терминирующего предиката
reads2List :: (String -> Bool) -> String -> [([Cmb],String)]
reads2List termPred s = [(c:cs, s2) | (c, s1) <- readsOne s,
(cs, s2) <- reads2List termPred s1]
++
[([c], s1) | (c, s1) <- readsOne s, termPred s1]
-- читает один комбинатор (возможно упакованный в скобки)
readsOne :: String -> [(Cmb, String)]
readsOne s = [(Cmb x, t) | (x, t) <- lexLitChar s, isAlpha $ head x]
++
[(foldl1 (:#) cs, s3) | ("(", s1) <- lex s,
(cs , s2) <- reads2List checkTerminate' s1,
(")", s3) <- lex s2]
-- разбор основной строки терминируется концом ввода или небуквенным
-- символом (кроме открывающей скобки)
checkTerminate s = s == "" || not (isAlpha (head s) || head s == '(')
-- разбор строки в скобках терминируется закрывающей скобкой
checkTerminate' s = head s == ')'
Вопрос в том, нельзя ли обойтись без монтирования списка, то есть написать некую функцию magic, которая пересобирает дерево правильным образом. Скажем, в первой версии readsCmb' заменить a :# b на a `magic` b и она (первая версия) заработает верно.
Здравствуйте, deniok, Вы писали:
D>Вопрос в том, нельзя ли обойтись без монтирования списка, то есть написать некую функцию magic, которая пересобирает дерево правильным образом. Скажем, в первой версии readsCmb' заменить a :# b на a `magic` b и она (первая версия) заработает верно.
Тебе надо ассоциативность поменять?
Попробуй
x `magic` (l :# r) = (x `magic` l) :# r
x `magic` y = x :# y
Но, вообще то, я бы не стеснялся делать фолдинг, возможно, там даже списка реально существовать не будет.
Ну и Parsec подключил бы, на нём такие вещи выглядят более понятно и, следовательно, меньше подвержены ошибкам.
Здравствуйте, lomeo, Вы писали:
L>Но, вообще то, я бы не стеснялся делать фолдинг, возможно, там даже списка реально существовать не будет.
Я не стесняюсь. Я пытаюсь выдавить из программы "сложность", а она перекатывается с места на место, а понять её природу пока не удаётся.
L>Ну и Parsec подключил бы, на нём такие вещи выглядят более понятно и, следовательно, меньше подвержены ошибкам.
Parsec — это тяжёлая артиллерия. А задачка, вобщем-то, учебного характера.
Здравствуйте, deniok, Вы писали:
D>Я не стесняюсь. Я пытаюсь выдавить из программы "сложность", а она перекатывается с места на место, а понять её природу пока не удаётся.
В общем, я понял в чём проблема. Мне кажется нельзя написать комбинатор, который бы обработал правильно оба эти выражения:
A(BC) -> ABC
A(BC)D -> A(BC)D
Т.к. в первом случае ему нужно раскрыть скобки, а во втором оставить их как есть. Это зависит от наличия последнего комбинатора. При чём, первый вызов magic (A `magic` BC) должен вернуть обязательно ABC, но тогда после ABC `magic` D мы уже не знаем как был получен ABC — ABC->ABC или A(BC)->ABC, поэтому восстановить не сможем. Для этого нам потребуется не непосредственное исполнение magic, а создание структуры, по которой мы позже пройдёмся, собирая нужный комбинатор. Например, фолдингом
L>>Ну и Parsec подключил бы, на нём такие вещи выглядят более понятно и, следовательно, меньше подвержены ошибкам. D>Parsec — это тяжёлая артиллерия. А задачка, вобщем-то, учебного характера.
Ну, не знаю. Парсек всё же проще
pCombinator = pApply <|> pParens <|> pSingle
pSingle = liftM (\name -> Cmb [name]) letter -- эх, чуть не написал liftM (Cmb . return) letter, да понял, что закидают здесь :-(
pParens = between open close pCombinator
where
open = char '('
close = char ')'
pApply = (pParens <|> pSingle) `chainl1` (return (:#))
-- ну и инстанс вроде этогоinstance Read Cmb where
readsPrec _ input =
case (parse pCombinator "" input) of
Left errs -> error (show errs)
Right val -> [(val, "")]
Здравствуйте, lomeo, Вы писали:
L>В общем, я понял в чём проблема. Мне кажется нельзя написать комбинатор, который бы обработал правильно оба эти выражения:
L>A(BC) -> ABC L>A(BC)D -> A(BC)D
L>Т.к. в первом случае ему нужно раскрыть скобки, а во втором оставить их как есть. Это зависит от наличия последнего комбинатора. При чём, первый вызов magic (A `magic` BC) должен вернуть обязательно ABC, но тогда после ABC `magic` D мы уже не знаем как был получен ABC — ABC->ABC или A(BC)->ABC, поэтому восстановить не сможем. Для этого нам потребуется не непосредственное исполнение magic, а создание структуры, по которой мы позже пройдёмся, собирая нужный комбинатор. Например, фолдингом
Точно! Разбор здесь "нелокален": на результат может повлиять сколь угодно далёкий от текущего места кусок входной строки.
Да, действительно, зачем там предохранители ...
(Где-то я это видел)
