Early this year, I made a post on LtU about the experimental "abstract" algorithm in MLC. Soon after that, Gabriel Scherer suggested doing exhaustive search through all possible inputs up to a particular size. Recently, I decided to conduct such an experiment. Here are

Some results

I managed to collect some results [1]. First of all, I had to pick a particular definition for "size" of a λ-term, because there are many. I chose the one that is used in A220894 [2]:

size(x) = 0;
size(λx.M) = 1 + size(M);
size(M N) = 1 + size(M) + size(N).

For sizes from 1 to 9, inclusively, there exist 5663121 closed λ-terms. I tested all of them against both "abstract" [3] and "optimal" [4] algorithms in MLC, with up to 250 interactions per term. The process took almost a day of CPU time. Then, I automatically compared them [5] using a simple awk(1) script (also available in [1]), looking for terms for which normal form or number of β-reductions using "abstract" would deviate from "optimal".

No such terms have been found this way. Surprisingly, there have been identified apparent Lambdascope counterexamples instead, the shortest of which is λx.(λy.y y) (λy.x (λz.y)) resulting in a fan that reaches the interaction net interface. I plan to look into this in near future.

As for sizes higher than 9, testing quickly becomes unfeasible. For example, there are 69445532 closed terms of sizes from 1 to 10, inclusively, which takes a lot of time and space just to generate and save them. [6] is a 200MB gzip(1)'ed tarball (4GB unpacked) with all these terms split into 52 files with 1335491 terms each. In my current setting, it is unfeasible to test them.

I may come up with optimizations at some point to make it possible to process terms of sizes up to 10, but 11 and higher look completely hopeless to me.

[1] https://gist.github.com/codedot/3b99edd504678e160999f12cf30da420
[2] http://oeis.org/A220894
[3] https://drive.google.com/open?id=1O2aTULUXuLIl3LArehMtwmoQiIGB62-A
[4] https://drive.google.com/open?id=16W_HSmwlRB6EAW5XxwVb4MqvkEZPf9HN
[5] https://drive.google.com/open?id=1ldxxnbzdxZDk5-9VMDzLvS7BouxwbCfH
[6] https://drive.google.com/open?id=1XjEa-N40wSqmSWnesahnxz6SXVUzzBig
Так называемые жесткие комбинаторы принадлежат более узкому классу graph relabeling systems, чем graph rewriting systems, к которым относятся сети взаимодействия в общем случае. По научным меркам, они введены буквально вчера - в нулевых. По их поводу написано полторы статьи, а наивная реализация в современных FPGA/ASIC и для жестких комбинаторов не очень многообещающая, так как агенты одновременно служат и для вычисления и для хранения данных, что слишком затратно для FPGA/ASIC, где суммарный объем памяти регистров всегда на порядок, если не на два, меньше доступной на той же доске встроенной RAM. У последнего неизбежно оказывается бутылочное горлышко.

В определенной перспективе жесткие сети взаимодействия - логичное продолжение развития процессоров. Но на данном этапе этот подход кажется слишком далеким от практики, - возможно, им потребуется еще несколько лет побыть в академических кругах. Впрочем, коммерческие компании типа ARM и сами метят в ту же сторону. К сожалению, пока это только пресс-релизы и провалившиеся проекты, тем не менее, ключевые слова правильные - "clockless computation".

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

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

Интернет позволяет передавать петабайты данных одновременно по тысячам разных каналов, когда как ни один из существующих суперкомпьютеров не может в одиночку добиться той же суммарной скорости в RAM. Можно посмотреть на интернет как на распределенную RAM. В связи с этим интересно было бы рассмотреть произвольные вычисления с использованием этой памяти.

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

Если же мы хотели бы иметь децентрализованную вычислительную сеть для произвольной работы без требования единого timeline, то неизбежно возникают проблемы локальности и конфлюэнтости. К счастью, системы взаимодействия как раз и обладают последними двумя свойствами, давая возможность продолжать вычисления оптимальным образом без необходимости немедленной синхронизации.


