Anton Salikhmetov

Изучая программирование, на определенном этапе я натолкнулся на функциональное программирование и, в частности, язык LISP. В первую очередь я изучил так называемый Pure LISP, который позволяет оперировать списками, построенными из других списков и атомов. Все структуры данных в нем, включая сами выражения языка, по сути, представляют собой бинарные деревья с атомами в узлах. Такие структуры в нем называют S-выражениями.

Вскоре я заметил, что некоторые элементарные операции выражаются через другие, и я предположил, что должен существовать язык, в котором любые выражения строятся с помощью лишь одного атома X. Однако потребовалось время, чтобы понять, какие операции действительно необходимы и как построить хотя бы одну операцию, через которую выражаются любые другие.

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

Продвинувшись еще немного в лямбда-исчислении, а именно затронув раздел комбинаторной логики, я нашел ответ и на второй поставленный вопрос. Оказывается, существует бесконечное счетное множество комбинаторов X, которые составляют одноточечные базисы комбинаторной логики.

Тогда я задумался о реализации такого языка программирования, затребовав сильную редукцию и вообще HP-полноту: два эквивалентных (экстенсионально равных) выражения должны были редуцироваться к одному и тому же выражению, если редукция завершается. Следующим ключевым моментом стало обнаружение статьи, показывающей, что сильная редукция для комбинаторной логики невозможна, или, точнее, требует бесконечного набора аксиом.

Таким образом я вернулся к системе λβη, и посвятил остальное время изучению различных способов её реализации. Начав с исторически первых стековых абстрактных машин, вплоть до машин для редукции графов, я решил добавить к требованиям определенный вид состояний абстрактной машины редукции. А именно, я затребовал однородную память в качестве состояния, имея в виду отказ от каких-либо стеков и других типов данных, кроме указателей. Однако, формализовать это требование удалось не сразу. Теперь я у меня есть четкое определение такого состояния и свойств машины на его основе, которое также сопряжено с непростым вопросом об одновременном выполнении этих свойств.

С другой стороны, в конечном итоге, я понял, что именно такая непопулярная тема, как оптимальная редукция, снова поднимает проблему вычислений, закрытую отрицательно в монографии Барендрегта: не существует оптимальной стратегии вычисления для λβη. Оказывается, при определенном представлении лямбда-выражений графами оптимальная редукция становится возможной. И так как это немедленно оказывается самым эффективным способом вычислений в общем случае на очень больших выражениях, я, конечно, сосредоточил свои усилия на изучении данной темы. Коротко говоря, цель моей небольшой теоретической работы можно описать как реализацию оптимальной редукции на основе однородной памяти.

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

Вторую же, в свою очередь, я обнаружил, почти случайно подобрав четыре правила редукции, которые заменяют обычную подстановку. Потребовалось немало усилий, чтобы найти упоминания этих правил в литературе, и в этом мне очень помогли профессор Барендрегт, профессор Клоп и теперь уже тоже профессор ван Оостром. Также совместными усилиями удалось закрыть прежде открытый вопрос о нормализующей стратегии для такой системы правил редукции: я предложил неформально описанную стратегию, а ван Оостром в очень сжатые сроки представил ее формализацию и доказательство нормализующего свойства. Кстати, настоящий текст является наброском того рассказа, который бы я мог представить на возможном семинаре, о котором упомянул Клоп в недавней личной переписке, в частности, по поводу оптимальных TRS, с которыми, возможно, связана дистрибутивная редукция.

Оказывается, профессор Барендрегт — автор не только известной монографии и многих фундаментальных работ в лямбда-исчислении, но и следующих публикаций:

Buddhist Phenomenology, Part I.
Proceedings of the Conference on Topics and Perspectives of Contemporary Logic and Philosophy of Science,
Cesena, Italy, January 7-10, 1987, (Ed. M. dalla Chiara), Clueb, Bologna, 1988, 37-55.
[Experience with vipassana; the three fundamental characteristics of existence.]

Mysticism and beyond, Buddhist Phenomenology, Part II.
The Eastern Buddhist, New Series, vol XXIX, 1996, 262-287.
[The cover-up model of the mind, a contemporary view on the four nobel truths.]

Brain distribution and evidence for both central and neurohormonal actions of
cocaine- and amphetamine-regulated transcript peptide in Xenopus laevis.
E.W. Roubos, Lázár, G., Calle, M., Barendregt, H.P., Gaszner, B. and Kozicz, L.T.
Journal of Comparative Neurology. 507 (4), pp. 1622-1638.

Effect of starvation on Fos and neuropeptide immunoreactivities in the brain and pituitary gland of Xenopus laevis.
M. Calle and T. Kozicz and E. van der Linden and A. Desfeux and J.G. Veening and H.P. Barendregt and E.W. Roubos
General and Comparative Endocrinology. vol. 147. pp. 237-246.

