Anton Salikhmetov

This is how you convert C source code (or any other ASCII text) into strings in C using Shell.

make(1) rules:


sed(1) script:


( Output )

Чтобы упростить разработку симулятора нашей системы слепой перезаписи графов, мы подготовили проект нового языка программирования на основе нотации Lafont с описанием побочных действий на языке Си. По аналогии с yacc(1) и lex(1) выходными данными нашего компилятора будет модуль на языке Си. Синтаксис нашего языка программирования выбран близким к тому, как записываются правила взаимодействия в LaTeX.


Ниже пример программы на этом языке. Как видно по данному "Hello World", программы похожи по структуре к описанию парсеров и лексических анализаторов на yacc(1) и lex(1), с помощью которых и будет реализован компилятор нашего языка.


https://github.com/codedot/inet

Это музыкой навеяло:

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$ 

Только что понял, что именно мне напоминает схема вычисления с четырьмя списками 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 в его современном виде.

Помимо материала, компактно собранного в шпаргалках по теории и практике λ-исчисления, ниже будут использоваться следующие обозначения. Во-первых, металамбда-абстракция λx.f(x) — безымянная запись теоретико-множественной функции f, например (λx.x² + 1)(3) = 10. Во-вторых, определим множество кодов конечных последовательностей (при какой-либо стандартной их кодировке натуральными числами)

Seq = {<n₁,…, n_k> | k ∈ N, n₁,…, n_k ∈ N} ∪ {< >};
lh(< >) = 0;
α = <n₁,…, n_k> ∈ Seq ⇒ lh(α) = k;
α = <m₁,…, m_p>, β = <n₁,…, n_q> ∈ Seq ⇒ a * b = <m₁,…, m_p, n₁,…, n_q>;
α = <m₁,…, m_p>, β = <n₁,…, n_q> ∈ Seq ∧ p ≤ q ∧ m₁ = n₁ ∧ … ∧ m_p = n_p ⇒ α ≤ β.

Пусть D = (D, ⊑) — частично упорядоченное множество с рефлексивным отношением ⊑. Тогда подмножество X ⊆ D называется направленным, если

X ≠ ∅ ∧ ∀x, y ∈ X: ∃z ∈ X: x ⊑ z ∧ y ⊑ z.

При этом D называется полным, если для любого направленного подмножества X ⊆ D существует супремум ⊔X ∈ D и имеется дно ⊥:

∃⊥ ∈ D: ∀x ∈ D: ⊥ ⊑ x.

Топология Скотта на полном частично упорядоченном множестве (D, ⊑) определяется следующим образом: множество O ⊆ D считается открытым, если

1) x ∈ O ∧ x ⊑ y ⇒ y ∈ O;
2) X ⊆ D ∧ ⊔X ∈ O ⇒ X ∩ O ≠ ∅.

Частичное отображение φ: X ↝ Y — это отображение φ, такое, что область определения Dom(φ) ⊆ X. Для x ∈ X запись φ(x)↓ означает, что φ(x) определено, то есть x ∈ Dom(φ); φ(x)↑ означает, что φ(x) не определено, то есть x ∉ Dom(φ).

Если Σ — некоторое множество символов, то частично Σ-помеченное дерево — это частичное отображение φ: Seq ↝ Σ × N, такое, что

1) φ(σ)↓ ∧ τ ≤ σ ⇒ φ(τ)↓;
2) φ(σ) = <a, n> ⇒ ∀k ≥ n: φ(σ * <k>)↑.

Обнаженное дерево, лежащее в основе частично Σ-помеченного дерева φ, — это дерево

T_φ = {< >} ∪ {σ | σ = σ' * <k> ∧ φ(σ') = <a, n> ∧ k < n}.

Если σ ∈ T_φ и φ(σ) = <a, n>, то a называется меткой в узле σ. Если же для σ ∈ T_φ φ(σ)↑, то говорят, что узел σ непомеченный. Частично помеченные деревья будем обозначать заглавными буквами и будем писать σ ∈ A вместо σ ∈ T_A и A(α) = ⊥, когда A(α)↑, но все же α ∈ A.

Если Σ = {λx₁.…λx_n.x | n ≥ 0, x₁,…, x_n, x ∈ Λ}, то частично Σ-помеченное дерево называется деревом бемовского типа. Множество всех таких деревьем обозначим B. Поддерево дерева A, исходящее из узла α — это A_α = λβ.A(α * β). Очевидно, что ∀A ∈ B: ∀α: A_α ∈ B.

Комбинатор M разрешим, если

∃n: ∃N₁,…, N_n ∈ Λ₀: M N₁ … N_n = I.

Например, комбинатор неподвижной точки разрешим, так как Y (K I) = K I (Y (K I)) = I. С другой стороны, Ω неразрешим. Произвольное λ-выражение разрешимо, если разрешим комбинатор λx₁.…λx_n.M, где {x₁,…, x_n} = FV(M).

λ-выражение M является головной нормальной формой, если оно имеет вид

M ≣ λx₁.…λx_n.x M₁ … M_m, m, n ≥ 0.