Один из вариантов того, как можно читать классическую монографию по λ-исчислению [1]:

параграф 2.1;
упр. 2.4.1 (i)-(iii), 2.4.2-2.4.13;
упр. 2.4.15 (только в оригинале [2]);
параграф 2.2;
упр. 2.4.14;

параграфы 3.1-3.3;
упр. 3.5.1 (v), 3.5.1 (i), 3.5.6 (i), 3.5.2, 3.5.3, 3.5.11;
параграфы 13.1-13.2 до приложения 13.2.3 включительно;

часть II (главы 6-10);

параграф 4.1;
упр. 4.3.2, 4.3.4;
главы 15 и 16.

В каком-то приближении именно этот материал изложен чрезвычайно кратко в [3] (по-русски).

[1] Х. Барендрегт. Ламбда-исчисление, его синтаксис и семантика. Москва, 1985.
[2] H. P. Barendregt. The Lambda Calculus, Its Syntax and Semantics. North-Holland, 1984.
[3] A. Salikhmetov. Lambda Calculus Synopsis. arXiv:1304.0558, 2013.
What's your status?

Issue 735 Resolved and Accepted.

Issue 736 Needs an Interpretation and Accepted as Marked by Don Cragun:
Interpretation response
------------------------
The standard is unclear on this issue, and no conformance
distinction can be made between alternative implementations
based on this.  This is being referred to the sponsor.

Rationale:
-------------
The following changes make the grammar and text reflect existing
practice.

Notes to the Editor (not part of this interpretation):
-------------------------------------------------------
On page 2350, lines 74801-74808, change

%start  complete_command
%%
complete_command : list separator
                 | list
                 ;

to:

%start program
%%
program          : linebreak complete_commands linebreak
                 | linebreak
                 ;
complete_commands: complete_commands newline_list complete_command
                 |                                complete_command
                 ;
complete_command : list separator_op
                 | list
                 ;

Cross-volume change to XRAT...

At page 3700 line 126612 section C.2.10 delete:

The start symbol of the grammar (complete_command) represents
either input from the command line or a shell script.  It is
repeatedly applied by the interpreter to its input and represents
a single "chunk" of that input as seen by the interpreter.

Issue 737 Resolved and Accepted.
http://austingroupbugs.net/view.php?id=737

Shell Grammar Rules for compound_list duplicate the definition of linebreak
linebreak        : newline_list
                 | /* empty */
                 ;
which results in four grammar rules for compound_list instead of two.

Desired Action

On page 2350, lines 74834-74838, change
compound_list    :              term
                 | newline_list term
                 |              term separator
                 | newline_list term separator
                 ;
to
compound_list    : linebreak term
                 | linebreak term separator
                 ;
http://austingroupbugs.net/view.php?id=736

An empty Shell program and a program consisting of two or more commands separated with NEWLINE tokens are valid Shell scripts. However, Shell Grammar Rules only accept exactly one single command which results in a syntax error against zero commands and two or more commands separated with NEWLINE tokens.

Desired Action

On page 2350, lines 74801-74808, change
%start  complete_command
%%
complete_command : list separator
                 | list
                 ;
to
%start script
%%
script           : commands linebreak
                 | /* empty */
                 ;
commands         : commands newline_list complete_command
                 |                       complete_command
                 ;
complete_command : list separator_op
                 | list
                 ;
http://austingroupbugs.net/view.php?id=735

When processed by yacc(1), Shell Grammar Rules result in 5 shift/reduce conflicts. These conflicts are all caused by unnecessary linebreak non-terminals in case_item_ns rule after compound_list non-terminals. The linebreak non-terminal are indeed unnecessary because compound_list rule
compound_list    :              term
                 | newline_list term
                 |              term separator
                 | newline_list term separator
                 ;
where
separator        : separator_op linebreak
                 | newline_list
                 ;
