Skip to content

Instantly share code, notes, and snippets.

@kana-sama

kana-sama/1.hs

Last active February 8, 2018 20:49
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save kana-sama/9ddd193f4f3e4ca05fec16cd65843200 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save kana-sama/9ddd193f4f3e4ca05fec16cd65843200 to your computer and use it in GitHub Desktop.
Download ZIP
Конспект по лямбда-исчислениям
Raw
1.hs
-- Истина
true === \t f -> t
-- Ложь
false === \t f -> f
-- Ветвления
-- Если первый аргумент - истина, то возвращает второй аргумент,
-- иначе третий аргумент
iif === \b x y -> b x y
-- Проверить: iif true x y === x
iif true x y == true x y
== (\t f -> t) x y [ t := x ]
== (\f -> x) y [ f := y ]
== x
-- Проверить: iif false x y === y
iif false x y == false x y
== (\t f -> f) x y [ t := x ]
== (\f -> f) y [ f := y ]
== y
-- Отрицание
-- если первый аргумент - истина, возвращает ложь
-- если первый аргумент - ложь, возвращает истину
not === \b -> b false true
-- Проверить: not true === false
not true == true false true
== (\t f -> t) false true [ t := false ]
== (\f -> false) true [ f := true ]
== false
-- Проверить: not false === true
not false == false false true
== (\t f -> f) false true [ t := false ]
== (\f -> f) true [ f := true ]
== true
-- Конъюнкция
-- Если два аргумент - истина, то возвращает истину,
-- иначе ложь
and === \x y -> x y false
-- Проверить: and true true === true
and true true == true true false
== (\t f -> t) true false [ t := true ]
== (\f -> true) false [ f := false ]
== true
-- Проверить: and true false === false
and true false == true false false
== (\t f -> t) false false [ t := false ]
== (\f -> false) false [ f := false ]
== false
-- Проверить: and false true === false
and false true == false true false
== (\t f -> f) true false [ t := true ]
== (\f -> f) false [ f := false ]
== false
-- Проверить: and false false === false
and false false == false false false
== (\t f -> f) false false [ t := false ]
== (\f -> f) false [ f := false ]
== false
-- Дизъюнкция
-- Если хотя бы один аргумент - истина, то возвращает истину,
-- иначе ложь
or === \x y -> x true y
-- Проверить: or true true === true
or true true == true true true
== (\t f -> t) true true [ t := true ]
== (\f -> true) true [ f := true ]
== true
-- Проверить: or true false === true
or true false == true true false
== (\t f -> t) true false [ t := true ]
== (\f -> true) false [ f := false ]
== true
-- Проверить: or false true === true
or false true == false true true
== (\t f -> f) false true [ t := false ]
== (\f -> f) true [ f := true ]
== true
-- Проверить: or false false === false
or false false == false true false
== (\t f -> f) true false [ t := true ]
== (\f -> f) false [ f := false ]
== false
-- Комбинаторы
I === \x -> x
K === \x y -> x
S === \f g x -> (f x) (g x)
B === \f g x -> f (g x)
-- Доказать: S K K == I
S K K == \x -> (K x) (K x)
== \x -> (\y -> x) (\y -> x)
== \x -> x
== I
-- Доказать: S (K S) K == B
S (K S) K == S (\x -> S) K
== S (\x -> S) (\x y -> x)
== S (\x' -> S) (\x' y -> x')
== \x -> ((\x' -> S) x) ((\x' y -> x') x)
== \x -> ((\x' -> S) x) (\y -> x)
== \x -> S (\y -> x)
== \x -> (\f g x' -> (f x') (g x')) (\y -> x)
== \x -> (\g x' -> ((\y -> x) x') (g x'))
== \x -> (\g x' -> x (g x'))
== \x g x' -> x (g x')
== \f g x' -> f (g x')
== \f g x -> f (g x)
== B
-- Доказать: \x -> M N == S (\x -> M) (\x -> N)
S (\x -> M) (\x -> N) == \x' -> ((\x -> M) x') ((\x -> N) x')
== \x' -> M (\x -> N) x')
== \x' -> M N
== \x -> M N
-- Упростить: (x (\x -> ((x y) x)) y)
(x (\x -> ((x y) x)) y) == x (\x -> (x y x)) y
== x (\x' -> x' y x') y
-- Упростить: ((\p -> (\q -> ((q (p r)) s))) ((q (p r)) s))
((\p -> (\q -> ((q (p r)) s))) ((q (p r)) s)) == (\p -> (\q -> ((q (p r)) s))) ((q (p r)) s)
== (\p' -> (\q' -> ((q' (p' r)) s)) ((q (p r)) s)
== (\q' -> ((q' (((q (p r)) s) r)) s))
== \q' -> ((q' (((q (p r)) s) r)) s)
== \q' -> q' (q (p r) s r) s
-- Пара, кортеж
pair === \x y f -> f x y
-- Достать первый элемент
first === \p -> p true
-- Достать второй элемент
second === \p -> p false
-- Проверить: first (pair a b) === a
first (pair a b) == (pair a b) true
== (\x y f -> f x y) a b true
== (\f -> a b) true
== a
-- Проверить: second (pair a b) === b
second (pair a b) == (pair a b) false
== (\x y f -> f x y) a b false
== (\f -> a b) false
== b
-- Числа
n0 === \s z -> z
n1 === \s z -> s z
n2 === \s z -> s (s z)
n3 === \s z -> s (s (s z))
n4 === \s z -> s (s (s (s z)))
-- Проверка на нуль
-- Если первый аргумент - n0, то вернуть истину,
-- иначе ложь
iszero === \n -> n (\x -> false) true
-- Проверить: iszero n0 === true
iszero n0 == n0 (\x -> false) true
== (\s z -> z) (\x -> false) true
== (\z -> z) true
== true
-- Проверить: iszero n1 === false
iszero n1 == n1 (\x -> false) true
== (\s z -> s z) (\x -> false) true
== (\z -> (\x -> false) z) true
== (\x -> false) true
== false
-- Получение следующего числа (инкрементация)
succ === \n s z -> s (n s z)
-- Проверить: succ n0 === n1
succ n0 s z == s (n0 s z)
== s z
== n1 s z
-- Проверить: succ n2 === n3
succ n2 s z == s (n2 s z)
== s ((\s' z' -> s' (s' z')) s z)
== s (s (s z))
== n3 s z
-- Сложение
plus === \m n s z -> m s (n s z)
-- Проверить: plus n1 n2 === n3
plus n1 n2 s z == n1 s (n2 s z)
== n1 s ((\s' z' -> s' (s' z')) s z)
== n1 s (s (s z))
== (\s' z' -> s' z') s (s (s z))
== s (s (s z))
== n3 s z
-- Проверить: plus n0 n0 === n0
plus n0 n0 s z == n0 s (n0 s z)
== n0 s ((\s' z' -> z') s z)
== n0 s z
== (\s' z' -> z') s z
== z
== n0 s z
-- Умножение
mult === \m n -> m (plus n) n0
-- оно работает, проверил на хаскеле, писать проверки вручную теперь стало лень
-- Возведение в степень
pow === \m n s z -> n m s z -- MAGIC
-- Проверить: pow n3 n2 === n9
pow n3 n2 s z == n2 n3 s z
== (\s' z' -> s' (s' z')) n3 s z
== n3 (n3 s) z
== (\s' z' -> s' (s' (s' z'))) (n3 s) z
== n3 s (n3 s (n3 s z)) -- n3 s (n3 s z) это по сути plus n3 n3 == n6, но мы распишем
== n3 s ((\s' z' -> s' (s' (s' z'))) s (n3 s z))
== n3 s (s (s (s (n3 s z))))
== n3 s (n6 s z) -- а тут plus n3 n6 == n9, но мы снова распишем
== (\s' z' -> s' (s' (s' z'))) s (n6 s z)
== s (s (s (n6 s z)))
== n9 s z
-- Проверял на больших числах, все аналогично. Возведение в 0 тоже работает.
Raw
проверки на хаскеле.hs
{-# LANGUAGE RankNTypes #-}
import Prelude hiding (succ)
-- тип для булевых значений
type Boolean = forall a. a -> a -> a
-- тип для нумералов Чёрча
type Number = forall a. (a -> a) -> a -> a
-- Истина
true :: Boolean
true t f = t
-- Ложь
false :: Boolean
false t f = f
-- Получение следующего нумерала
succ :: Number -> Number
succ n s z = s (n s z)
-- числа от 0 до 5
n0 :: Number
n1 :: Number
n2 :: Number
n3 :: Number
n4 :: Number
n5 :: Number
n0 _ z = z
n1 = succ n0
n2 = succ n1
n3 = succ n2
n4 = succ n3
n5 = succ n4
-- проверка на 0
isZero :: Number -> Boolean
isZero n = n (const false) true
-- сложение чисел
plus :: Number -> Number -> Number
plus m n s z = m s (n s z)
-- умножение
mult :: Number -> Number -> Number
mult m n s = m (n s)
-- возведение в степень
pow :: Number -> Number -> Number
pow m n s z = n m s z
-- преобразование в обычный Int для вывода
perform :: Number -> Int
perform n = n (+ 1) 0
main = do
print $ perform $ n5 -- 5
print $ perform $ plus n5 n2 -- 7
print $ perform $ succ n5 -- 6
print $ perform $ mult n5 n3 -- 15
print $ perform $ pow n5 n3 -- 125
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment