Представление натуральных чисел функциями высшего порядка
Church encoding
Церковное кодирование: представление чисел и операторов в лямбда-исчислении. Оптимальный способ кодирования данных и функций, основанный на трудах Алозо Чёрча.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Представление натуральных чисел как функций высшего порядка
Representation of the natural numbers as higher order functions
В математике кодирование Черча — это способ представления данных и операторов в лямбда-исчислении. Числа Черча — это представление натуральных чисел с использованием лямбда-нотации. Метод назван в честь Алонзо Черча, который впервые таким образом закодировал данные в лямбда-исчислении. Термины, которые обычно считаются примитивными в других системах обозначений (такие как целые числа, булевы значения, пары, списки и объединения с тегами), отображаются в функции высшего порядка при кодировании Черча. Тезис Черча — Тьюринга утверждает, что любой вычислимый оператор (и его операнды) может быть представлен с помощью кодирования Черча. В нетипизированном лямбда-исчислении единственным примитивным типом данных является функция.
In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded data in the lambda calculus this way. Terms that are usually considered primitive in other notations (such as integers, booleans, pairs, lists, and tagged unions) are mapped to higher order functions under Church encoding. The Church–Turing thesis asserts that any computable operator (and its operands) can be represented under Church encoding. In the untyped lambda calculus the only primitive data type is the function.
Рациональные и действительные числа
Рациональные и вычислимые действительные числа также могут быть закодированы в лямбда-исчислении. Рациональные числа могут быть закодированы как пара целых чисел с знаком. Вычислимые действительные числа могут быть закодированы посредством процесса стремления к пределу, который гарантирует, что отклонение от истинного значения может быть уменьшено до любой заданной величины. Приведенные ссылки описывают программное обеспечение, которое теоретически можно было бы перевести на лямбда-исчисление. После определения действительных чисел, комплексные числа естественным образом кодируются как пара действительных чисел. Описанные выше типы данных и функции демонстрируют, что любой тип данных или вычисление может быть закодировано в лямбда-исчислении. Это и есть тезис Черча — Тьюринга.
Rational and computable real numbers may also be encoded in lambda calculus. Rational numbers may be encoded as a pair of signed numbers. Computable real numbers may be encoded by a limiting process that guarantees that the difference from the real value differs by a number which may be made as small as we need. The references given describe software that could, in theory, be translated into lambda calculus. Once real numbers are defined, complex numbers are naturally encoded as a pair of real numbers. The data types and functions described above demonstrate that any data type or calculation may be encoded in lambda calculus. This is the Church–Turing thesis.
Представьте список с помощью правой складки
В качестве альтернативы кодированию с использованием пар Черча, список можно закодировать, отождествляя его с функцией правого свёртки. Например, список из трех элементов x, y и z можно закодировать функцией высшего порядка, которая при применении к комбинатору c и значению n возвращает c x (c y (c z n)). Это представление списка может быть типизировано в системе F.
As an alternative to the encoding using Church pairs, a list can be encoded by identifying it with its right fold function. For example, a list of three elements x, y and z can be encoded by a higher order function that when applied to a combinator c and a value n returns c x (c y (c z n)). This list representation can be given type in System F.