Flight Over Helsinki
Daria Morgendorffer
codedot


This entry was originally posted at http://codedot.dreamwidth.org/170977.html

Y (K M) = M
Daria Morgendorffer
codedot
Encoding ω Α (K ω), where ω ≡ λx.x x, A ≡ λx.λf.f (x x f), and K ≡ λx.λy.x:

$ cat init.txt 
term = \read_{strdup("")}(\print);

term = \apply(\apply(omega1, a), \apply(k, omega2));

omega1 = \lambda(x1, \apply(\amb(y1, \share(x1, z1), z1), y1));
omega2 = \lambda(x2, \apply(\amb(y2, \share(x2, z2), z2), y2));

a = \lambda(self, \lambda(func, \apply(func1, rec)));
rec = \apply(\apply(self1, self2), func2);
self1 = \amb(self2, \share(self, back1), back1);
func1 = \amb(func2, \share(func, back2), back2);

k = \lambda(x, \lambda(\erase, x));
$ make
        printf '%s\n\n$$\n\n%s\n\n$$\n\n%s\n' >test.in \
                "`cat rset.txt`" \
                "`cat init.txt`" \
                "`cat tail.txt`"
        inc <test.in
        mv in.tab.c test.c
        cc    -o test test.c 
        valgrind ./test
==20346== Memcheck, a memory error detector
==20346== Copyright (C) 2002-2010, and GNU GPL'd, by Julian Seward et al.
==20346== Command: ./test
==20346== 
v1: (v1 (v1))
==20346== 
==20346== HEAP SUMMARY:
==20346==     in use at exit: 0 bytes in 0 blocks
==20346==   total heap usage: 606 allocs, 606 frees, 23,934 bytes allocated
==20346== 
==20346== All heap blocks were freed -- no leaks are possible
==20346== 
==20346== For counts of detected and suppressed errors, rerun with: -v
==20346== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 4 from 4)
$ 


This entry was originally posted at http://codedot.dreamwidth.org/170715.html

Call-by-Need Evaluation Strategy
Daria Morgendorffer
codedot
https://gist.github.com/codedot/24f277ef4df5828c70a8

Call-by-need evaluation strategy using non-deterministic extension in Interaction Nets Compiler:

@@ -14,10 +14,18 @@
 \print {
 	/* Output results of read-back. */
 	puts(RVAL);
-	exit(EXIT_SUCCESS);
+	free(RVAL);
 } \atom;
 
 \read[a] {
+	/* Unshare variable. */
+} \share[\copy(b, \read_{LVAL}(a)), b];
+
+\read[a] {
+	/* Initiate application. */
+} \apply[\lambda(b, \read_{LVAL}(a)), b];
+
+\read[a] {
 	/* Read back abstraction. */
 } \lambda[\atom_{var(1)}, \read_{ABST(LVAL, var(0))}(a)];
 
@@ -29,10 +37,6 @@
 	/* Read back an atom. */
 } \atom;
 
-\bind[a, \atom_{RVAL}, a] {
-	/* Bind variable to an atom. */
-} \atom;
-
 \copy[\atom_{RVAL}, \atom_{strdup(RVAL)}] {
 	/* Copy an atom. */
 } \atom;
@@ -47,40 +51,56 @@
 } \atom;
 
 \lambda[a, b] {
+	/* Unshare variable. */
+} \share[\copy(c, \lambda(a, b)), c];
+
+\lambda[a, b] {
+	/* Initiate application. */
+} \apply[\lambda(c, \lambda(a, b)), c];
+
+\lambda[a, b] {
 	/* Apply a closed term. */
 } \lambda[a, b];
 
+\copy[a, b] {
+	/* Unshare variable. */
+} \share[\copy(c, \copy(a, b)), c];
+
+\copy[a, b] {
+	/* Initiate application. */
+} \apply[\lambda(c, \copy(a, b)), c];
+
 \copy[\lambda(a, b), \lambda(c, d)] {
 	/* Initiate copy of a closed term. */
 } \lambda[\dup(a, c), \dup(b, d)];
 