itself embeds linebreak definition
linebreak        : newline_list
                 | /* empty */
                 ;
Without the trailing linebreak non-terminals following compound_list, yacc(1) produces no shift/reduce conflicts.

Desired Action

On page 2351, lines 74863-74866, change
case_item_ns     :     pattern ')'               linebreak
                 |     pattern ')' compound_list linebreak
                 | '(' pattern ')'               linebreak
                 | '(' pattern ')' compound_list linebreak
                 ;
to
case_item_ns     :     pattern ')' linebreak
                 |     pattern ')' compound_list
                 | '(' pattern ')' linebreak
                 | '(' pattern ')' compound_list
                 ;
http://www.cims.nyu.edu/~eve2/predprey.pdf

Prime number selection of cycles in a predator-prey model
Eric Goles, Oliver Schulz, Mario Markus

The fact that some species of cicadas appear every 7, 13, or 17 years and that these periods are prime numbers has been regarded as a coincidence. We found a simple evolutionary predator-prey model that yields prime-periodic preys having cycles predominantly around the observed values. An evolutionary game on a spatial array leads to travelling waves reminiscent of those observed in excitable systems. The model marks an encounter of two seemingly unrelated disciplines: biology and number theory. A restriction to the latter, provides an evolutionary generator of arbitrarily large prime numbers.

Via [livejournal.com profile] udod's post and Wikipedia.
http://mathoverflow.net/questions/129923

It is possible to implement λ-calculus in Schönhage's storage modification machine using an infinite set of nodes and one single program consisted exclusively of (about hundred) instructions set w to v (with different w and v) using a compact directed encoding for λ-terms closely related to directed interaction combinators by Lafont, and four infinite spaghetti stacks based on linked nodes to perform interaction and indirection rules on configurations.

Is it possible to preserve Turing-completeness of the SMM model while restricting its instruction set to only a single instruction set w to v (with constant w and v) during the whole computation process?

I would be very grateful for any references regarding this question.
In theoretical computer science a pointer machine is an "atomistic" abstract computational machine model akin to the Random access machine.

Depending on the type, a pointer machine may be called a linking automaton, a KU-machine, an SMM, an atomistic LISP machine, a tree-pointer machine, etc. (cf Ben-Amram 1995). At least three major varieties exist in the literature—the Kolmogorov-Uspenskii model (KUM, KU-machine), the Knuth linking automaton, and the Schönhage Storage Modification Machine model (SMM). The SMM seems to be the most common.

This should definitely help to answer two questions on MathOverflow, regarding Turing-complete primitive blind automata and Universality of blind graph rewriting.
http://mathoverflow.net/questions/126941/

Существуют несколько способов представить λ-термы в сетях взаимодействия; например, алгоритм Лэмпинга для оптимальной редукции или компиляция λ-исчисления в комбинаторы взаимодействия. Однако, все известные нам способы реализуют только β-редукцию, но не экстенсиональное λ-исчисление (где также есть η-редукция).

Можно ли представить λ-термы в сетях взаимодействия, реализовав βη-редукцию?

(Нормальная форма сети для терма должна соответствовать его βη-нормальной форме.)

Emacs

Jan. 7th, 2013 01:02 am
IEEE 1003.1-2008, C.4.3 Exclusion of Utilities:

emacs

The community of emacs editing enthusiasts was adamant that the full emacs editor not be included in the base documents because they were concerned that an attempt to standardize this very powerful environment would encourage vendors to ship versions conforming strictly to the standard, but lacking the extensibility required by the community. The author of the original emacs program also expressed his desire to omit the program. Furthermore, there were a number of historical UNIX systems that did not include emacs, or included it without supporting it, but there were very few that did not include and support vi.
  • Английский язык.
  • Десятипальцевая печать.
    • Аппликатура.
    • Раскладка клавиатуры для левой руки и модификаторы справа.
    • Раскладка клавиатуры для правой руки и модификаторы слева.
    • Caps-lock.
  • E-mail.
    • Оформление писем.
      • Plain text.
      • Обращение, приветствие, введение.
      • Соответствующий языковой стиль текста.
      • Заключение и подпись.
      • Постскриптум и краткая подпись.
    • Carbon-copy и blind-carbon-copy.
    • Reply и reply-to-all.
    • Forwarding.
  • Базовые навыки работы с операционной системой
  • Элементы предметной области.
    • LaTeX.
    • Web.
    • Portable System Interface.
  • Практика программирования.
