Представление отрицательных и комплексных чисел с использованием лямбда-исчисления

14

В большинстве учебных пособий по лямбда-исчислению приводится пример, в котором положительные целые и логические значения могут быть представлены функциями. Как насчет -1 и я?

zcaudate
источник

Ответы:

18

Сначала закодируйте натуральные числа и пары, как описано в jmad.

Представьте целое число в виде пары натуральных чисел ( a , b ), таких что k = a - b . Затем вы можете определить обычные операции над целыми числами как (используя запись Хаскелла для λ- калькуляции):К(a,б)Кзнак равноa-бλ

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)

Случай комплексных чисел аналогичен в том смысле, что комплексное число кодируется как пара вещественных чисел. Но более сложный вопрос заключается в том, как кодировать реалы. Здесь вы должны сделать больше работы:

  1. Кодируйте рациональное число в виде пары ( k , a ), где k - целое число, a - натуральное, а q = k / ( 1 + a ) .Q(К,a)КaQзнак равноК/(1+a)
  2. Кодировать действительное число с помощью функции f, такой что для каждого натурального k N , f k кодирует рациональное число q такое, что | х - д | < 2 - к . Другими словами, действительное кодируется как последовательность рациональных чисел, сходящихся к нему со скоростью k 2 - k .ИксеКNеКQ|Икс-Q|<2-КК2-К

Кодирование реалов - это большая работа, и вы не хотите делать это в калькуляторе. Но посмотрите, например, подкаталог Marshall для простой реализации реалов в чистом Haskell. В принципе это можно перевести на чистый λ- расчет.λetc/haskellλ

Андрей Бауэр
источник
1
Вау =) Мне интуитивно интересно, что это значит ... например, используя кодировку церковных чисел ... т.е. Церковное число целого числа n представлено функцией, которая применяет функцию к значению n раз. Имеют ли пары и отрицательные значения лямбда такое же интуитивное чувство к ним?
zcaudate
1
Кодировка Черча кодирует натуральные числа , 1 , 2 , ... Не кодирует отрицательные числа. В ответе выше я предположил, что вы уже знаете о кодировании натуральных чисел, поэтому я объяснил, как получить целые числа. Целые числа, как я их кодировал, представляют собой более формальную конструкцию, в отличие от церковных цифр, которые более сложно связаны с λ- калькуляцией. Я не думаю, что «отрицательные значения лямбда» - это осмысленная фраза. 012λ
Андрей Бауэр
@zcaudate [Тип аннотация: 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является обратимым).
никто не
@zcaudate Дополнительные функции необходимы, так как числа, закодированные Церковью, "рекурсивно", но пары передадут вам только свои компоненты. Вспомогательные функции просто склеивают компоненты в «правильном» порядке (что происходит автоматически для nats). См. Также: en.wikipedia.org/wiki/… - Кодировка Church в основном fold . ctorдля любого конструктора и этого типа fold( r). (Именно поэтому, для рекурсивных типов, данные будут «рекурсия на своем» Для не рекурсивных типов это больше похожи. case/ Матч шаблона.)
никто не
13

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

fst = λ p . p ( λ x y . x ) snd = λ p . p ( λ x y . y )

паразнак равноλИксYZ,ZИксY
FSTзнак равноλп,п(λИксY,Икс)
SNDзнак равноλп,п(λИксY,Y)

Тогда пара имеет вид p = ( пара  a b ), и если вы хотите получить обратно a и b, вы можете выполнить ( fst  p ) и ( snd  p ) .(a,b)p=(pair ab)ab(fst p)(snd p)

Это означает, что вы можете легко представлять положительные и отрицательные целые числа парой: знак слева и абсолютное значение справа. Знак должен быть логическим, который указывает, является ли число положительным. Право - это натуральное число с использованием церковного кодирования.

(sign,N)

исключающее

мультзнак равноλaб,пара  (исключающее(FST a)(FST б))  (мульт(snd a)(snd b))

Чтобы определить сложение, вы должны сравнить два натуральных числа и использовать вычитание, когда знаки разные, так что это не λ-термин, но вы можете адаптировать его, если вы действительно хотите:

add=λab.{(true,add(snd a)(snd b))if a0b0(false,add(snd a)(snd b))if a<0b<0(true,sub(snd a)(snd b))if a0b<0|a||b|(false,sub(snd b)(snd a))if a0b<0|a|<|b|(true,sub(snd b)(snd a))if a<0b0|a|<|b|(false,sub(snd a)(snd b))if a<0b0|a||b|

но тогда вычитание действительно легко определить:

minus=λa.pair(not(fst a))(snd a)
sub=λab.add(a)(minusb)

(a,b)a+bi

add[i]=λz1z2.pair(add(fst z1)(fst z2))(add(snd z1)(snd z2))
jmad
источник
6
k(a,b)k=ab
Сложные целые числа хорошо, но он просил комплексные числа. Опять же, они, конечно, никогда не могут быть представлены, так как существуют бесчисленные.
HDM
@AndrejBauer: очень хороший трюк (возможно, не такой простой) HdM: конечно, могут, даже не во всех. Но я подумал, что метод построения материала в λ-исчислении с церковным кодированием был более важным / уместным здесь.
Джмад
Хотел бы я дать два правильных ответа =) Я даже не думал, что можно представить реалы, когда я спрашиваю о комплексных числах, но вот, пожалуйста!
zcaudate