Evidence that urocortin1 acts as a neurohormone to stimulate alpha-MSH releasein the toad Xenopus laevis.
M. Calle and G.J.H. Corstens and L.C. Wang and T. Kozicz and R.J. Denver and H.P. Barendregt and E.W. Roubos
Brain Res. vol. 1040. pp. 14-28.

Opioid peptides, CRF, and Urocortin in cerebrospinal fluid-contacting neurons in Xenopus leavis.
M. Calle and I.E.W.M. Claassen and J.G. Veening and T. Kozicz and E.W. Roubos and H.P. Barendregt
Trends in Comparative Endocrinology and Neurobiology. vol. 1040. pp. 249-252.

Reflection and its Use, from Meditation to Science.
Spiritual Information, 100 perspectives on science and religion. Edited by Ch.L. Harper Jr..
Philadelphia and London. Templeton Foundation Press. pp. 415-423.
Dutch version: Reflectie: van Wetenschap via Meditatie tot Lambda Calculus.
Wijsgerig Perspectief. vol. 44. 2004. pp. 39-54.

Вот такая трава.

Задавшись вопросом об этимологии значка «λ», выбранном Черчем для обозначения абстракции в λ-исчислении, я скоро натолкнулся на статью «History of Lambda-calculus and Combinatory Logic» (Felice Cardone, J. Roger Hindley), где, в частности, поднимается история этого обозначения. Оказывается, изначально для некоторого другого типа абстракции Whitehead и Russell использовали запись «x̂». Для новой конструкции, чтобы отличать ее от прежней абстракции, Черч заменил обозначение сначала на «∧x», а затем на «λx», очевидно, интерпретировав первый символ как заглавную букву «Λ», для упрощения набора:

«By the way, why did Church choose the notation “λ”? In [Church, 1964, §2] he stated clearly that it came from the notation “x̂” used for class-abstraction by Whitehead and Russell, by first modifying “x̂” to “∧x” to distinguish function-abstraction from class-abstraction, and then changing “∧” to “λ” for ease of printing. This origin was also reported in [Rosser, 1984, p.338]. On the other hand, in his later years Church told two enquirers that the choice was more accidental: a symbol was needed and “λ” just happened to be chosen».

До обнаружения приведенного отрывка в голове крутились лишь два варианта: первый заключался в указании альтернативности λ-исчисления логике («logics») первого порядка, а второй относился к связи абстракции с квантором общности (см., например, «Аппликативные вычислительные системы» Вольфенгагена, часть VI «Логика»).

Исходные объекты для построения теорий всегда выбраны из счетного множества: например, из имен; имена счетны ввиду счетности языка как множества текстов. Далее, при попытке ввести множество всех подмножеств такого или некоторого производного счетного множества возникает проблема континуума. Однако, конструктивно доказать, что континуальные множества вообще существуют, не представляется возможным.

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

Возникает логичный вопрос о том, как же быть с вещественными числами, и до какого множества следует их урезать, чтобы описать именно те, которые можно определить конструктивно. Такие числа есть в конструктивном вещественном анализе, и называются рекурсивными вещественными числами [вольный перевод с англ.].

В принципе, на каждом этапе, где требуются новые конструкции, в традиционной математике из-за неконструктивных определений обычно ведущие к несчетным множествам, можно каждый раз вводить надлежащую топологию и урезать отображения до непрерывных. Утверждается, что это возможно для любых мыслимых конструкций, что таким образом освобождает от интуитивно присутствующей опасности ограниченности конструктивного подхода.

Наконец, учитывая, что система λβη соответствует максимальным непротиворечивым теориям и при этом в виду тезиза Черча–Тьюринга имеет максимальную выразительность, любые мыслимые конструкции оказываются возможными для определения внутри нее. И это может, в свою очередь, служить дополнительным аргументом в сторону ее использования и большей концентрации внимания на эквивалентных системах и на теории вычислимости вообще.

Выношу из комментариев цитату о дельта-редукции (Х. Барендрегт, «Лямбда-исчисление. Его синтаксис и семантика», перевод с английского Г. Е. Минца под редакцией А. С. Кузичева, 1985, глава 15 «Другие понятия редукции», § 3 «Дельта-редукция»).

Хочу 1) интерпретируемый язык программирования 2) со следующим синтаксисом (пример кода) или, по крайней мере, похожий в нотации для выражений:

<text> ::= <term> | <assign> <text>;

<assign> ::= <ID> '=' <term> ';';

<term> ::= <appl> | <abstr>;

<abstr> ::= <ID> ':' <term> | <ID> ',' <abstr>;

<appl> ::= <atom> | <appl> <atom>;

<atom> ::= <ID> | '[' <term> ']' | '{' <term> '}' | '(' <term> ')';

