Комбинаторная логика: формализм без переменных. Основана на комбинаторах, заменяющих кванторы. Модель вычислений и база функциональных языков программирования.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Логический формализм, использующий комбинаторы вместо переменных.
Logical formalism using combinators instead of variables
Комбинаторная логика — это нотация, позволяющая избежать необходимости использования квантифицированных переменных в математической логике. Она была предложена Моисеем Шенфинкелем и Хаскеллом Карри и в последнее время находит применение в информатике как теоретическая модель вычислений, а также в качестве основы для разработки функциональных языков программирования. Она базируется на комбинаторах, которые Шенфинкель ввёл в 1920 году с целью предложить аналогичный способ построения функций и исключить упоминание переменных, особенно в логике предикатов. Комбинатор — это функция высшего порядка, которая для получения результата из своих аргументов использует только применение функций и ранее определённые комбинаторы.
Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming languages. It is based on combinators, which were introduced by Schönfinkel in 1920 with the idea of providing an analogous way to build up functions—and to remove any mention of variables—particularly in predicate logic. A combinator is a higher order function that uses only function application and earlier defined combinators to define a result from its arguments.
В математике
Комбинаторная логика изначально задумывалась как "предварительная логика", призванная прояснить роль квантифицированных переменных в логике, по сути, путем их исключения. Другой способ исключения квантифицированных переменных – логика предикативных функторов Куйна. Хотя выразительная сила комбинаторной логики обычно превосходит выразительную силу логики первого порядка, выразительная сила логики предикативных функторов идентична выразительной силе логики первого порядка (Куин, 1960, 1966, 1976). Первооткрыватель комбинаторной логики, Моисей Шёнфинкель, после своей оригинальной статьи 1924 года больше ничего не публиковал по комбинаторной логике. Хаскелл Карри заново открыл комбинаторы, работая преподавателем в Принстонском университете в конце 1927 года. В конце 1930-х годов Алонзо Чёрч и его студенты в Принстоне разработали конкурирующий формализм для функциональной абстракции – лямбда-исчисление, которое оказалось более популярным, чем комбинаторная логика. В итоге, из-за этих исторических обстоятельств, до тех пор, пока теоретическая информатика не проявила интерес к комбинаторной логике в 1960-х и 1970-х годах, почти все работы в этой области выполнялись Хаскеллом Карри и его учениками или Робертом Фейсом в Бельгии. Обзор ранней истории комбинаторной логики представлен в работах Карри и Фейса (1958) и Карри с соавторами (1972). Более современное изложение комбинаторной логики и лямбда-исчисления можно найти в книге Барендрегта, в которой рассматриваются модели, разработанные Даной Скоттом для комбинаторной логики в 1960-х и 1970-х годах.
Combinatory logic was originally intended as a 'pre logic' that would clarify the role of quantified variables in logic, essentially by eliminating them. Another way of eliminating quantified variables is Quine's predicate functor logic. While the expressive power of combinatory logic typically exceeds that of first order logic, the expressive power of predicate functor logic is identical to that of first order logic (Quine 1960, 1966, 1976). The original inventor of combinatory logic, Moses Schönfinkel, published nothing on combinatory logic after his original 1924 paper. Haskell Curry rediscovered the combinators while working as an instructor at Princeton University in late 1927. In the late 1930s, Alonzo Church and his students at Princeton invented a rival formalism for functional abstraction, the lambda calculus, which proved more popular than combinatory logic. The upshot of these historical contingencies was that until theoretical computer science began taking an interest in combinatory logic in the 1960s and 1970s, nearly all work on the subject was by Haskell Curry and his students, or by Robert Feys in Belgium. Curry and Feys (1958), and Curry et al. (1972) survey the early history of combinatory logic. For a more modern treatment of combinatory logic and the lambda calculus together, see the book by Barendregt, which reviews the models Dana Scott devised for combinatory logic in the 1960s and 1970s.
В вычислительной технике
В информатике комбинаторная логика используется как упрощенная модель вычислений, применяемая в теории вычислимости и теории доказательств. Несмотря на свою простоту, комбинаторная логика отражает многие существенные черты вычислений. Комбинаторную логику можно рассматривать как вариант лямбда-исчисления, в котором лямбда-выражения (представляющие функциональную абстракцию) заменяются ограниченным набором комбинаторов – примитивными функциями без свободных переменных. Лямбда-выражения легко преобразуются в комбинаторные выражения, а редукция комбинаторов значительно проще, чем редукция лямбда-выражений. Поэтому комбинаторная логика использовалась для моделирования некоторых нестрогих функциональных языков программирования и аппаратного обеспечения. Наиболее чистым воплощением этого подхода является язык программирования Unlambda, единственными примитивами которого являются комбинаторы S и K, дополненные операциями ввода/вывода символов. Хотя Unlambda не является практичным языком программирования, он представляет определенный теоретический интерес. Комбинаторная логика допускает различные интерпретации. Многие ранние работы Карри показали, как переводить аксиоматические системы обычной логики в уравнения комбинаторной логики. Дана Скотт в 1960-х и 1970-х годах продемонстрировала, как объединить теорию моделей и комбинаторную логику.
In computer science, combinatory logic is used as a simplified model of computation, used in computability theory and proof theory. Despite its simplicity, combinatory logic captures many essential features of computation. Combinatory logic can be viewed as a variant of the lambda calculus, in which lambda expressions (representing functional abstraction) are replaced by a limited set of combinators, primitive functions without free variables. It is easy to transform lambda expressions into combinator expressions, and combinator reduction is much simpler than lambda reduction. Hence combinatory logic has been used to model some non strict functional programming languages and hardware. The purest form of this view is the programming language Unlambda, whose sole primitives are the S and K combinators augmented with character input/output. Although not a practical programming language, Unlambda is of some theoretical interest. Combinatory logic can be given a variety of interpretations. Many early papers by Curry showed how to translate axiom sets for conventional logic into combinatory logic equations. Dana Scott in the 1960s and 1970s showed how to marry model theory and combinatory logic.
Комбинатные вычисления
Поскольку абстракция — единственный способ определения функций в лямбда-исчислении, что-то должно заменить её в комбинаторном исчислении. Вместо абстракции комбинаторное исчисление предоставляет ограниченный набор примитивных функций, из которых можно строить другие функции.
Since abstraction is the only way to manufacture functions in the lambda calculus, something must replace it in the combinatory calculus. Instead of abstraction, combinatory calculus provides a limited set of primitive functions out of which other functions may be built.
Расчет CLK против CLI
Следует различать CLK, как описано в этой статье, и исчисление CLI. Это различие соответствует различию между λK и λI исчислениями. В отличие от λK исчисления, λI исчисление ограничивает абстракции выражением вида λx. E, где x имеет хотя бы одно свободное вхождение в E. Как следствие, комбинатор K отсутствует в λI исчислении и в исчислении CLI. Константами CLI являются I, B, C и S, которые образуют базис, из которого можно составить все термы CLI (с точностью до равенства). Любой терм λI может быть преобразован в эквивалентный комбинатор CLI по правилам, аналогичным представленным выше для преобразования термов λK в комбинаторы CLK. См. главу 9 в Barendregt (1984).
A distinction must be made between the CLK as described in this article and the CLI calculus. The distinction corresponds to that between the λK and the λI calculus. Unlike the λK calculus, the λI calculus restricts abstractions to:
λx. E where x has at least one free occurrence in E.
As a consequence, combinator K is not present in the λI calculus nor in the CLI calculus. The constants of CLI are: I, B, C and S, which form a basis from which all CLI terms can be composed (modulo equality). Every λI term can be converted into an equal CLI combinator according to rules similar to those presented above for the conversion of λK terms into CLK combinators. See chapter 9 in Barendregt (1984).
Неразрешимость комбинаторного исчисления
Нормальная форма — это любой комбинаторный термин, в котором примитивные комбинаторы, если они присутствуют, не применены к достаточному числу аргументов для возможности упрощения. Неразрешимо, имеет ли общий комбинаторный термин нормальную форму, эквивалентны ли два комбинаторных термина и так далее. Это можно доказать аналогично соответствующим задачам для лямбда-термов.
A normal form is any combinatory term in which the primitive combinators that occur, if any, are not applied to enough arguments to be simplified. It is undecidable whether a general combinatory term has a normal form; whether two combinatory terms are equivalent, etc. This can be shown in a similar way as for the corresponding problems for lambda terms.
Сборник функциональных языков
Дэвид Тернер использовал свои комбинаторы для реализации языка программирования SASL. Кеннет Иверсон использовал примитивы, основанные на комбинаторах Карри, в своем языке программирования J, являющемся преемником APL. Это позволило ему реализовать то, что Иверсон назвал неявным программированием, то есть программирование с помощью функциональных выражений, не содержащих переменных, а также мощные инструменты для работы с такими программами. Оказывается, неявное программирование возможно в любом языке, подобном APL, с пользовательскими операторами.
David Turner used his combinators to implement the SASL programming language. Kenneth E. Iverson used primitives based on Curry's combinators in his J programming language, a successor to APL. This enabled what Iverson called tacit programming, that is, programming in functional expressions containing no variables, along with powerful tools for working with such programs. It turns out that tacit programming is possible in any APL like language with user defined operators.