#if 0
#include <stdbool.h>
#endif

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

static enum bool {
	true = 0xdead, false = 0xbeaf
} bool;

static enum cast {
	const_cast,
	dynamic_cast,
	reinterpret_cast,
	static_cast
} cast;

static struct class {
	struct class *namespace;
	int explicit;
	int friend;
	int mutable;
	int private;
	int protected;
	int public;
	int virtual;
} class;

static catch()
{
	return 0;
}

static try()
{
	return 0;
}

static throw()
{
	return 0;
}

static delete()
{
	return 0;
}

static export()
{
	return 0;
}

static usage(str)
	const char *str;
{
	fprintf(stderr, "Usage: %s id type op\n", str);
	exit(EXIT_FAILURE);
}

main(argc, argv)
	char *argv[];
{
	void *new = &class;
	char *typeid, *typename, *operator;
	int this;
	int using;

	if (4 > argc)
		usage(argv[0]);

	class.namespace = new;
	typeid = argv[1];
	typename = argv[2];
	operator = argv[3];
	this = !strcmp(typename, "this");
	using = atoi(typeid);
	printf("ID#%d is %s\n", using, this ? "mine" : "yours");
	return 0;
}
https://gist.github.com/4139831

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

alexo@euromake:/tmp$ git clone git://gist.github.com/4139831.git gentree
Cloning into gentree...
remote: Counting objects: 8, done.
remote: Compressing objects: 100% (7/7), done.
remote: Total 8 (delta 1), reused 5 (delta 1)
Receiving objects: 100% (8/8), done.
Resolving deltas: 100% (1/1), done.
alexo@euromake:/tmp$ cd gentree/
alexo@euromake:/tmp/gentree$ make
cc     gentree.c   -o gentree
./gentree 0 >output.c
make output
make[1]: Entering directory `/tmp/gentree'
cc     output.c   -o output
make[1]: Leaving directory `/tmp/gentree'
[ 0 = $(./output) ]
alexo@euromake:/tmp/gentree$ git grep Grammar
gentree.c:/* Grammar: <tree> ::= '0' | '1' <tree> <tree>. */
alexo@euromake:/tmp/gentree$ make TEST=1101000
./gentree 1101000 >output.c
make output
make[1]: Entering directory `/tmp/gentree'
cc     output.c   -o output
make[1]: Leaving directory `/tmp/gentree'
[ 1101000 = $(./output) ]
make: *** [all] Error 1
alexo@euromake:/tmp/gentree$ git grep TODO
gentree.c:      /* TODO: print some code in stdout. */
alexo@euromake:/tmp/gentree$ vi gentree.c
Это музыкой навеяло:

alexo@euromake:/tmp/and$ cat and.c
void *
true_(x, y)
void *x, *y;
{
        return x;
}

void *
false_(x, y)
void *x, *y;
{
        return y;
}

void *
bool_[] = {false_, true_};

void *
and(x, y)
void *(*x)(), *y;
{
        return x(y, x);
}

main(argc, argv)
char *argv[];
{
        int x = argv[1][0] - '0';
        int y = argv[2][0] - '0';

        return (true_ == and(bool_[x], bool_[y]));
}
alexo@euromake:/tmp/and$ cat Makefile
all: and
        ./and 0 0; echo $$?
        ./and 0 1; echo $$?
        ./and 1 0; echo $$?
        ./and 1 1; echo $$?

clean:
        -rm -f and
