Codedot (![[info]](http://l-stat.livejournal.com/img/userinfo.gif){kind=small} codedot) wrote,@ 2010-02-21 20:08:00 |
|
| Entry tags: | index |
Работа с лямбда-исчислением
Темы:
- Знакомство с лямбда-исчислением
- Комбинаторная логика с одноточечным базисом
- "The Heap Lambda Machine"
- Четыре правила
- Переписка с профессором Барендрегтом о "Micro Lambda Calculus"
- Стратегия Gyorgy Revesz
- "J. Klop's Ustica Notes" в открытом доступе
- Сильная редукция в комбинаторной логике
- Попытка реализации эта-редукции в стиле "Micro Lambda Calculus"
- Промежуточные итоги поиска
- Диалог о типизации
- "Явная" эта-редукция
- Диалог о целях и мотивации работы над лямбда-исчислением
- Оставшиеся без ответа вопросы о реализации эта-редукции
- Закрытие вопроса об одношаговой стратегии для "Micro Lambda Calculus"
- Трансляция записей в "Russian Lambda Planet"
- Незнакомец со странными обозначениями для лямбда-исчисления
- Эмуляция бестипового лямбда-исчисления им самим
- HP-полнота экстенсионального лямбда-исчисления
- "Рекурсивные вещественные числа"
- Теорема о неподвижной точке
- Тьюринг- и HP-полнота в реальном времени
- Краткое определение системы лямбда-бета-эта
- Проект языка MLC (Macro Lambda Calculus)
- "Хэш-коды" лямбда-выражений
Содержание:
- Знакомство с лямбда-исчислением
- Комбинаторная логика с одноточечным базисом
- "The Heap Lambda Machine"
- Четыре правила
- Изобретение четырех правил для редукции лямбда-выражений
- Безуспешный поиск источников и последующее оформление идеи в виде "Theoretical Pearls" для журнала "Journal of Functional Programming"
- Отправление вопроса об упоминании в литературе профессору Барендрегту и его ответ с указанием на "Micro Lambda Calculus"
- "Micro Lambda Calculus" - источник для четырех правил
- Дальнейшая переписка с Барендрегтом, вопрос о существовании одношаговой рекурсивной нормализующей стратегии для "Micro Lambda Calculus" и планы использования этой конструкции для обеспечения времени O(1) для шагов редукции в комбинации с ленивым связыванием подвыражений и, как следствие, "сборкой мусора"
- Стратегия Gyorgy Revesz для "Micro Lambda Calculus"
- Инициированная перепиской с профессором Барендрегтом публикация в интернете лекционных материалов "J. Klop's Ustica notes", поднимающих, в частности, тему "Micro Lambda Calculus"
- Сильная редукция в комбинаторной логике и неприемлемость ее использования для создания вычислительных систем
- Безуспешная попытка изобрести эта-мю-редукцию (эта-редукцию в стиле "Micro Lambda Calculus")
- Промежуточные итоги поиска и планы по эффективной реализации машины для сильной редукции
- Диалог о типизации
- "Явная" эта-редукция
- Диалог о целях и мотивации работы над лямбда-исчислением
- Так и оставшиеся без ответа вопросы о методах реализации эта-редукции в соответствующих сообществе ЖЖ и Usenet-группе
- Предложение одношаговой стратегии для "Micro Lambda Calculus"
- Предложение одношаговой стратегии для "Micro Lambda Calculus", похожей на стратегию Gyorgy Revesz
- Ответ J. Klop на предложение одношаговой стратегии, привлечение внимания Vincent van Oostrom
- Формализация предложенной стратегии и набросок статьи с доказательством ее нормализующего свойства, то есть закрытие прежде открытого вопроса в "Micro Lambda Calculus"
- Трансляция записей с тэгом "lambda calculus" проектом "Russian Lambda Planet"
- Незнакомец с просьбой помочь в решении задач по лямбда-исчислению, использующий странные непринятые обозначения
- Эмуляция бестипового лямбда-исчисления им самим
- HP-полнота экстенсионального лямбда-исчисления
- "Рекурсивные вещественные числа"
- Изобретение "The Representable Continuum Set", представления любых вещественных чисел лямбда-термами и, следовательно, ограничивающего множество вещественных чисел до счетного множества, ставя под вопрос само понятие континуума
- Поиск упоминаний в литературе данной конструкции и ссылки на так называемый "конструктивный вещественный анализ" и вводимое в его рамках понятие "рекурсивные вещественные числа"
- Теорема о неподвижной точке в лямбда-исчислении
- Тьюринг- и HP-полнота в реальном времени
- Краткое определение системы лямбда-бета-эта, то есть экстенсионального лямбда-исчисления
- MLC (Macro Lambda Calculus)
- Определение формальной грамматики языка для описания лямбда-выражений с макросами и без избыточных скобок
- Идея объединять множества свободных переменных с помощью подхода, похожего на один из методов интегрирования по контуру
- Реализация идеи на языке Си
- Рассмотрение ввода-вывода по схеме O = (i: P) I, позволяющей ограничиться самим лямбда-исчислением для написания произвольных программ P
- Заготовка интерпретатора с выводом без лишних скобок
- Смена синтаксиса и вывода: скобки разных видов, объединение переменных при каррировании, вычисление только последнего выражения (остальные - присваивания)
- "Хэш-коды" лямбда-выражений