-\bind[a, \lambda(b, c), a] {
-	/* Bind variable to a closed term. */
-} \lambda[b, c];
+\dup[\amb(a, \share(b, c), c), \amb(d, \share(e, f), f)] {
+	/* Duplicate sharing. */
+} \share[\dup(b, e), \dup(a, d)];
+
+\dup[\apply(a, b), \apply(c, d)] {
+	/* Duplicate application. */
+} \apply[\dup(a, c), \dup(b, d)];
 
 \dup[\lambda(a, b), \lambda(c, d)] {
-	/* Duplicate abstraction or application. */
+	/* Duplicate abstraction. */
 } \lambda[\dup(a, c), \dup(b, d)];
 
-\dup[\copy(a, b), \copy(c, d)] {
-	/* Duplicate copy initiator. */
-} \copy[\dup(a, c), \dup(b, d)];
-
-\dup[\bind(a, b, c), \bind(d, e, f)] {
-	/* Duplicate variable binding. */
-} \bind[\dup(a, d), \dup(b, e), \dup(c, f)];
-
 \dup[a, b] {
 	/* Finish duplication. */
 } \dup[a, b];
 
 \erase {
-	/* Erase abstraction or application. */
-} \lambda[\erase, \erase];
+	/* Erase sharing. */
+} \share[a, a];
 
 \erase {
-	/* Erase variable binding. */
-} \bind[\erase, \erase, \erase];
+	/* Erase application. */
+} \apply[\erase, \erase];
+
+\erase {
+	/* Erase abstraction. */
+} \lambda[\erase, \erase];
 
 \erase {
 	/* Erase copy initiator. */
@@ -96,17 +116,12 @@
 
 $$
 
-{"Application"} = result;
-function = \lambda(argument, result);
-shared1 = \copy(first1, second1);
-shared2 = \copy(first2, second2);
-shared3 = \copy(first3, second3);
-
-{"Abstraction"} = bind0;
-bv1 = \bind(bind1, fv1, bind0);
-bv2 = \bind(bind2, fv2, bind1);
-bv3 = \bind(bind3, fv3, bind2);
-bindn = \lambda(variable, body);
+{"Application"} = \apply(function, argument);
+first1 = \amb(second1, \share(shared1, back1), back1);
+first2 = \amb(second2, \share(shared2, back2), back2);
+first3 = \amb(second3, \share(shared3, back3), back3);
+
+{"Abstraction"} = \lambda(variable, body);
 
 term = \read_{strdup("")}(\print);
 term = {"Encoding"};


This entry was originally posted at http://codedot.dreamwidth.org/170431.html

Поддержка недетерминированного расширения в INC
Daria Morgendorffer
codedot
В компиляторе сетей взаимодействия INC (Interaction Nets Compiler) теперь есть поддержка недетерминированного расширения в виде специального бинарного агента Amb с двумя главными портами. Это расширение необходимо при реализации стратегии "call-by-need" для λ-исчисления.

Синтаксис для недетерминированного расширения сетей взаимодействия выбран наиболее консервативным образом (по отношению к основной части языка программирования) и отличается от того, который встречается в литературе: при описании правил взаимодействия и начальной конфигурации агент Amb обозначается как тернарный, первый дополнительный порт которого выполняет роль второго главного. К примеру, следующее изменение не меняет поведение тестовой программы:

 
 $$
 
-\fan_{1}(x, x) = \fan_{2}(\erase, {&wire1});
+\fan_{1}(x, x) = \amb({&wire1}, \fan_{2}(\erase, y), y);
 
 {&wire2} = \fan_{3}({&erase}, \erase);
 


This entry was originally posted at http://codedot.dreamwidth.org/170218.html

Read-Back Extension
Daria Morgendorffer
codedot
Decoding extension for Implementation of Closed Reduction using Interaction Nets Compiler:

${
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

char *var(int fresh);
char *append(char *format, char *buf, char *str);

#define ABST(BUF, STR) append("%s%s: ", (BUF), (STR))
#define APPL(BUF, STR) append("%s%s ", (BUF), (STR))
#define ATOM(BUF, STR) append("%s(%s)", (BUF), (STR))
}$

\print {
	/* Output results of read-back. */
	puts(RVAL);
	exit(EXIT_SUCCESS);
} \atom;

\read[a] {
	/* Read back abstraction. */
} \lambda[\atom_{var(1)}, \read_{ABST(LVAL, var(0))}(a)];

\lambda[\read_{APPL(strdup(""), RVAL)}(a), a] {
	/* Read back application. */
} \atom;

\read[\atom_{ATOM(LVAL, RVAL)}] {
	/* Read back an atom. */
} \atom;

\bind[a, \atom_{RVAL}, a] {
	/* Bind variable to an atom. */
} \atom;

\copy[\atom_{RVAL}, \atom_{strdup(RVAL)}] {
	/* Copy an atom. */
} \atom;

\dup[\atom_{RVAL}, \atom_{strdup(RVAL)}] {
	/* Duplicate an atom. */
} \atom;

\erase {
	/* Erase an atom. */
	free(RVAL);
} \atom;

$$

term = \read_{strdup("")}(\print);
term = {"Encoding"};

$$

char *var(int fresh)
{
	static int id;

	char buf[BUFSIZ];

	if (fresh)
		++id;

	sprintf(buf, "v%d", id);
	return strdup(buf);
}

char *append(char *format, char *buf, char *str)
{
	size_t size = strlen(format) + strlen(str);
	char *result = malloc(strlen(buf) + size);

	sprintf(result, format, buf, str);

	free(buf);
	free(str);
	return result;
}


This entry was originally posted at http://codedot.dreamwidth.org/169787.html

Implementation of Closed Reduction
Daria Morgendorffer
codedot
An Interaction Net Implementation of Closed Reduction by Ian Mackie using Interaction Nets Compiler:

\lambda[a, b] {
	/* Apply a closed term. */
} \lambda[a, b];

\copy[\lambda(a, b), \lambda(c, d)] {
	/* Initiate copy of a closed term. */
} \lambda[\dup(a, c), \dup(b, d)];

\bind[a, \lambda(b, c), a] {
	/* Bind variable to a closed term. */
} \lambda[b, c];

\dup[\lambda(a, b), \lambda(c, d)] {
	/* Duplicate abstraction or application. */
} \lambda[\dup(a, c), \dup(b, d)];

\dup[\copy(a, b), \copy(c, d)] {
	/* Duplicate copy initiator. */
} \copy[\dup(a, c), \dup(b, d)];

\dup[\bind(a, b, c), \bind(d, e, f)] {
	/* Duplicate variable binding. */
} \bind[\dup(a, d), \dup(b, e), \dup(c, f)];

\dup[a, b] {
	/* Finish duplication. */
} \dup[a, b];

\erase {
	/* Erase abstraction or application. */
} \lambda[\erase, \erase];

\erase {
	/* Erase variable binding. */
} \bind[\erase, \erase, \erase];

\erase {
	/* Erase copy initiator. */
} \copy[\erase, \erase];

\erase {
	/* Erase duplicator. */
} \dup[\erase, \erase];

\erase {
	/* Finish erasing. */
} \erase;

$$

{"Application"} = result;
function = \lambda(argument, result);
shared1 = \copy(first1, second1);
shared2 = \copy(first2, second2);
shared3 = \copy(first3, second3);

{"Abstraction"} = bind0;
bv1 = \bind(bind1, fv1, bind0);
bv2 = \bind(bind2, fv2, bind1);
bv3 = \bind(bind3, fv3, bind2);
bindn = \lambda(variable, body);


This entry was originally posted at http://codedot.dreamwidth.org/169624.html

Hello Interaction Nets!
Daria Morgendorffer
codedot
$ cat >hello.in 
${
#include <stdio.h>
}$

\alpha {
        printf("%s %s!\n", LVAL, RVAL);
} \beta;

$$

\alpha_{"Hello"} = \beta_{"World"};

$$

#include <stdlib.h>

inagent *inaux(void *aux, void *offline)
{
        return NULL;
}

int main()
{
        interact();
        return 0;
}
$ inc <hello.in
$ c99 in.tab.c
$ ./a.out
Hello World!
$ 


This entry was originally posted at http://codedot.dreamwidth.org/169326.html

Поддержка начальной конфигурации в INC
Daria Morgendorffer
codedot
В компиляторе сетей взаимодействия INC (Interaction Nets Compiler) теперь есть поддержка начальной конфигурации. Конфигурация описывается на языке, близком к исчислению взаимодействия. Эта функциональность должна сильно упростить проект MLC: текст на языке MLC (Macro Lambda Calculus) можно будет целиком транслировать в исходный код для INC, а уже оттуда - в исполняемый код на Си. Трансляцию из MLC в INC можно сделать с помощью компактного представления λ-термов в сетях взаимодействия и механизма "readback" в виде системы взаимодействия с побочными действиями.

Ниже пример работы INC.

$ inc <example.in
$ c99 in.tab.c
$ ./a.out
inaux: rewired
inaux: returns
inaux: returns
inaux: returns
fan_1 >< fan_2
fan_3 >< fan_3
erase >< fan_3
fan_3 >< fan_3
erase >< erase
erase >< erase
$ 


This entry was originally posted at http://codedot.dreamwidth.org/169130.html

2048
Daria Morgendorffer
codedot
24308

This entry was originally posted at http://codedot.dreamwidth.org/168920.html

Проект P2Pinet
Daria Morgendorffer
codedot
В связи с идеей распределенных сетей взаимодействия, хотелось бы вернуться к проекту компилятора inet, который используется в MLC для механизма read-back. Приложение было реализовано уже после подготовки формального описания проекта и строго следуя проектной документации; имели место лишь мелкие уточнения и исправления по ходу работы.

Как модифицировать компилятор inet, чтобы получить вместо него распределенную универсальную P2P-сеть взаимодействия? Обозначим гипотетическую распределенную версию inet как p2pinet.

P2P-сеть всегда основана на дублировании информации для случаев, когда одна из нод отключается от сети. Заметим, что стэк активных пар, используемый в проекте inet, - это исчерпывающая информация о редуцируемой сети взаимодействия. Чаще всего (псевдо-)активная пара состоит не из двух агентов, а из агента и (псевдо-)агента wire, который служит для разыменования. Последнее в случае P2P-сети служило бы простым запросом на дублирование информации.

В p2pinet активные пары технически нигде не хранятся в явном виде, и ноды могут даже не знать, активна ли данная конкретная связь между одним идентификатором (портом) и каким-то другим в сети. Обмен информацией и (неявное) создание новых активных пар произходило бы в такой сети с помощью операции разыменования, а собственно применение правил взаимодействия - локально на нодах ввиду нескольких причин.

Во-первых, правила могут быть приватными для группы нод. Во-вторых, правила могут иметь побочные действия, как в проекте inet. В-третьих, набор правил может быть бесконечным и очень сложным. Наконец, одно из правил может быть вычислительно затратно, например вычисление n-ного простого числа.

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

Конкретно эту задачу сети взаимодействия и решают на качественном уровне. Они служат своеобразным планировщиком задач, который уже, в свою очередь, управляет остальными процессорами как устройствами, чем-то похожим на OpenCL образом. Однако, в отличие от OpenCL (который тоже, в принципе, может быть использован в распределенной сети), сети взаимодействия позволили бы делать и само планирование децентрализованным, при этом избегая лишних обмена данных и дублирования работы.

НаброскиCollapse )

This entry was originally posted at http://codedot.dreamwidth.org/168459.html

You are viewing codedot