codedot

Содержание по основным темам журнала:

• Личное
• Общекомпьютерная тематика
• Избранное
• Memories
• Проект Uniweb
• Работа с лямбда-исчислением

Analyzing possible modifications of interaction combinators' representation suitable for uniform memory led to the subject of so-called hard combinators. In particular, trying to compose a universal equivalent of {γ, δ} such as {φ, ψ, ξ} resulted in necessary rotation of ξ with respect to its principal port in some cases. The hard combinators discovered were introduced in a quite recent same-name paper by Bechet and Lippi, namely in 2008. Some idea of Bechet most probably related to the subject was actually mentioned in the paper by Lafont, although without any details and only referencing private communication instead.

Somewhat similar to hard combinators could be of use for uniform memory implementation of interaction systems from the view point of memory-preserving property. Specifically, the total amount of cells involved in a rule for a cut should remain the same before and after reduction. This way, implementation of duplication and annihilation as well as free cells buffer appear to be explicitly embedded into a formal interaction system.

There are also some slides demonstrating the hard combinators. They are available through the following address:

http://iml.univ-mrs.fr/ldp/Seminaire/documents0607/lippi.pdf

Using Lafont's notation, the resulted system can be described as a system of interaction nets with agents of types in {0, 1, –, +}, which has been proved to be Turing-complete with the following interaction rules:

0[0(x, y), x] >< –[–(y)], 1[1(x, y), x] >< –[+(y)];
0[x, 0(y, x)] >< +[–(y)], 1[x, 1(y, x)] >< +[+(y)].

The only remaining part of tree representation of minimal interaction systems are the interaction combinators γ and δ themselves. Let us define pseudo-unary agents φ, χ, and ψ. Then, the combinators γ and δ can be encoded as φ(ξ(x, y)) and ψ(ξ(x, y)), respectively. Also, we change the representation of passive connections to υ (free port) and ω (as for permutation) as follows:



Going through agonizing indecision of wondering which exactly model would be the best possible, one might consider a formal interaction system based on {φ, ψ, ξ} which would be equivalent by universality to that of {γ, δ}. (Garbage collection based on ε from the original system of interaction combinators by Lafont can be implemented separately.)

Using pseudo-agents of type τ which allows arbitrary amount of auxiliary ports and type ξ which allows arbitrary amount of connections on primary port, let us also introduce the definitions of ο, ρ, and ζ, then provide representation of an arbitrary interaction combinator net N into a form suitable for uniform memory whose nodes are equivalent to pseudo-agents' type ξ:



The interaction rules for this system are yet to be done. Since the above representation cannot have any cuts, any reduction rules will produce a graph rewriting system which is formally not an interaction system. The reduction rules will involve two trees τ, the root node ο, and the next redex ρ. Since ο includes a virtually infinite list of free ξ pseudo-agents, the reduction rules can be defined a way preserving the amount of ξ pseudo-agents involved.

The favorite track “Doo Uap, Doo Uap, Doo Uap” by Gabin from Hotel Costes by Stephane Pompougnac:

Осенью прошлого года я закончил первый этап обучения вождению и получил временные права на два года. Весной этого года надеюсь пройти второй этап и получить постоянные. Больше месяца назад для промежуточного этапа была куплена машина Dacia Sandero, которую я недавно упоминал. Ее двигатель называется Hi-Flex — это марка Renault для обозначения машин с двигателями «flex fuel», которые работают со смесью бензина с содержанием этанола до 85%.

Найдя список заправок St1, где есть этанол E85, я съездил на одну из них, где залил полбака. На данный момент заправок всего 14 на всю страну. Здесь это топливо выходит под маркой RE85 и производится из биоотходов в Финляндии. Эта смесь бензина с содержанием этанола до 85% стоит на треть дешевле бензина 95E10 (10% этанола), которым я все время заправлялся до этого, будучи на треть и менее энергоемкой. То есть расход примерно тот же самый в евро на км.

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

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

Продолжим преобразовывать «interaction nets» на основе «interaction combinators» с целью последующей реализации системы в однородной памяти. Для этого введем обозначение: тип ξ псевдоагентов, главный порт которых может быть связан одновременно с произвольным количеством дополнительных портов агентов γ и δ и псевдоагентов ξ. Псевдоагенты ξ напрямую соответствуют ячейкам однородной памяти. Один псевдоагент типа ξ в системе мы будем обозначать ν — он будет выступать в роли выделенной ячейки NULL однородной памяти. Графически позволим себе изображать эту выделенную ячейку произвольное количество раз. Деревья мы будем обозначать как псевдоагенты типа τ, имеющие произвольное количество дополнительных портов.

Заметим также, что любая «interaction net» с γ и δ может быть записана в виде набора бинарных деревьев с явными связями между корнями и листьями. При этом соединения между корнями мы будем называть активными, так как они представляют собой редексы, а между листьями — пассивными. Рассмотрим представления тех и других отдельно.

Начнем с активных соединений τ₁ >< τ₂. Они могут быть представлены как деревья ξ(τ₁, τ₂). Список редексов, построенный ранее, в свою очередь, запишем как ν(ξ(τ₁, τ₂), ξ(ξ(τ₃, τ₄), … )), оставив пока в стороне буфер свободных ячеек. (На самом деле, буфер свободных ячеек можно заменить искусственными аннигиляционными редексами.)

Теперь обратимся к пассивным соединениям. В отличие от редексов, где достаточно деревьев (хранятся лишь связи от главного порта к дополнительным, но не наоборот), там необходимы двусторонние равноправные ссылки. Но эта конструкция уже была построена для двусвязных ненаправленных списков, и применив ее к τ₁(x), τ₂(x), получим τ₁(ξ₁(ξ₁, ξ₂)), τ₂(ξ₂(ξ₂, ξ₁)). (Связываемыми объектами здесь выступают сами ξ₁ и ξ₂. Этой информации достаточно в общем случае, так как на месте пассивных связей не порождаются новые редексы, а лишь могут продолжаться деревья на месте листьев — этого легко добиться, заменив ξ на корневой агент соответствующего дерева.)

Наконец, свободные порты поставим в соответствие связям с главным портом ν. Активным это соединение будет вести себя как правило ε >< α(ε, ε) в оригинальной системе «Interaction Combinators» (Lafont), но без дублирования ν, учитывая множественные связи на его главном порту.

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

Для выполнения условия работы в реальном времени требуется не только конечные наборы типов агентов и правил для них, но также явные дублирование и аннигиляция агентов с помощью буфера свободных ячеек и время O(1) на выбор следующего редекса с помощью дополнительных связей. Этих свойств можно добиться преобразованием произвольной «interaction net» N на основе «interaction combinators», имеющую n редексов α_{2i - 1} >< α_2i, где i = 1, … , n, следующим образом:



Так как любая контракция может порождать не более четырех новых редексов, той части графа, которая ограничена пунктирными линиями, достаточно, чтобы обновить список редексов. Описанный подход позволяет построить Тьюринг-полную универсальную абстрактную машину для реализации любых «interaction nets», в том числе для оптимальной редукции.

[Прим. автора сплошных глубоких постов®: уже боевые домики набигают, чтобы можно было грабить корованы.]

Решил подвести промежуточные итоги, сначала реконструировав свой небольшой поиск, который привел к «interaction combinators», а затем представив список статей по данной теме.

Постановка задачи была такой, что требовалось реализовать экстенсиональную версию оптимальной редукции для Тьюринг-полного чистого бестипового λ-исчисления на основе однородной памяти с работой в реальном времени и без потери памяти при N_C = 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).