codedot: (Default)
2017-06-02 10:58 am

Useful Software

Command line

  • POSIX (XCU "Shell & Utilities"): vi(1), awk(1), make(1), bc(1), sed(1), grep(1), sort(1), uniq(1), tee(1), wc(1), etc.
  • GNU Screen (useful to echo exec screen -xR >>~/.profile on a remote host)
  • Git: git-grep(1), git-stash(1), git-bisect(1), etc.
  • Ledger (useful for optimizing both finances and time)
  • Taskwarrior (TODO manager, highly recommended)
  • drive (one of CLIs for Google Drive)
  • Jekyll (generates static websites from markdown)


Chrome OS

  • Google Keep (quite convenient for grocery lists)
  • Google Drive (directly accessible in Chrome OS' Files)
  • Secure Shell (the main SSH client for Chrome OS, supports SFTP in Files and SSH bookmarks, type ssh in the address field)
  • Wolfram Alpha (type = universe age in planck times in the address field)

Disclaimer: I'm celebrating five years as a Chromebook user.

codedot: (Default)
2017-05-30 10:53 am
Entry tags:

How to Profile Google Calendar

Here is one way to profile calendars:

  1. Export calendars in iCalendar format.
  2. Check out this Awk script:

    function parse(dt)
    	Y = substr(dt, 1, 4);
    	M = substr(dt, 5, 2);
    	D = substr(dt, 7, 2);
    	h = substr(dt, 10, 2);
    	m = substr(dt, 12, 2);
    	s = substr(dt, 14, 2);
    	return Y "/" M "/" D " " h ":" m ":" s;
    	dtstart = "";
    	dtend = "";
    	summary = "";
    /^DTSTART:/ {
    	sub(/\r$/, "");
    	sub(/^DTSTART:/, "");
    	dtstart = parse($0);
    /^DTEND:/ {
    	sub(/\r$/, "");
    	sub(/^DTEND:/, "");
    	dtend = parse($0);
    /^SUMMARY:/ {
    	sub(/\r$/, "");
    	sub(/^SUMMARY:/, "");
    	gsub(/  */, " ");
    	summary = $0;
    /^END:VEVENT/ {
    	if (dtstart && dtend && summary) {
    		print "i " dtstart " " prefix summary;
    		print "o " dtend;

  3. Have the Ledger utility installed:
    sudo apt install ledger # or whatever
  4. Convert the exported ICS files to timelog format:
    awk -f ics2tc.awk *.ics >
  5. Generate various reports from timelog, for example:
    ledger -f b -S -T
  6. Optionally specify a prefix:
    awk -f ics2tc.awk -v prefix=Work: Work.ics >
  7. Or even create a Makefile like this:

    all: $(TIMELOGS)
    	-rm -f $(TIMELOGS)
    .SUFFIXES: .ics .tc
    	awk -f ics2tc.awk -v prefix=$*: $< >$@

  8. ?????
  9. PROFIT!!1oneone
codedot: (Default)
2017-05-16 11:12 pm
Entry tags:

Codedot Logo in SVG

<svg xmlns=""
	viewBox="0,0 5,5"
<path d="M0,0 L5,0 L5,2 L4,2 L4,1 L1,1
	L1,4 L4,4 L4,3 L5,3 L5,5 L0,5 Z" />
<path d="M2,2 L2,3 L3,3 L3,2 Z">
<animateMotion begin="mouseover" restart="whenNotActive"
	keyPoints="0; .5; .5; 1"
	keyTimes="0; .36; .64; 1"
	keySplines=".5 0 .5 1; 0 0 1 1; .5 0 .5 1"
	path="M0,0 L2,0 Z" />
codedot: (Daria Morgendorffer)
2017-03-21 04:42 pm
Entry tags:

Универсальное решение

Я понял. Надо просто переместить:

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

А также:

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

Ну и так далее. Теоремой Геделя навеяло.

codedot: (Default)
2017-03-10 02:09 am

Лямбды на веревочках с рюшечками

Большие новости!

Я доделал needed reduction на веревочках, почистил лямбду от уродской waiting construct, сделал closed reduction дефолтным алгоритмом и обновил браузерную демку. Там теперь есть бесконечная прокрутка для дебага. Зацените рюшечки:

Приятно иметь калькулятор в браузере, который одновременно печатает полную βη-нормальную форму для любого бестипового λK-терма и при этом считает 10 2 2 1 в цифрах Черча за долю секунды на моем Хромбуке.

Напомню, что 21024 примерно в (1017)4 раз больше, чем гиперобъем пространства-времени всей наблюдаемой вселенной с момента большого взрыва в планковских единицах измерения, в наши дни имеющий порядок (1060)4 планковских единиц.

codedot: (Default)
2017-03-06 11:04 pm

How to Fix a Bug with Git

I am currently working on implementing needed reduction for interaction nets. To do that, I first needed to refactor a lot of somewhat ugly fast-written code in inet-lib. At some point, I changed retrieving an element from an array to .pop() from .shift(), just because in JavaScript the former happens to be a cheaper operation than the latter.

Many commits later, I decided to play with the program a little bit and compare performance between .shift()ing and .pop()ing. Boom! The program appeared to be broken. Even worse, invariance of the queue that is represented by that array with respect to the order in which it is processed is the whole point of interaction nets, namely the property of strong confluence also known as the one-step diamond property. I thought I fucked up hard.

First, I took a look at git-blame(1) for the line of code that calls .pop(), and found the corresponding commit. Then, I marked its parent commit as good with git-bisect(1). After a few steps, git-bisect(1) found the first bad commit.

Evidently, the problem had something to do with indirection applied by non-deterministic extension of interaction nets. And it did not take more than a couple of minutes to figure out a simple one-liner fix.

Overall, it took less than half an hour from finding a bug to fixing it which I first thought would take hours if not days. To me, it looks like yet another evidence that the idea of git-bisect(1) is totally genius. So, thanks again, Linus!

P. S. Free advice: when making commits, it is always useful to keep in mind 1) a possible need to git-grep(1) some lines of code later, and 2) almost inevitable need to deal with bugs which is a lot easier when commits are suitable for git-bisect(1).
codedot: (Default)
2017-02-21 06:25 am
Entry tags:

arXiv:1702.06092 [cs.LO]

Parallel needed reduction for pure interaction nets

Reducing interaction nets without any specific strategy benefits from constant time per step. On the other hand, a canonical reduction step for weak reduction to interface normal form is linear by depth of terms. In this paper, we refine the weak interaction calculus to reveal the actual cost of its reduction. As a result, we obtain a notion of needed reduction that can be implemented in constant time per step without allowing any free ports and without sacrificing parallelism.
codedot: (Default)
2017-01-30 02:21 am

Лямбды на веревочках в командной строке

$ npm install -g @alexo/lambda
└── @alexo/lambda@0.1.6 

$ lambda -e 'S hello bye world'
hello world (bye world)
$ lambda -de 'x: (x: x) v1 x'
\read_{[ ]}(\print) = \lambda(w1, \apply(\apply(\lambda(w2, w2), \atom_{v1}), w1));
\apply(\apply(\lambda(w2, w2), \atom_{v1}), \atom_{v2}) = \read_{v2: [ ]}(\print);
\apply(\lambda(w2, w2), \atom_{v1}) = \lambda(\atom_{v2}, \read_{v2: [ ]}(\print));
\lambda(w2, w2) = \lambda(\atom_{v1}, \lambda(\atom_{v2}, \read_{v2: [ ]}(\print)));
\lambda(\atom_{v2}, \read_{v2: [ ]}(\print)) = \atom_{v1};
\atom_{v2} = \read_{v1 [ ]}(\read_{v2: [ ]}(\print));
\read_{v2: [ ]}(\print) = \atom_{v1 v2};
\print = \atom_{v1};
$ npm explore -g @alexo/lambda -- sh
SAMPLE             NORMAL          CLOSED         OPTIMAL        ABSTRACT
counter             54(7)           58(6)          145(4)             N/A
w2eta             125(20)         137(16)          208(7)           38(7)
22210ii               N/A       1740(182)        7918(70)         732(70)
3222ii                N/A       5896(545)      164474(43)        1183(43)
1022ii                N/A     23026(2085)     2490504(59)        4299(59)
4222ii                N/A 1442259(131124)             N/A      262402(64)
222210ii              N/A 6685119(655415)             N/A    2359813(201)
cfact4         8605(1028)      18606(887)      96676(691)      13985(691)
yfact4        92395(4833)     53519(1741)     659727(760)      16611(760)
cfact5      170958(16917)   895848(16170)  5906411(13462)   287527(13462)
yfact5      783031(43651)  1371216(22267)             N/A   291418(13550)
codedot: (Default)
2016-09-30 05:59 pm
Entry tags:


Только что опубликовали IEEE 1003.1-2008+TC1+TC2.

В список участников TC2 мое имя попало в связи с багами 735-737 против TC1:

Теперь грамматика языка Shell не содержит shift/reduce-конфликтов (можно засунуть ее в yacc(1) и убедиться, раньше было пять конфликтов), лишена двух лишних правил, а также корректно описывает произвольное количество команд в скриптах.
codedot: (Default)
2016-09-11 09:38 am
Entry tags:

Token-passing Optimal Reduction with Embedded Read-back

Token-passing Optimal Reduction with Embedded Read-back
Anton Salikhmetov

We introduce a new interaction net implementation of optimal reduction for the pure untyped lambda calculus. Unlike others, our implementation allows to reach normal form regardless of the interaction net reduction strategy using the approach of so-called token-passing nets and a non-deterministic extension for interaction nets. Another new feature is the read-back mechanism implemented without leaving the formalism of interaction nets.

In Andrea Corradini and Hans Zantema: Proceedings 9th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2016), Eindhoven, The Netherlands, April 8, 2016, Electronic Proceedings in Theoretical Computer Science 225, pp. 45–54.
Published: 10th September 2016.
codedot: (Default)
2016-09-03 11:34 am
Entry tags:

Interactive Tonnetz

The Tonnetz is a lattice diagram representing tonal space. It can be used to visualize harmonic relationships in music. Each node in the diagram corresponds to one of the twelve tones and is connected to six adjacent tones that are related to it by a major third, a minor third, or by a perfect fifth, depending on their relative position in the diagram.

I forked on GitHub the source code of TonnetzViz created by Ondřej Cífka and implemented the following features:

  • zero configuration without any menus;
  • Tonnetz-like keyboard layout;
  • Shepard tones using Web Audio;
  • plug and play Web MIDI support;
  • blue minor and red major triads;
  • Tonnetz bent to represent halftones;
  • Shift key to sustain notes;
  • and arrow keys to transpose.

Now the live version is available at

codedot: (Default)
2016-05-25 03:00 pm
Entry tags:

Еще одно введение в веревочковедение

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

Сети взаимодействия (interaction nets) - это структуры, подобные графам, состоящие из агентов (agents) и дуг. Агент типа α

имеет арность ar(α) ≥ 0. Если ar(α) = n, то агент α имеет n дополнительных портов (auxiliary ports) x1,..., xn в дополнение к его главному порту (principle port) x0. Все типы агентов принадлежат множеству Σ, называемому сигнатурой (signature). К любому порту можно присоединить не более одной дуги. Порты, которые не соединены ни одной дугой, называются свободными (free ports). Совокупность всех свободных портов в сети называется ее интерфейсом. Разводка (wiring) ω

состоит исключительно из дуг. Индуктивно определяемые деревья (trees)

соответствуют термам t ::= α(t1,..., tn) | x в исчислении взаимодействия (interaction calculus), где x называется именем (name).

С помощью разводок и деревьев любая сеть может быть представлена следующим образом:

что в исчислении взаимодействия будет соответствовать конфигурации (configuration)
<t1,..., tm | v1 = w1,..., vn = wn>,
где ti, vi, wi - некоторые термы. Последовательность t1,..., tm называется интерфейсом (interface), остальное же представляет собой мультимножество уравнений (equations). Разводка ω транслируется в выбор имен, и каждое имя обязано иметь ровно два вхождения в конфигурации.

Как и в λ-исчислении, в исчислении взаимодействия естественным образом определяются понятия α-конверсии и подстановки (substitution). Оба вхождения любого имени могут быть заменены на новое имя, если оно не участвует в данной конфигурации. Если терм t имеет ровно одно вхождение имени x, то подстановка t[x := u] определяется как результат замены имени x в терме t некоторым термом u.

Когда два агента соединены своими главными портами, они формируют активную пару (active pair). Для активных пар можно ввести правила взаимодействия (interaction rules), которые описывают, как активная пара будет заменена во время редукции сети взаимодействия. Графически любое правило взаимодействия можно преставить следующим образом:

где α, β ∈ Σ, а сеть N представлена с помощью разводок и деревьев в виде, пригодном для исчисления взаимодействия: в нотации Lafont это соответствует
a[v1,..., vm] >< β[w1,..., wn].
Говорят, что сеть без активных пар находится в нормальной форме (normal form). Сигнатура и множество правил взаимодействия вместе задают систему взаимодействия (interaction system).

Теперь рассмотрим пример для введенных конструкций, в котором участвуют часто использующиеся агенты ε и δ. В нотации Lafont правила взаимодействия для удаляющего (erasing) агента ε

записываются как ε >< α[ε,..., ε], а правила для дублирующего (duplicating) агента δ

выглядят следующим образом:
δ[α(x1,..., xn), α(y1,..., yn)] >< α[δ(x1, y1),..., δ(xn, yn)].
В качестве примера сети, в которой участвуют правила удаления и дублирования, возьмем простую сеть которая не имеет нормальной формы и редуцируется к самой себе:

В исчислении взаимодействия такая сеть соответствует конфигурации
<∅ | δ(ε, x) = γ(x, ε)> без интерфейса.

Редукция для конфигураций определяется более подробно, чем для сетей. Если
a[v1,..., vm] >< β[w1,..., wn], то следующая редукция:
<... | α(t1,..., tm) = β(u1,..., un), Δ> → <... | t1 = v1,..., tm = vm, u1 = w1,..., un = wn, Δ>
называется взаимодействием (interaction). Когда одно из уравнений имеет форму x = u, к конфигурации применимо разыменование (indirection), в результате которого другое вхождение имени x в некотором терме t будет заменено на терм u:
<...t... | x = u, Δ> → <...t[x := u]... | Δ> или <... | x = u, t = w, Δ> → <... | t[x := u] = w, Δ>.
Уравнение t = x называется тупиком (deadlock), если x имеет вхождение в t. Обычно рассматривают только сети, свободные от тупиков (deadlock-free). Вместе взаимодействие и разыменование задают отношение редукции на конфигурациях. Тот факт, что некоторая конфигурация c редуцируется к своей нормальной форме c', где мультимножество уравнений пусто, обозначают через c ↓ c'.

Если вернуться к примеру незавершающейся редукции сети, то бесконечная редукционная цепочка, начинающаяся с соответствующей конфигурации выглядит следующим образом:
<∅ | δ(ε, x) = γ(x, ε)> →
<∅ | ε = γ(x1, x2), x = γ(y1, y2), x = δ(x1, y1), ε = δ(x2, y2)> →*
<∅ | x1 = ε, x2 = ε, x = γ(y1, y2), x = δ(x1, y1), x2 = ε, y2 = ε> →*
<∅ | δ(ε, x) = γ(x, ε)> → ...

На нашем языке программирования, который подобен yacc(1)/lex(1) по структуре и лексически близок к LaTeX-нотации для исчисления взаимодействия, тот же самый пример можно записать следующим образом:
\epsilon {
        console.log("epsilon >< delta");
} \delta[\epsilon, \epsilon];

\epsilon {
        console.log("epsilon >< gamma");
} \gamma[\epsilon, \epsilon];

\delta[\gamma(x, y), \gamma(v, w)] {
        console.log("delta >< gamma");
} \gamma[\delta(x, v), \delta(y, w)];


\delta(\epsilon, x) = \gamma(x, \epsilon);
Отметим, что наш язык программирования позволяет записывать побочные действия в императивном стиле, таким образом давая возможность исполнять произвольный код, включая ввод-вывод, а также условные множественные правила для пар вида αi >< βj в зависимости от значений i и j, которые могут быть произвольными данными, привязанными к агентам.

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

Сигнатура и арности агентов соответствующей системы взаимодействия автоматически выводятся при компиляции исходного кода программы на основе правил взаимодействия и начальной конфигурации. Правила взаимодействия вместе с их побочными действиями компилируются заранее, до начала редукции сети, при этом компилятор формирует таблицу для быстрого O(1)-поиска правил, соответствующих активным парам, во время последующего исполнения программы. После этого начальная конфигурация добавляется в FIFO-очередь уравнений, которая затем обрабатывается, пока она не станет пуста.

P. S. Недавно адаптировал этот текст и дополнил им статью на Википедии.
codedot: (Default)
2015-12-10 03:18 am
Entry tags:

arXiv:1512.02995 [cs.LO]

A token-passing net implementation of optimal reduction with embedded read-back

In this paper, we introduce a new interaction net implementation of optimal reduction for pure untyped lambda calculus. Unlike others, our implementation allows to reach normal form regardless of interaction net reduction strategy using the approach of so-called token-passing nets. Another new feature is the read-back mechanism also implemented without leaving the formalism of interaction nets.
codedot: (Default)
2015-11-15 02:30 pm

Анонс пакета Node.js для сетей взаимодействия

JavaScript-движок для сетей взаимодействия

Данный пакет Node.js позволяет редуцировать сети взаимодействия, описанные на языке, близком к исчислению взаимодействия, но без понятия интерфейса, или корня сети взаимодействия. Правила взаимодействия определяются с помощью нотации Yves Lafont. Реализация неявно расширяет системы взаимодействия специальным недетерминированным агентом amb, а также позволяет задавать побочные действия на языке JavaScript.

Ранее этот движок разрабатывался в контексте Macro Lambda Calculus (MLC), Web-реализации λ-исчисления с помощью сетей взаимодействия:

Теперь MLC использует пакет inet-lib в качестве языка низкого уровня, чтобы транслировать в него λ-термы, реализуя механизм readback также внутри формализма сетей взаимодействия.
codedot: (Default)
2015-10-20 11:06 am
Entry tags:

Token-Passing Net Implementation of Optimal Reduction

In the book "The Optimal Implementation of Functional Programming Languages" by Andrea Asperti and Stefano Guerrini the initial encoding of a λ-term M into an interaction net is a configuration <x | x = [M]0> where translation [M]n is inductively defined by the following rules:

The corresponding interaction rules consist of annihilation:

and propagation:

where i < j.

The problem is that, in case of an arbitrary λK-term, reduction of such an interaction net has to avoid interactions in parts of the net that are disconnected from the interface; otherwise, it may not reach the normal form.

It appears that in order to allow safe reduction without restricting evaluation strategy, it is sufficient to change initial encoding to <x | Eval(x) = [M]0> and β-reduction to @i[x, y] >< λi[Wait(z, Hold(z, x)), y], introducing additional agent types Eval, Wait, Hold, Call and Decide with the following interaction rules:

Eval[λi(x, y)] >< λi[x, Eval(y)];
Eval[δi(x, y)] >< δi[x, y];
Eval[x] >< Wait[Eval(x), Call];
Call >< Hold[x, Eval(x)];
δi[Wait(x, Amb(y, Decide(z, v), v)), Wait(w, y)] >< Wait[δi(x, w), z];
Call >< Decide[Call, ε];
ε >< Decide[x, x];
@i[x, Wait(y, Hold(@i(x, y), Wait(v, w)))] >< Wait[v, w];
α[Wait(x, y)] >< Wait[α(x), y],

where α is a bracket or a croissant, and Amb(x, y, z) is McCarthy's amb, x representing its second principle port.

This token-passing net version of optimal reduction is implemented on the optimal branch of the MLC repository.
codedot: (Default)
2015-09-11 05:56 pm
Entry tags:

Copy-on-Demand in Interaction Nets

Using McCarthy's amb agent:

you can represent copy-on-demand in interaction nets:

with the following interaction rules:
codedot: (Default)
2015-08-27 02:14 am

Лямбды на веревочках нынче в браузере

Добрались-таки лямбды на веревочках до ваших браузеров:

codedot: (Default)
2015-08-24 03:22 pm

Лямбды на веревочках почти в браузере

Хуяк-хуяк, и в продакшн:

$ make
        make parsers
        node_modules/.bin/jison mlc.jison
        node_modules/.bin/jison inet.jison
`parsers' is updated.
        make example
        node parse.js example.mlc >
        inc <
        mv example.c
        cc    -o example example.c 
        time -p ./example
v1: v2: v1 (v1 (v1 (v2)))
real 0.09
user 0.08
sys 0.00
        make example.p2p
        node parse.js example.mlc p2p >example.p2p
        time -p node interact.js example.p2p
v1: v2: v1 (v1 (v1 (v2)))
real 0.79
user 0.76
sys 0.02

Осталось немного причесать, и цель достигнута.