alexo@euromake:/tmp/and$ make
cc     and.c   -o and
./and 0 0; echo $?
0
./and 0 1; echo $?
0
./and 1 0; echo $?
0
./and 1 1; echo $?
1
alexo@euromake:/tmp/and$ 
Едва заметным прошел момент, когда в нашем распоряжении оказалось достаточно материала, чтобы более явно показать, что системы слепой перезаписи графов действительно обладают полнотой по Тьюрингу. Как и предполагалось ранее, достаточно элегантным способом является симуляция направленных комбинаторов взаимодействия, которые сами обладают Тьюринг-полнотой (см. статью Lafont "Interaction Combinators" 1997 года). И хотя по общим соображениям этот факт был понятен еще полгода назад (см. "Логические операции без сравнений"), на данный момент доказательство можно построить из нескольких пунктов.

Мы будем опираться на предыдущие описания наших конструкций. Напомним, что первым шагом был выбор представления направленных комбинаторов γ, γ*, δ и δ*, а также двух видов связей между агентами: между двумя главными портами и между дополнительным и главным (см. "Слепые комбинаторы взаимодействия"). Затем мы получили представление для недостающего третьего вида связей, то есть между двумя дополнительными портами (см. "Слепые двунаправленные соединения"). Наконец, мы добились того, чтобы за один цикл работы системы количество используемых ячеек оставалось постоянным (см. "Баланс освобождаемой и выделяемой памяти"). В заключение мы пояснили выбор алгоритмов работы системы (см. "Трюки в синтаксическом сахаре λ-исчисления").

Итак, во-первых, заметим, что участие ε не влияет на ход вычислений. Поэтому мы можем заменить ε и ε* на свободные порты, которые, в свою очередь, симулируем парами ξ и ξ*, не связанными с чем-либо на противоположной стороне.

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

В-третьих, по аналогии с aord построим алгоритм слепого копирования агентов, такой, что для данных α, β из набора {γ, δ} на месте β оказывается тот же тип агента, что и у агента α (пусть данная задача послужит несложным упражнением читателю). Копирование агентов γ* и δ* тривиально. Поясним, что копирование необходимо при дублировании (элемент списка D), для чего требуется преобразовать оба освобождаемых после аннигиляции агента (элемент списка A) неизвестных типов, в общем случае, в неизвестные типы.

Тогда в порядке обработки списков, диктуемом балансом освобождаемой и выделямой памяти, то есть за цикл по паре элементов из списков L и R и по одному элементу из списков A и D, машина слепой перезаписи симулирует взаимодействие направленных комбинаторов.



P. S. Как правильно заметил [livejournal.com profile] nivanych, полученная нами система имеет прямое отношение к конкатенационным языкам программирования. А именно, о списках A, D, L и R можно думать как о четырех стеках. Как мы видим, симуляция направленных комбинаторов взаимодействия с помощью слепой перезаписи графов в данном случае действительно породила стековую машину, имеющую одну кучу и четыре стека.
Только что понял, что именно мне напоминает схема вычисления с четырьмя списками L, A, D, R и алгоритмом сортировки "мусора" aord. Она во многом похожа на механизм транскрипции в биологии (процесс синтеза РНК с использованием ДНК в качестве матрицы).

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

Произведя нехитрый поиск, я немедленно натолкнулся на книгу Maribel Fernandez под названием "Models of Computation: An Introduction to Computability Theory" и теперь жду не дождусь заполучить ее в руки:



http://www.amazon.co.uk/dp/1848824335

P. S. Получил, наконец-то. Оказалось неплохим вводным учебником по CS в его современном виде.
+

1. Implement eye-tracking in Project Glass as a pointing input device.
2. Buy Dasher Project by Inference Group before someone else does.
3. Apply real-time collaborative filtering to online dictionaries if your cloud got any balls :-P
4. ???
5. PROFIT!!!
Page generated Jul. 18th, 2025 03:17 am
Powered by Dreamwidth Studios