3) бестиповый или со слабой типизацией, 4) возможно, с набором дельта-функций для быстрых операций на числах, строках и т.п., и, наконец, 5) с нормальным порядком вычисления.

Дайте.

Написано по просьбе babybitch_

В середине 1930-х годов Черчем и Тьюрингом было высказано фундаментальное утверждение. Неформально говоря, согласно этому утверждению, все строго описываемые функции являются рекурсивными. Это означает, что любая функция, которую можно точно вычислять или для которой можно изготовить устройство, которое будет ее вычислять, может быть всегда описана внутри любого языка, который обладает так называемой Тьюринг-полнотой. Таковыми являются многие языки программирования, а также бестиповое экстенсиональное лямбда-исчисление, которое, в принципе, тоже может рассматриваться как язык программирования.

С другой стороны, в 1930 году была доказана теорема Геделя о неполноте любой непротиворечивой теории, которая включает арифметику, то есть такая теория всегда содержит некоторое утверждение, которое нельзя доказать внутри нее. Иначе говоря, если теория полна, то она неизбежно противоречива, и в ней можно доказать любое утверждение, включая заведомо неверные. В связи с этим, уместен вопрос о максимальной непротиворечивой теории, которая бы позволяла записывать логические утверждения, содержащие общность, существования, переменные, функции и их свойства. Более формально, такия система называется логикой первого порядка, или, что то же самое, логикой предикатов.

Оказывается, максимальным непротиворечивым теориям соответствуют полные по Гильберту-Посту теории, утверждениями которых являются равенства. Такие теории называются эквациональными (от английского "равенство") и сами по себе свободны от логики, но с их помощью, тем не менее, можно описывать утверждения логики первого порядка. Полнота по Гильберту-Посту, в свою очередь, говорит о том, что любое верное утверждение доказуемо, а любое неверное утверждение делает систему противоречивой. Это свойство, естественно, слабее полноты теории в общем смысле, о котором идет речь в упомянутой теореме Геделя: ложность неверных утверждений в общем случае невозможно доказать.

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

Известно, что когда дети учатся говорить, они строят в своей голове заново учебник, описывая грамматику языка. Это означает, что люди генетически приспособлены к изучению грамматики. При преподавании математики в школе, однако, эта способность мало используется: часто имеют место неформальные определения и "объяснение на пальцах". В противоположность такому подходу, для некоторых детей, изучающих математику, возможно, было бы более естественно изучить сначала новый язык описания, и уже на этом языке увидеть определяемые математические конструкции. Ввиду простоты, на роль такого языка годится бестиповое экстенсиональное лямбда-исчисление.

Using yacc(1) and lex(1), specified by POSIX and available in Debian through packages `bison' and `flex', respectively, a parser was automatically generated for a simple language called Macro Lambda Calculus.

Теорема о неподвижной точке. Для любого F существует X, такой, что F X = X.

Доказательство. Пусть W ≣ λx.F (x x) и X ≣ W W. Тогда имеем X ≣ W W ≣ (λx.F (x x)) W = F (W W) = F X, что и требовалось доказать…

Теорема… о неподвижной точке - один из основных результатов лямбда-исчисления. Читатель, возможно, заметил одну особенность в доказательстве этой теоремы. Чтобы установить, что F X = X, мы начинаем с терма X и редуцируем его к F X, а не наоборот…

Определение. Комбинатор неподвижной точки - это терм M, такой, что для любого F имеет место M F = F (M F), то есть M F - неподвижная точка для F…

Пусть Y ≣ λf.(λx.f (x x)) (λx.f (x x)). Тогда Y — комбинатор неподвижной точки…

Задача. Построить F, такой, что F x y = F y x F.

Решение. F x y = F y x F следует из равенства F = λxy.F y x F, а оно вытекает из F = (λfxy.f y x f) F. Теперь положим F ≣ Y (λfxy.f y x f), и все в порядке.

Dedicated to dmvo:

\documentclass{article}
\title{The Representable Continuum Set}
\author{Anton Salikhmetov}

\begin{document}
\maketitle

\begin{abstract}
This paper introduces a new mathematical structure representing
all rational numbers’ sequences that can be defined to provide a
countable replacement for the usual continuum set of real
numbers, the question whether it is appropriate, say, for physics
being still open.
\end{abstract}

The Representable Continuum Set consists of all combinators that
are computable for all Church numerals and for each Church
numeral return a lambda expression of the list form
${\lambda x. x b [m] [n]}$, where $m$ and $n$ are natural
numbers, and $b$ is a boolean value representing sign, which
corresponds to a rational number ${\pm m / n}$.
If $S_i$ is the corresponding rational number for ${(M [i])}$,
an element $M$ from this set is considered as
${\lim_{n \rightarrow \infty} \sum_{i = 0}^n S_i}$.
\end{document}