Говорят, что M имеет головную нормальную форму N, если M = N. Главной называется та головная нормальная форма выражения, которая первой достигается его левой редукцией.

Уодсворт ввел класс λ-выражений, не имеющих головной нормальной формы, и привел доводы в пользу того, что элементы этого класса должны рассматриваться как бессмысленные выражения в λ-исчислении. Также ему принадлежит следующий важный результат: λ-выражение разрешимо тогда и только тогда, когда оно имеет головную нормальную форму. Таким образом, из неразрешимости M следует, что для любых выражений N₁,…, N_n выражение M N₁ … N_n не имеет нормальной формы.

Дерево Бема для терма M, обозначаемое через BT(M), — это дерево бемовского типа, определяемое следующим образом:

1) если M неразрешим, то ∀σ: BT(Μ)(σ)↑,
2) если M разрешим и имеет главную головную нормальную форму λx₁.…λx_n.x M₀ … M_{m - 1}, то

BT(M)(< >) = <λx₁.…λx_n.x, m>;
k < m ⇒ BT(M)(<k> * σ) = BT(M_k)(σ);
k ≥ m ⇒ BT(M)(<k> * σ)↑.

Рассмотрим полное частично упорядоченное множество B = (B, ⊆) с топологией Скотта. Топология деревьев на множестве Λ — это наименьшая топология, в которой непрерывно отображение BT: Λ → B. Иными словами, открытые подмножества Λ имеют вид BT^-1(O), где O открыто в топологии Скотта на B.

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

Доказано, что аппликация и абстракция непрерывны в топологии деревьев на Λ, причем для аппликации это нетривиальный результат, имеющий интересные следствия. Например, множество Sol ⊆ Λ разрешимых термов открыто. Действительно, в любом полном частично упорядоченном множестве множество {x | x ≠ ⊥} открыто по Скотту. Следовательно, множество Sol = BT^-1{A | A ≠ ⊥} открыто в Λ.

Читая о моделях λ-исчисления в классической монографии по λ-исчислению (Х. Барендрегт, «Ламбда-исчисление. Его синтаксис и семантика», перевод с английского Г. Е. Минца под редакцией А. С. Кузичева, Москва, «Мир», 1985), я вдруг нашел ответ на свое старое недоумение, почему категорщикам не нравится отсутствие типов:

История λ-исчисления уходит в начало прошлого века. Этимология названия данного раздела математической логики, который служит основой для «computer science», следующая. Сам значек «λ» используется для одной из двух основных конструкций в созданной Черчем системе — абстракции. Оказывается, что выбор обозначения абстракции не был совершенно случайным, а сделан в противопоставление другой более ранней конструкции, которую использовали Whitehead и Russell и обозначали как «xˆ». Для новой конструкции, чтобы отличать ее от прежней, Черч заменил обозначение сначала на «∧x», а затем — на «λx», очевидно, интерпретировав первый символ как заглавную букву «Λ», для упрощения набора.

Опишем кратко систему λβη, то есть классическое бестиповое экстенсиональное λ-исчисление, вывернув наизнанку монографию Барендрегта.

Множество λ-выражений Λ строится индуктивно из переменных

x, y, z… ∈ Λ

с помощью абстракций

M ∈ Λ ⇒ λx.M ∈ Λ

и аппликаций

M, N ∈ Λ ⇒ M N ∈ Λ,

при этом аппликация лево-ассоциативна:

(M) ≣ M, M N P ≣ (M N) P.

Рефлексивное транзитивное отношение Μ ⊂ N означает, что M является подвыражением выражения N:

M ⊂ M ⊂ λx.M;
M ⊂ M N ⊃ N;
M ⊂ N ∧ N ⊂ P ⇒ M ⊂ P.

FV(M) — это множество свободных переменных в выражении M:

FV(x) ≣ {x};
FV(λx.M) ≣ FV(M) ∖ {x};
FV(M N) ≣ FV(M) ∪ FV(N).

Переменные, которые не являются свободными, называются связанными и могут быть заменены другой переменной (такое преобразование называют α-конверсией):

y ∉ FV(M) ⇒ λx.M ≣ λy.M[x := y], где M[x := N] — результат подстановки:

x[x := P] ≣ P;
y[x := P] ≣ y;
(λx.M)[x := P] ≣ λx.M;
(λy.M)[x := P] ≣ λy.M[x := P];
(M N)[x := P] ≣ M[x := P] N[x := P].

В четвертом пункте не нужно специально оговаривать условие «x ≢ y и y ∉ FV(P)», так как оно выполняется в силу соглашения о переменных: если в определенном математическом контексте встречаются термы M₁,…, M_n, то подразумевается, что связанные переменные в них выбраны так, чтобы они были отличны от свободных переменных.

Если множество FV(M) пусто, то M называют комбинатором. Множество всех комбинаторов обозначают Λ₀:

Λ₀ ≣ {M ∈ Λ | FV(M) = ∅}.

Следующие отношения β, η и βη являются редукциями:

β ≣ {((λx.M) N, M[x := N]) | M, N ∈ Λ};
η ≣ {(λx.M x, M) | M ∈ Λ, x ∉ FV(M)};
βη ≣ β ∪ η.

Выражение, подвыражением которого является дырка, называется контекстом и обозначается C[ ], при этом C[M] — результат подстановки выражения M вместо дырки в контексте C[ ].

Если σ — редукция, то выражение M — σ-редекс, если ∃N: (M, N) ∈ σ. Также можно говорить и о σ-конверсии «=_σ»:

(M, N) ∈ σ ⇒ C[Μ] →_σ C[N];
M ↠_σ M;
M →_σ N ⇒ M ↠_σ N;
M →_σ N ∧ N →_σ P ⇒ M ↠_σ P;
∃P: M ↠_σ P ∧ N ↠_σ P ⇒ M =_σ N.

σ-нормальной формой называют выражение Μ, если ∄Ν: M →_σ Ν. В экстенсиональном λ-исчислении под редексом имеют в виду βη-редекс, а под нормальной формой — βη-нормальную форму. Говорят, что M имеет нормальную форму N, если M ↠ N. При этом βη-конверсию обычно обозначают просто «=», и это неслучайно: формально система λβη является эквациональной теорией. Так как такие теории свободны от логики, непротиворечивость в них определяется несколько иначе.

Равенством будем считать формулу вида M = N, где M, N — λ-выражения; такое равенство замкнуто, если M и N — комбинаторы. Пусть T — формальная теория, формулами которой являются равенства. Тогда говорят, что T непротиворечива (и пишут Con(T)), если в T доказуемо не любое замкнутое равенство. В противном случае говорят, что T противоречива. Одна из причин рассмотрения λβη состоит в том, что эта теория обладает определенным свойством полноты. Эквациональная теория T называется полной по Гильберту-Посту (сокращенно HP-полной), если для любого равенства M = N в языке теории T или M = N доказуемо, или T + (M = N) противоречива. HP-полные теории соответствуют максимальным непротиворечивым теориям в теории моделей для логики первого порядка.

Стратегия — это такое отображение F: Λ → Λ, что ∀M: M ↠ F(M). Для одношаговой стратегии выполняется ∀M: M → F(M). Стратегия называется нормализующей, если для любого выражения M, имеющего нормальную форму N, для некоторого числа n выполняется Fⁿ(M) ≣ N. Левая редукция F_l — одна из самых простых одношаговых нормализующих стратегий: она заключается в выборе β-редекса, значек «λ» в котором стоит текстуально левее, чем у других β-редексов, либо левого η-редекса, если β-редексов нет. Таким образом, если два терма имеют общую нормальную форму, то с помощью левой редукции доказательство соответствующей формулы можно получить за конечное число простых шагов. Если же формула недоказуема, то либо процесс не завершается вовсе, либо он завершается на разных нормальных формах.

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)].

Одним из наиболее компактных способов описания правил «interaction nets» является эзотерический язык программирования, предложенный в статье 1989 года «Interaction nets» (Lafont) — см. стр. 104. Он основан на двух наблюдениях. Во-первых, левая часть любого правила всегда содержит лишь два агента, которые связаны своими главными портами. Во-вторых, правая часть каждого правила никогда не содержит редексов, из чего следует, что дополнительные порты обоих взаимодействующих агентов в общем случае являются корнями деревьев, листья которых связаны между собой произвольным образом. Поэтому описанию подлежат лишь сами деревья, а также связи между листьями.

В качестве примера возьмем первое правило для системы с агентами типов γ и δ. Сначала оттолкнемся от более простой избыточной нотации, не требующей дополнительных пояснений, в которой первый аргумент агента соответствует главному порту:

γ(x, y, z), δ(x, v, w) → δ(y, a, b), δ(z, c, d), γ(v, a, c), γ(w, b, d).

Воспользуемся первым наблюдением:

γ[y, z] >< δ[v, w] → δ(y, a, b), δ(z, c, d), γ(v, a, c), γ(w, b, d).

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

γ[δ(a, b), δ(c, d)] >< δ[γ(a, c), γ(b, d)].

Два других правила системы записываются проще, так как соответствующие деревья с корнями на дополнительных портах левой части состоят каждое лишь из одного листа:

δ[x, y] >< δ[x, y], γ[x, y] >< γ[y, x].

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

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

Другое дело с конструктивными объектами. Любой из них можно определить индуктивно с помощью правил как при описании нового языка, без аксиоматики. Известно, что любая конструкция, которой можно в общем случае научить оперировать другого человека или машину, неизбежно окажется определимой таким образом.

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

Не все знают, что такое λ-исчисление. Чаще всего с этим термином связывают систему λΚβη, иногда типизированные ее варианты. Однако, более общее значение термина — это раздел математической логики, занимающийся изучением целого класса подобных систем и их свойств, центральное место среди которых, действительно, занимает бестиповая λΚβη. Более точно, λ-исчисление — это применение классического матаппарата к изучению λ-теорий и их моделей.

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