Библиография по «interaction combinators»
Jan. 16th, 2012 01:03 pmРешил подвести промежуточные итоги, сначала реконструировав свой небольшой поиск, который привел к «interaction combinators», а затем представив список статей по данной теме.
Постановка задачи была такой, что требовалось реализовать экстенсиональную версию оптимальной редукции для Тьюринг-полного чистого бестипового λ-исчисления на основе однородной памяти с работой в реальном времени и без потери памяти при NC = 2. Я начал решать эту задачу, познакомившись с монографией по оптимальной редукции. Так как оригинальный алгоритм Лэмпинга, как и основные его варианты, является «interaction system» с бесконечными (из-за наличия индексов) наборами типов агентов и правил взаимодействия, требование работы в реальном времени выполняться не могло. Поэтому я сосредоточился на единственном варианте оптимальной редукции с конечным набором операторов, который был представлен в монографии, — это нотация с помощью шин.
Далее, я заметил, что в некоторых случаях поведение разделяющей ноды может симулировать работу как брекетов и круассанов, так и самой ширины шины разделяющей ноды. Это подтолкнуло меня к попытке построить систему с поляризованным представлением λ-выражений и редукциями γ, β и η. Различные варианты этой системы оказались некорректными, однако, их изучение дало необходимые ключевые слова, чтобы продолжить поиск.
Одной из «interaction systems» с конечными наборами типов агентов и правил взаимодействия оказался самый эффективный, по крайней мере, на 2004 год, вариант KCLE [1]. Тем не менее, огромное количество типов и правил данной системы затрудняло ее реализацию в однородной памяти. Заметив в [2, 3, 4] использование, среди прочих, агентов γ и δ с правилами взаимодействия γ[δ(a, b), δ(c, d)] >< δ[γ(a, c), γ(b, d)], δ[x, y] >< δ[x, y] и γ[x, y] >< γ[y, x], я стал копать в сторону их происхождения. Оказалось, что как нотация для правил выше, так и сама система {γ, δ} принадлежат Yves Lafont. Называемая «interaction combinators», она была введена и подробно рассмотрена в одноименной статье [5]. В частности, доказывается, что система {γ, δ} полна по Тьюрингу.
Таким образом, оставалось лишь изучить способы представления λ-выражений с помощью исключительно «interaction combinators» [6], а также дополнительных правил преобразования за формальными пределами «interaction nets», которые бы заменяли η-редукцию в λ-исчислении [7]. То есть на данный момент вопрос остается лишь в выборе представления «interaction combinators» с дополнительными η-правилами в однородной памяти. После этого можно продолжить работу над проектом MLC (Macro Lambda Calculus), основной целью которого является отделение операций над данными от «control flow» постановкой барьера ввода-вывода по старой схеме Haskell через прерывания по обращению к памяти.
1. Ian Mackie. Efficient λ-Evaluation with Interaction Nets (2004).
2. Ian Mackie. Static analysis of interaction nets for distributed implementations (1997).
3. François-Régis Sinot. Token-Passing Nets: Call-by-Need for Free (2005).
4. Sylvain Lippi. Encoding left reduction in the λ-calculus with interaction nets (2002).
5. Yves Lafont. Interaction Combinators (1997).
6. Ian Mackie, Jorge Sousa Pinto. Compiling the λ-calculus into Interaction Combinators (1998).
7. Maribel Fernandez, Ian Mackie. A Theory of Operational Equivalence for Interaction Nets (2000).
Постановка задачи была такой, что требовалось реализовать экстенсиональную версию оптимальной редукции для Тьюринг-полного чистого бестипового λ-исчисления на основе однородной памяти с работой в реальном времени и без потери памяти при NC = 2. Я начал решать эту задачу, познакомившись с монографией по оптимальной редукции. Так как оригинальный алгоритм Лэмпинга, как и основные его варианты, является «interaction system» с бесконечными (из-за наличия индексов) наборами типов агентов и правил взаимодействия, требование работы в реальном времени выполняться не могло. Поэтому я сосредоточился на единственном варианте оптимальной редукции с конечным набором операторов, который был представлен в монографии, — это нотация с помощью шин.
Далее, я заметил, что в некоторых случаях поведение разделяющей ноды может симулировать работу как брекетов и круассанов, так и самой ширины шины разделяющей ноды. Это подтолкнуло меня к попытке построить систему с поляризованным представлением λ-выражений и редукциями γ, β и η. Различные варианты этой системы оказались некорректными, однако, их изучение дало необходимые ключевые слова, чтобы продолжить поиск.
Одной из «interaction systems» с конечными наборами типов агентов и правил взаимодействия оказался самый эффективный, по крайней мере, на 2004 год, вариант KCLE [1]. Тем не менее, огромное количество типов и правил данной системы затрудняло ее реализацию в однородной памяти. Заметив в [2, 3, 4] использование, среди прочих, агентов γ и δ с правилами взаимодействия γ[δ(a, b), δ(c, d)] >< δ[γ(a, c), γ(b, d)], δ[x, y] >< δ[x, y] и γ[x, y] >< γ[y, x], я стал копать в сторону их происхождения. Оказалось, что как нотация для правил выше, так и сама система {γ, δ} принадлежат Yves Lafont. Называемая «interaction combinators», она была введена и подробно рассмотрена в одноименной статье [5]. В частности, доказывается, что система {γ, δ} полна по Тьюрингу.
Таким образом, оставалось лишь изучить способы представления λ-выражений с помощью исключительно «interaction combinators» [6], а также дополнительных правил преобразования за формальными пределами «interaction nets», которые бы заменяли η-редукцию в λ-исчислении [7]. То есть на данный момент вопрос остается лишь в выборе представления «interaction combinators» с дополнительными η-правилами в однородной памяти. После этого можно продолжить работу над проектом MLC (Macro Lambda Calculus), основной целью которого является отделение операций над данными от «control flow» постановкой барьера ввода-вывода по старой схеме Haskell через прерывания по обращению к памяти.
1. Ian Mackie. Efficient λ-Evaluation with Interaction Nets (2004).
2. Ian Mackie. Static analysis of interaction nets for distributed implementations (1997).
3. François-Régis Sinot. Token-Passing Nets: Call-by-Need for Free (2005).
4. Sylvain Lippi. Encoding left reduction in the λ-calculus with interaction nets (2002).
5. Yves Lafont. Interaction Combinators (1997).
6. Ian Mackie, Jorge Sousa Pinto. Compiling the λ-calculus into Interaction Combinators (1998).
7. Maribel Fernandez, Ian Mackie. A Theory of Operational Equivalence for Interaction Nets (2000).
