В большинстве учебных пособий по лямбда-исчислению приводится пример, в котором положительные целые и логические значения могут быть представлены функциями. Как насчет -1 и я?
14
В большинстве учебных пособий по лямбда-исчислению приводится пример, в котором положительные целые и логические значения могут быть представлены функциями. Как насчет -1 и я?
Сначала закодируйте натуральные числа и пары, как описано в jmad.
Представьте целое число в виде пары натуральных чисел ( a , b ), таких что k = a - b . Затем вы можете определить обычные операции над целыми числами как (используя запись Хаскелла для λ- калькуляции):
neg = \k -> (snd k, fst k)
add = \k m -> (fst k + fst m, snd k + snd m)
sub = \k m -> add k (neg m)
mul = \k m -> (fst k * fst m + snd k * snd m, fst k * snd m + snd k * fst m)
Случай комплексных чисел аналогичен в том смысле, что комплексное число кодируется как пара вещественных чисел. Но более сложный вопрос заключается в том, как кодировать реалы. Здесь вы должны сделать больше работы:
Кодирование реалов - это большая работа, и вы не хотите делать это в калькуляторе. Но посмотрите, например, подкаталог Marshall для простой реализации реалов в чистом Haskell. В принципе это можно перевести на чистый λ- расчет.etc/haskell
i:ℤ
,x:a
,f,u,s:a→a
,p:(a→a,a→a)
] Если вы закодировать ℤ , как(Sign,ℕ)
то, учитывая пар функций ,(s,f)
какp
этот терминλi.λp.λx.(fst i) (fst p) id ((snd i) (snd p) x)
будет производить либоf(…f(x)…)
илиs(f(…f(x)…))
(если результат отрицательный). Если вы закодируете ℤ как(ℕ,ℕ)
, вам нужна функция, которая имеет обратное значение - заданная пара(f,u)
иx
, функцияλi.λp.λx.(snd i)(snd p)((fst i)(fst p) x)
выдаст,u(…u(f(…f(x)…))…)
что оставитf
приложенноеi
время доx
. Оба работают в разных контекстах (результат может быть «перевернут» ||f
является обратимым).fold . ctor
для любого конструктора и этого типаfold
(r
). (Именно поэтому, для рекурсивных типов, данные будут «рекурсия на своем» Для не рекурсивных типов это больше похожи.case
/ Матч шаблона.)Лямбда-исчисление может кодировать большинство структур данных и основных типов. Например, вы можете закодировать пару существующих терминов в лямбда-исчислении, используя ту же кодировку Черча, которую вы обычно видите для кодирования неотрицательных целых чисел и логического значения:
fst = λ p . p ( λ x y . x ) snd = λ p . p ( λ x y . y )
Тогда пара имеет вид p = ( пара a b ), и если вы хотите получить обратно a и b, вы можете выполнить ( fst p ) и ( snd p ) .(a,b) p=(pair ab) a b (fst p) (snd p)
Это означает, что вы можете легко представлять положительные и отрицательные целые числа парой: знак слева и абсолютное значение справа. Знак должен быть логическим, который указывает, является ли число положительным. Право - это натуральное число с использованием церковного кодирования.
Чтобы определить сложение, вы должны сравнить два натуральных числа и использовать вычитание, когда знаки разные, так что это не λ-термин, но вы можете адаптировать его, если вы действительно хотите:
но тогда вычитание действительно легко определить:
источник