Моё небольшое CS-исследование
Aug. 8th, 2011 12:33 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
codedotИзучая программирование, на определенном этапе я натолкнулся на функциональное программирование и, в частности, язык LISP. В первую очередь я изучил так называемый Pure LISP, который позволяет оперировать списками, построенными из других списков и атомов. Все структуры данных в нем, включая сами выражения языка, по сути, представляют собой бинарные деревья с атомами в узлах. Такие структуры в нем называют S-выражениями.
Вскоре я заметил, что некоторые элементарные операции выражаются через другие, и я предположил, что должен существовать язык, в котором любые выражения строятся с помощью лишь одного атома X. Однако потребовалось время, чтобы понять, какие операции действительно необходимы и как построить хотя бы одну операцию, через которую выражаются любые другие.
Следующим важным шагом стало обнаружение чистого бестипового лямбда-исчисления, которое отвечало на вопрос о том, какие именно конструкции в Pure LISP необходимы: бесконечный набор атомов в качестве имен переменных и безымянная функция. Остальные функции можно определить с помощью аппликации.
Продвинувшись еще немного в лямбда-исчислении, а именно затронув раздел комбинаторной логики, я нашел ответ и на второй поставленный вопрос. Оказывается, существует бесконечное счетное множество комбинаторов X, которые составляют одноточечные базисы комбинаторной логики.
Тогда я задумался о реализации такого языка программирования, затребовав сильную редукцию и вообще HP-полноту: два эквивалентных (экстенсионально равных) выражения должны были редуцироваться к одному и тому же выражению, если редукция завершается. Следующим ключевым моментом стало обнаружение статьи, показывающей, что сильная редукция для комбинаторной логики невозможна, или, точнее, требует бесконечного набора аксиом.
Таким образом я вернулся к системе λβη, и посвятил остальное время изучению различных способов её реализации. Начав с исторически первых стековых абстрактных машин, вплоть до машин для редукции графов, я решил добавить к требованиям определенный вид состояний абстрактной машины редукции. А именно, я затребовал однородную память в качестве состояния, имея в виду отказ от каких-либо стеков и других типов данных, кроме указателей. Однако, формализовать это требование удалось не сразу. Теперь я у меня есть четкое определение такого состояния и свойств машины на его основе, которое также сопряжено с непростым вопросом об одновременном выполнении этих свойств.
С другой стороны, в конечном итоге, я понял, что именно такая непопулярная тема, как оптимальная редукция, снова поднимает проблему вычислений, закрытую отрицательно в монографии Барендрегта: не существует оптимальной стратегии вычисления для λβη. Оказывается, при определенном представлении лямбда-выражений графами оптимальная редукция становится возможной. И так как это немедленно оказывается самым эффективным способом вычислений в общем случае на очень больших выражениях, я, конечно, сосредоточил свои усилия на изучении данной темы. Коротко говоря, цель моей небольшой теоретической работы можно описать как реализацию оптимальной редукции на основе однородной памяти.
Наконец, стоит упомянуть, что на своем пути мне также встретились еще две интересные связанные темы: кодирование, или сериализация, лямбда-выражений и дистрибутивное лямбда-исчисление. Для сериализации я придумал использовать комбинаторную логику с одноточечным базисом, выражения в которой легко записать префиксными бинарными кодами, так как они по сути являются ориентированным бинарными деревьями без нагрузки в узлах. Такой подход может оказаться предпочтительным потому, что позволяет выдавать каждый следующий бит кода за конечное время независимо от сериализуемого лямбда-выражения.
Вторую же, в свою очередь, я обнаружил, почти случайно подобрав четыре правила редукции, которые заменяют обычную подстановку. Потребовалось немало усилий, чтобы найти упоминания этих правил в литературе, и в этом мне очень помогли профессор Барендрегт, профессор Клоп и теперь уже тоже профессор ван Оостром. Также совместными усилиями удалось закрыть прежде открытый вопрос о нормализующей стратегии для такой системы правил редукции: я предложил неформально описанную стратегию, а ван Оостром в очень сжатые сроки представил ее формализацию и доказательство нормализующего свойства. Кстати, настоящий текст является наброском того рассказа, который бы я мог представить на возможном семинаре, о котором упомянул Клоп в недавней личной переписке, в частности, по поводу оптимальных TRS, с которыми, возможно, связана дистрибутивная редукция.
Вскоре я заметил, что некоторые элементарные операции выражаются через другие, и я предположил, что должен существовать язык, в котором любые выражения строятся с помощью лишь одного атома X. Однако потребовалось время, чтобы понять, какие операции действительно необходимы и как построить хотя бы одну операцию, через которую выражаются любые другие.
Следующим важным шагом стало обнаружение чистого бестипового лямбда-исчисления, которое отвечало на вопрос о том, какие именно конструкции в Pure LISP необходимы: бесконечный набор атомов в качестве имен переменных и безымянная функция. Остальные функции можно определить с помощью аппликации.
Продвинувшись еще немного в лямбда-исчислении, а именно затронув раздел комбинаторной логики, я нашел ответ и на второй поставленный вопрос. Оказывается, существует бесконечное счетное множество комбинаторов X, которые составляют одноточечные базисы комбинаторной логики.
Тогда я задумался о реализации такого языка программирования, затребовав сильную редукцию и вообще HP-полноту: два эквивалентных (экстенсионально равных) выражения должны были редуцироваться к одному и тому же выражению, если редукция завершается. Следующим ключевым моментом стало обнаружение статьи, показывающей, что сильная редукция для комбинаторной логики невозможна, или, точнее, требует бесконечного набора аксиом.
Таким образом я вернулся к системе λβη, и посвятил остальное время изучению различных способов её реализации. Начав с исторически первых стековых абстрактных машин, вплоть до машин для редукции графов, я решил добавить к требованиям определенный вид состояний абстрактной машины редукции. А именно, я затребовал однородную память в качестве состояния, имея в виду отказ от каких-либо стеков и других типов данных, кроме указателей. Однако, формализовать это требование удалось не сразу. Теперь я у меня есть четкое определение такого состояния и свойств машины на его основе, которое также сопряжено с непростым вопросом об одновременном выполнении этих свойств.
С другой стороны, в конечном итоге, я понял, что именно такая непопулярная тема, как оптимальная редукция, снова поднимает проблему вычислений, закрытую отрицательно в монографии Барендрегта: не существует оптимальной стратегии вычисления для λβη. Оказывается, при определенном представлении лямбда-выражений графами оптимальная редукция становится возможной. И так как это немедленно оказывается самым эффективным способом вычислений в общем случае на очень больших выражениях, я, конечно, сосредоточил свои усилия на изучении данной темы. Коротко говоря, цель моей небольшой теоретической работы можно описать как реализацию оптимальной редукции на основе однородной памяти.
Наконец, стоит упомянуть, что на своем пути мне также встретились еще две интересные связанные темы: кодирование, или сериализация, лямбда-выражений и дистрибутивное лямбда-исчисление. Для сериализации я придумал использовать комбинаторную логику с одноточечным базисом, выражения в которой легко записать префиксными бинарными кодами, так как они по сути являются ориентированным бинарными деревьями без нагрузки в узлах. Такой подход может оказаться предпочтительным потому, что позволяет выдавать каждый следующий бит кода за конечное время независимо от сериализуемого лямбда-выражения.
Вторую же, в свою очередь, я обнаружил, почти случайно подобрав четыре правила редукции, которые заменяют обычную подстановку. Потребовалось немало усилий, чтобы найти упоминания этих правил в литературе, и в этом мне очень помогли профессор Барендрегт, профессор Клоп и теперь уже тоже профессор ван Оостром. Также совместными усилиями удалось закрыть прежде открытый вопрос о нормализующей стратегии для такой системы правил редукции: я предложил неформально описанную стратегию, а ван Оостром в очень сжатые сроки представил ее формализацию и доказательство нормализующего свойства. Кстати, настоящий текст является наброском того рассказа, который бы я мог представить на возможном семинаре, о котором упомянул Клоп в недавней личной переписке, в частности, по поводу оптимальных TRS, с которыми, возможно, связана дистрибутивная редукция.
