https://dx.doi.org/10.2139/ssrn.3271944

This paper takes a look at the Talmudic rule aka the 1/N rule aka the uniform investment strategy from the viewpoint of elementary microeconomics. Specifically, we derive the cardinal utility function for a Talmud-obeying agent which happens to have the Cobb-Douglas form. Further, we investigate individual supply and demand due to rebalancing and compare them to market depth of an exchange. Finally, we discuss how operating as a liquidity provider can benefit the Talmud-obeying agent with every exchange transaction in terms of the identified utility function.
https://arxiv.org/abs/1808.06351

Lambda Calculus with Explicit Read-back

This paper introduces a new term rewriting system that is similar to the embedded read-back mechanism for interaction nets presented in our previous work, but is easier to follow than in the original setting and thus to analyze its properties. Namely, we verify that it correctly represents the lambda calculus. Further, we show that there is exactly one reduction sequence that starts with any term in our term rewriting system. Finally, we represent the leftmost strategy which is known to be normalizing.
Configuration

<... | x = α(...y...), y = β(...x...)>

can be reduced to both

<... | x = α(...β(...x...)...)>

and

<... | y = β(...α(...y...)...)>,

which syntactically appears as a counterexample to strong confluence, while essentially representing the same configuration.

Is there a way to formalize equivalence between those two normal forms?

I think there is:

https://arxiv.org/abs/1806.07275

Upward confluence in the interaction calculus

The lambda calculus is not upward confluent, one of counterexamples being known due to Plotkin. This paper explores upward confluence in the interaction calculus. Can an interaction system have this property? We positively answer this question and also provide a necessary and sufficient condition for stronger one-step upward confluence. However, the provided condition is not necessary for upward confluence as we prove that the interaction system of the linear lambda calculus is upward confluent.
https://dx.doi.org/10.2139/ssrn.3166840

This paper studies the Talmudic rule aka the 1/N rule aka the uniform investment strategy on the microscopic scale, that is on the scale of single transactions. We focus on the simplest case of only two assets and show that the Talmudic rule results in each transaction to increase geometric mean of assets, regardless of price change direction. Then, we answer the following question: given any sequence of prices, how to find its optimal subsequence, maximizing the total growth of the geometric mean of assets? We conclude with an algorithm that can be used to analyze various sequences of prices and help develop trading strategies based on the Talmudic rule.
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
From command line to MLC:

$ npm i -g @alexo/lambda
└── @alexo/lambda@0.3.6

$ node work2mlc.js getwork.json 381353fa | tee test.mlc
Mid = x: x
        hex(24e39e50)
        hex(1efebbc8)
        hex(fb545b91)
        hex(db1ff3ca)
        hex(a66f356d)
        hex(7482c0f3)
        hex(acc0caa8)
        hex(00f10dad);

Data = x: x
        hex(a7f5f990)
        hex(fd270c51)
        hex(378a0e1c);

Nonce = hex(381353fa);

Zero32 (Pop 8 (RunHash Mid Data Nonce))
$ lambda -pem lib.mlc -f test.mlc
3335648(653961), 17837 ms
v1, v2: v1
$ 

https://gist.github.com/codedot/721469173df8dd197ba5bddbe022c487
https://gist.github.com/codedot/721469173df8dd197ba5bddbe022c487

$ npm i -g @alexo/lambda
└── @alexo/lambda@0.3.6

$ make
	shasum -a 256 /dev/null
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  /dev/null
	lambda -pem lib.mlc 'Pri32 hex(e3b0c442)'
857(230), 19 ms
_1 _1 _1 _0 _0 _0 _1 _1 _1 _0 _1 _1 _0 _0 _0 _0 _1 _1 _0 _0 _0 _1 _0 _0 _0 _1 _0 _0 _0 _0 _1 _0
	lambda -pem lib.mlc 'Pri32 (Shift 8 (Hash1 NullMsg))'
3247721(688463), 17211 ms
_1 _1 _1 _0 _0 _0 _1 _1 _1 _0 _1 _1 _0 _0 _0 _0 _1 _1 _0 _0 _0 _1 _0 _0 _0 _1 _0 _0 _0 _0 _1 _0
	shasum -a 256 </dev/null | xxd -r -p | shasum -a 256
5df6e0e2761359d30a8275058e299fcc0381534545f55cf43e41983f5d4c9456  -
	lambda -pem lib.mlc 'Pri32 hex(5df6e0e2)'
856(230), 15 ms
_0 _1 _0 _1 _1 _1 _0 _1 _1 _1 _1 _1 _0 _1 _1 _0 _1 _1 _1 _0 _0 _0 _0 _0 _1 _1 _1 _0 _0 _0 _1 _0
	lambda -pem lib.mlc 'Pri32 (Shift 8 (Hash2 NullMsg))'
6448027(1373506), 38750 ms
_0 _1 _0 _1 _1 _1 _0 _1 _1 _1 _1 _1 _0 _1 _1 _0 _1 _1 _1 _0 _0 _0 _0 _0 _1 _1 _1 _0 _0 _0 _1 _0
$ 
После пятнадцатой главы в плане "Как читать Барендрегта" остается только одна, самая главная - шестнадцатая. В ней, наконец-то, показано, что HP-полное расширение всех осмысленных λ-теорий - это H*, и другого не дано.

16.5.1. Покажем, что
(i) для любого замкнутого терма Z в теории H доказуемо
Z Ω~n = Ω для некоторого n:
если Z неразрешим, то он равен Ω по определению H, иначе
Z имеет головную нормальную форму x1,..., xn: xi Z1 ... Zn, и тогда
Z Ω~n неразрешим и равен Ω по определению H;
(ii) если A x ->> z: z (A (x Ω)), то A Z = A Z' доказуемо
в теории H* для любых термов Z и Z', а
в теории H только для замкнутых Z и Z':
ввиду (i) для некоторого n имеем
A Z ->>βηΩ z1: z1 (...(zn: zn (A Ω))...) <<-βηΩ A Z',
в HP-полной H* содержится, в частности,
непротиворечивая Hω ввиду ее осмысленности,
поэтому там выводимо также следствие A Z = A Z',
но в H правило ω не имеет места.

16.5.2. Покажем, что в H имеет место ext0, но не имеет места ext:
ext влечет правило η, а оно не имеет места в H;
пусть теперь M x = N x, где M и N замкнуты, тогда
M x = N x = Ω может быть только по причине M = N = Ω,
а в противном случае M = x1,..., xm: xi M1 ... Mn и N = y1,..., yn: yj N1 ... Nn,
для которых даже в λ доказуемо M = N (см. упр. 2.4.13).

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

16.5.9. Покажем, что терм M разрешим тогда и только тогда,
когда теория λ + (M = Y K) противоречива:
(=>) если M разрешим, то для некоторых термов N1,..., Nn
M N1 ... Nn = K, при этом Y K N1 ... Nn = Y K, но K # Y K (см. упр. 6.8.3);
(<=) если λ + (M = Y K) противоречива, то M разрешим, иначе
в непротиворечивой H выводилось бы M = Ω = Y K.
От упражнений остальных глав второй части монографии в 27 уже морщит, как в 50, поэтому перейду сразу к пятнадцатой, где вводится понятие редукции-оракула, которое анализирует доказуемость в осмысленной теории H и говорит, на что еще нет смысла тратить время.

15.4.1. Покажем, что любой терм M Ωη-сильно нормализуем:
η-редукцию всегда можно отложить, при этом
любой терм имеет единственную Ω-нормальную форму и
единственную η-нормальную форму.

15.4.2. Будем писать x \in_R M, если x входит в любой N =R M.
Покажем, что
(i) x \in_βηΩ A x, если A = ω ω, где ω = a, x, z: z (a a (x Ω)):
редукция A x ->>β <...<A (χ^n Ω)>...> не порождает Ω-редексов;
(ii) имеется замкнутый терм O, такой, что
O x [n] z ->>β z Ω~n (O x [n + 1] z) и x \in_βηΩ O x [0]:
возьмем O = Θ (o, x, n, z: (W z n) (o x (S+ n) z)),
где W = Θ (w, z, n: (Zero n) z (w z (P- n) Ω));
(iii) для любого замкнутого F есть замкнутый H, такой, что
H c i a ->>β x: x I (F c a (H c i (S+ a))) и x \in_βηΩ H c x [0]:
возьмем H = Θ (h, c, i, a: (x: x I (F c a (h c i (S+ a)))));
ни в редукции O, ни в редукции H не появляется Ω-редексов.

15.4.3. Пусть у нас есть такая рекурсивная функция f, что
f(n) = 0, если n входит в некоторое множество, иначе f(n) = 1.
Тогда покажем, что
(i)-(ii) λ + {Ω [n] = T | f(n) = 0} + {Ω [n] = F | f(n) = 1} непротиворечива:
λ-определим f через G и вспомним, что терм Ω легкий, поэтому
его можно, в частности, приравнять к n: Zero (G n);
(iii) без нерекурсивных функций не существует и континуума.

15.4.4 (Клоп). Практически решено в указании.

15.4.5. Пусть T = λ + {Ω [0] Z = Ω [1] Ζ | Z замкнут}. Покажем, что
(i) (Якопини) в T недоказуемо Ω [0] = Ω [1]:
заметим, что теория λ + Ω = n: (Zero n) x (y: x y)
непротиворечива из-за легкости Ω и при этом содержит в себе T,
но без аксиомы η недоказуемо равенство x = y: x y;
(ii) если T' = T + (Ω (x: Ω [0] x) = T) + (Ω (x: Ω [1] x) = F),
то T' непротиворечива, а T'ω противоречива:
в T'ω из дополнительных аксиом T следует Ω [0] = Ω [1],
а дополнительные аксиомы T' приведут к T = F, но T # F,
непротиворечивость же T' никому нахуй не сдалась.

15.4.6-15.4.10. Дальше совсем скучно.
В предыдущей серии были упр. 6.8.1-6.8.12. Сейчас будет вторая половина.

6.8.13. Покажем, что цифровая система d адекватна тогда и только тогда, когда
существуют такие Md и Nd, что Md [n] = dn и Nd dn = [n] для всех n:
(=>) Md = Y (f, n: (Zero n) d0 (Sd+ (f (P- n)))), Nd = Y (f, n: (Zerod n) [0] (S+ (f (Pd- n))));
(<=) Pd- = n: Md (P- (Nd n)).
Отсюда получим, что для адекватных цифровых систем d и d'
существуют M и N, что M dn = dn' и N dn' = dn:
возьмем M = n: Md' (Nd n) и N = n: Md (Nd' n).

6.8.14 (Клоп). Покажем, что M = N N~25, где
N = abcdefghijklmnopqstuvwxyzr: r (thisisafixedpointcombinator),
является комбинатором неподвижной точки:
заметим, что M = r: r (M r) = r: r (r (M r)) = ..., и уже все понятно,
но все-таки проверим по теореме о магической силе S I:
(y, f: f (y f)) (r: r (M r) = f: f ((r: r (M r)) f) = f: f (f (M f)) = M.

6.8.15. Упражнение задом наперед:
(iii) нерекурсивные функции - это иллюзия;
(ii) для рекурсивной функции f: N^2 -> N построим попарно различные замкнутые термы X0, X1,..., такие, что Xn Xm = Xf(n, m):
сначала воспользуемся лямбда-определимостью f и построим такой F, что
F [n] [m] = [f(n, m)], предположим Xi = x: x A [n], тогда
Xn Xm = Xm A [n] = (x: x A [m]) A [n] = A A [m] [n], а нам надо, чтобы было
A A [m] [n] = x: x A (F [n] [m]) => A = a, m, n: (x: x a (F n m)), при этом
Xn = Xm => Xn K = Xm K => [n] = [m], то есть термы Xi действительно разные;
(i) для произвольного конечного множества X = {x1,..., xn} с бинарной операцией * на X, покажем, что
Xi Xj = Xk <=> xi * xj = xk для всех i, j, k <= n:
заметим, что Xi Xj = Xk <=> k = f(i, j), и теперь
достаточно представить операцию * функцией f,
тогда xi * xj = xk <=> k = f(i, j).

6.8.16. Строить псевдоцифровую систему на неразрешимых термах - дело неблагодарное, так как при переходе от λ к H она схлопывается, как мыльный пузырь.

6.8.17 (Б. Фридман). Покажем, что f - адекватная цифровая система, если
f0 = x: K, Sf+ = x, y: y x, Pf- = x: x I и Zerof = x, y, z: x (t: F) y z:
Sf+ fn = y: y fn # fn, иначе (y: y fn) (K M) = fn (K M) => M = K,
Zerof f0 = y, z: f0 (t: F) y z = (x: K) (t: F) = T;
Zerof (Sf+ fn) = y, z: Sf+ fn (t: F) y z = y, z: (t: F) fn y z = F;
Pf- (Sf+ fn) = Sf+ fn I = I fn = fn.

6.8.18 (Ершов). Ой, ну его.

6.8.19. Покажем, что перед нами адекватные цифровые системы:
(i) (Ван дер Поль и др.) последовательность pn = x, y: x y~n:
Sp+ (x, y: x y~n) = x, y: x y~n y = x, y: Sp+ x y y = Y (f, x, y: f x y y);
(ii) (Бем, Дедзани-Чанкальини)
d0 = Y, Sd+ = x, y: y x P для любого P:
Pd- = x: x K => Pd- (Sd+ dn) = Sd+ dn K = K dn P = dn,
Zerod = x: x (K (K T)) I =>
Zerod d0 = Y (K (K T)) I = K (K T) (...) I = K T I = T и
Zerod (Sd+ dn) = Sd+ dn (K (K T)) I = K (K T) dn P I = K T P I = T I = F;
e0 = K, Se+ = x, y: y x Y:
Se+ en K = K en Y = en, поэтому годится тот же
Pe- = Pd- = x: x K,
Se+ en (K (K T)) I = K (K T) en Y I = T I = F, но
e0 (K (K T)) I = K (K (K T)) I = K (K T), поэтому придется взять другой
Zeroe = x: x (K (K T)) I I F;
комбинаторы неподвижной точки не имеют нормальной формы,
поэтому адекватная цифровая система не обязательно нормальна.

6.8.20-6.8.22. Ну и хватит уже цифровых систем.

6.8.23 (Дж. Терлаув). Теорема Скотта без использования второй теоремы о неподвижной точке уже практически доказана в указании к этому упражнению.

6.8.24. Покажем, что G X = G (F (G X)), если X = Y (x: F (G x)):
X = (x: F (G x)) X = F (G (X)) => G X = G (F (G X)).
После небольшого отступления к четвертой главе, вернемся к плану "Как читать Барендрегта". Итак, вторая часть, глава шестая. Она содержит довольно много упражнений, поэтому сейчас будет только половина.

6.8.1. Докажем, что <M1,..., Mn> = <N1,..., Nn> <=> M1 = N1,..., Mn = Nn:
(=>) <M1,..., Mn> (x1,..,xn: xi) = <N1,..., Nn> (x1,..,xn: xi) => Mi = Ni;
(<=) x = x => x M1 ... Mn = x N1 ... Nn => x: x M1 ... Mn = x: x N1 ... Nn.

6.8.2. Построим замкнутые термы K8 и A, такие, что:
(i) K8 x = K8:
K8 = y: K8 = (f, y: f) K8 = Y (f, y: f);
(ii) A x = x A:
A = y: y A = (f, y: y f) A = Y (f, y: y f).

6.8.3. Покажем, что для построенного K8 имеет место K # K8:
K = K8 => K M I = K8 M I => M = K8.

6.8.4. Поздоровавшись с LISP, построим замкнутые термы M и N, такие что
(i) M [n] x y = x y~n для всех n:
заметив, что M [n + 1] x y = x y~n+1 = (x y~n) y = (M [n] x y) y,
получаем M = Y (f, n, x, y: (Zero n) x ((f (P- n) x y) y));
(ii) N [n] [i] = x: x F~i T для i < n и N [n] [n] = x: x F~n:
введем сначала G [n] [i] = i < n ? T : F, взяв
G = Y (f, n, i: (Zero n) F ((Zero i) T (f (P- n) (P- i)))),
а потом используем M и G, чтобы определить
N = n, i: (G n i) (y, x: M [i] x F) (y, x: (M [i] x F) T).

6.8.5. Построим последовательность термов A0, A1..., такую, что
A0 = S и An+1 = An An+2:
для этого возьмем An = A [n], где
A [n] = n = 0 ? S : (A [n - 1]) (A [n + 1]), то есть
A = Y (a, n: (Zero n) S ((a (P- n)) (a (S+ n))).

6.8.6 (Россер). Все интернеты уже сто лет дрочат на то, как работают сложение, умножение и показательная функция для цифр Черча.

6.8.7. Пропустим супер-пупер-обобщение теорем о неподвижной точке.

6.8.8. Покажем, что для любого терма M существует такой M' в нормальной форме, что M' I = M:
построим сначала N, заменив в M каждый редекс (yi: Pi) Qi на x (yi: Pi) Qi,
тогда M' = x: N не будет содержать редексов, но при этом M' I ->> M.

6.8.9. В HP-полном расширении λ все комбинаторы неподвижной точки равны, поэтому утверждения
(i) Y_M = Y_N => M = N и
(ii) Ym = Yn => m = n
там не имеют места в общем случае, так что не будем забивать голову.

6.8.10. Покажем, что существует такой M, что M = [M]:
[M] = M => I [M] = M, а по второй теореме о неподвижной точке
можно взять M = W [W], где W = x: I (Ap x (Num x)).

6.8.11 (Черч). Покажем, что множество {M | M = I} не рекурсивно:
данное множество содержит I, но не содержит K, поэтому оно нетривиально,
при этом оно по определению замкнуто относительно равенства,
а мы уже знаем, что множества с двумя этими свойствами не рекурсивны.

6.8.12. Эффективно неотделимые множества определены за пределами монографии (см. "Теория рекурсивных функций и эффективная вычислимость" Роджерса, с. 126).

Продолжение следует...
Немного отклонюсь от плана "Как читать Барендрегта" и от третьей главы монографии внезапно перейду аж сразу к четвертой. Внимание: будут ссылки на упражнения второй главы.

4.3.1. См. упр. 2.4.12 (i).

4.3.2 (Виссер). Замкнутый терм M называется легким, если для всех замкнутых термов N теория λ + (M = N) непротиворечива. В предположении легкости терма M докажем следующие утверждения.
(i) M N легкий для любого замкнутого терма N:
в непротиворечивой λ + (M = K M) выводимо M N = K M N => M N = M,
откуда следует, что λ + (M N = Q) непротиворечива для любого замкнутого Q;
(ii) M неразрешим, иначе бы M N1 ... Nn = I для некоторых Ni,
а из (i) следовало бы, что λ + (I = K) непротиворечива, но I # K (упр. 2.4.2 (i));
(iii)-(iv) если функция f(n) = #Pn рекурсивна, то она представима некоторым лямбда-термом F, таким, что F [n] = Pn, и
тогда в непротиворечивой λ + (M = F) выводимы M [n] = F [n] => M [n] = Pn для всех n;
если же f(i) не является рекурсивной функцией, то я в эти игры не играю, потому что не считаю вопрос "Есть ли Б-г на Марсе?" уместным в этой теме.
(v) λ + {M = N | M и N легкие} непротиворечива:
мы уже знаем о непротиворечивости осмысленной теории H, которая приравнивает все неразрешимые термы, а в пунтке (ii) мы доказали, что все легкие термы неразрешимы.

4.3.3. Модельные соображения не включены в программу намеренно.

4.3.4. Покажем, что не существует такого M, чтобы для любых N теория H + (M = N) была непротиворечивой:
в 4.3.2 (ii) мы доказали, что M должен быть неразрешимым, но
в H все неразрешимые термы приравнены к W3 = (x: x x x) (x: x x x), а
из упр. 2.4.12 (ii) мы знаем, что I # W3.
Вчера были упражнения ко второй главе монографии, а сегодня пробежка галопом по третьей.

3.5.1. Нарисовать графы G(M) для каких угодно термов каждый может и сам.

3.5.2. А вот найти термы по заданному бета-графу - это уже интересно:
(i) M1 -> ... -> Mn -> M1 для произвольного n:
M1 = N N~n, где N = x1,..., xn: xn ... x2 x1 x1;
(ii) чтобы добавить к (i) Mi -> Mi для всех i, возьмем M1 Ω;
(iii) чтобы добавить к (i) Mi -> I для всех i, возьмем (x: I) M1;
второй граф имеет терм (x: x ω (y: x y)) ω -> Ω (y: ω y) -> Ω ω, Ω (y: ω y) -> Ω (y: ω y), Ω ω -> Ω ω;
третий граф имеет терм K I Ω -> (x: I) Ω -> I, K I Ω -> Κ Ι Ω, (x: I) Ω -> (x: I) Ω;
(iv) чтобы сделать бесконечный цилиндр из (i), возьмем M1 ((x: x x x) (x: x x x)).

3.5.3. Построим терм M0, такой, что M0 ->>β M1 ->η M2 ->>β M3 ->η M4 ->>β ...:
M0 = x: (y: M) x x ->>β x: M x ->η M ->>β Μ0;
M найдем, как будто мы до сих пор никогда не слышали про Y:
M = (f, x: (y: f) x x) M, M = W W, W = w: (f, x: (y: f) x x) (w w).

3.5.4. Пусть M = (b, x, z: z ( b b x)) (b, x, z: z (b b x)) x. Чтобы получить кайф, построив G(M) и установив, что для каждого n этот граф имеет n-мерный куб в качестве подграфа, нужно сначала покурить каннабис на родине автора.

3.5.5 (Бем). Бем не обидится, если не все будут рисовать G(M).

3.5.6 (Виссер). (i) Это мое самое любимое упражнение. Покажем, что имеется единственный редекс R с одной вершиной в G(R).
Если R = (x: M) N, то M[x := N] = (x: M) N. Рассмотрим все случаи:
1) x не входит в M => M = R => R = (x: R) N - это не терм;
2) M = x => x[x := N] = R => N = R => R = (x: x) R - это не терм;
3) M = P Q;
4) M = y: M' => R = y: M'[x := N] - это не редекс.
Значит, R = (x: P Q) N =
= (P Q)[x := N] = P[x := N] Q[x := N] = (x: P Q) N => P[x := N] = x: P Q и Q[x := N] = N;
Рассмотрим все случаи для P:
1) x не входит в P => P = (x: P Q) - это не терм;
2) P = x => N = x: x Q;
3) P = y: P', но тогда в R было бы два редекса, а не один;
4) P = P1 P2 => P[x := N] = P1[x := N] P2[x := N] - это аппликация, а не абстракция.
Значит, R = (x: x Q) (x: x Q) -> (x: x Q) Q[x := x: x Q] => Q[x := N] = x: x Q.
Рассмотрим все случаи для Q:
1) x не входит в Q => Q = x: x Q - это не терм;
2) Q = x;
3) Q = Q1 Q2 => Q1[x := N] Q2[x := N] - это аппликация, а не абстракция;
4) Q = y: Q' => y: Q'[x := N] = x: x Q => Q'[x := N] = y Q, но тогда x не входит в Q.
Таким образом, R = (x: x x) (x: x x).
(ii) А вот это не самое любимое мое упражнение.

3.5.7-3.5.10. Бла-бла-бла про хитровытраханные графы и понятия редукции.
Может быть, они и полезные упражнения, но я иду дальше.

3.5.11. Будем писать M ^ N, если L ->> M и L ->> N для некоторого терма L. Докажем, что
(i) K I K ^ K I S: возьмем K (K I S) K;
(ii) (x: a x) b ^ (y: y b) a: возьмем (y: (x: y x) b) a;
(iii) (x: x c) c ^ (x: x x) c: возьмем (y: (x: x y) y) c;
(iv) (x: b x) c ^ (x: x) b c: возьмем (y, x: y x) b c;
(v) (x: b x (b x)) c ^ (x: x x) (b c): возьмем (z, y: (x: x x) (z y)) b c;
(vi) (x: b x) c ^ (x: x) (b c): возьмем I ((y, x: y x) b c);
(vii)* (Плоткин) ...ах, если бы я смог доказать, что не имеет места (x: b x (b c)) c ^ (x: x x) (b c), то я бы прочувствовал, что бета-редукция не обладает "перевернутым свойством CR".

3.5.12-3.5.15. Дальше в редукционные дебри углубляться не буду.
Я решил пробежаться еще раз по плану "Как читать Барендрегта". По дороге буду срать в вашу френд-ленту следующим содержимым. (Чтобы не переключаться все время еще и на греческую раскладку, воспользуюсь синтаксисом, похожим на MLC.)

2.4.1. Покажем, что следующие термы имеют нормальную форму:
(i) (y: y y y) ((a, b: a) I (S S)) = (y: y y y) I = I I I = I;
(ii) (y, z: z y) ((x: x x x) (x: x x x)) (w: I) = (w: I) ((x: x x x) (x: x x x)) = I;
(iii) S S S S S S S = S S (S S S S S) = S S (S S (S S S)), если заметить S S M S = S S (M S);
(iv)* S (S S) (S S) (S S) S S... сдаюсь без калькулятора.

2.4.2. Покажем, что следующие пары термов несравнимы:
(i) I # K, иначе I I M = K I M => M = I;
(ii) I # S, иначе I K M I = S K M I => K M I = K I (M I) => M = I;
(iii) x y # x x, иначе x, y: x y = x, y: x x => (x, y: x y) I M = (x, y: x x) I M => M = I.

2.4.3. Построим замкнутые термы M0, M1..., такие, что Mi # Mj для всех i != j:
Mi = x0, x1,..., xi: xi;
Mi = Mj, i > j => Mi y1 ... yj = Mj y1 ... yj => Mk = I, k = i - j;
Mk = I => Mk I ...(k-1)... I = I I ...(k-1)... I => x: I = I => (x: I) M = I M => I = M.

2.4.4. Покажем, что аппликация не ассоциативна, точнее x (y z) # (x y) z:
x (y z) = (x y) z => x, y, z: x (y z) = x, y, z: (x y) z => K (I M) I = (K I) M I => M = I.

2.4.5 (К. Е. Шаап). Пусть X = S I. Покажем, что X X X X = X (X (X X)), и вообще для всех n имеет место X^n X = X X~n:
n = 1: X X = X X;
n = 2: X X X = S I X X = I X (X X) = X (X X).
n > 2: X^n X = X X~n =>
X X~n+1 = X X~n X = (X^n X) X = X (X^n-1 X) X =
= S I (X^n-1 X) X = X ((X^n-1 X) X) = X (X X~n-1 X) =
= X (X X~n) = X (X^n X) = X^n+1 X.

2.4.6. Покажем, что не существует такого F, чтобы для любых M и N выполнялось бы F (M N) = M:
I I = (x: I) I => F (I I) = F ((x: I) I) => I = x: I => I M = (x: I) M => M = I.

2.4.7. Покажем, что существует такой M, что для любого N выполняется M N = M M, применив теорему о неподвижной точке:
M x = M M => M = x: M M => M = (f, x: f f) M;
M = W W, W = w: (f, x: f f) (w w);
M N = (f, x: f f) M N = (x: M M) N = M M.

2.4.8. Бла-бла-бла про одновременную подстановку.
В пизду эту болтологическую муть.

2.4.9. Покажем, что (x, y: M) N = y: (x: M) N:
(x, y: M) N = (y: M)[x := N] = y: M[x := N] = y: (x: M) N.

2.4.10. Используем теорему о неподвижной точке, чтобы построить терм M, такой, что
(i) M = M S:
M = (f: f S) M, M = W W, W = w: (f: f S) (w w);
M = (f: f S) M = M S;
(ii) M I S S = M S:
M = (f, s: f I s s) M, M = W W, W = w: (f, s: f I s s) (w w);
M S = (f, s: f I s s) M S = M I S S.

2.4.11. Построим F, такой, что F I = x и F K = y, вспомнив упражнение 2.4.2 (i):
если F = f: f I M N, тогда
F K = K I M N = N => N = y;
F I = I I M N = M N => M = z: x;
cтало быть, F = f: f I (z: x) y.

2.4.12 (Якопини). Пусть w3 = x: x x x и W3 = w3 w3. Покажем, что
(i) I # w3, иначе I (x, y: I) = w3 (x, y: I) => x, y: I = I => (x, y: I) I M = I I M => I = M;
(ii) I # W3, иначе I = W3 => I w3 = W3 w3 => w3 = W3 w3, а если заметить
W3 = w3 w3 w3 = W3 w3, то W3 = I => I = I w3, что возвращает нас к пункту (i).

2.4.13. Покажем, что для любой абстракции M имеет место равенство x: M x = M:
M = y: N;
x: M x = x: (y: N) x = x: N[y := x] = y: N = M.

2.4.14. Пусть M = x: x (y: y y) (y: y y). Покажем, что M I-разрешим:
M (x, y: x I (y I)) = I I (I I) = I.

2.4.15 (почему-то есть только в оригинале, Минц не перевел). Suppose a symbol of the lambda calculus alphabet is always 0.5 cm wide. Let us write down a lambda term with length less than 20 cm having a normal form with length at least 10^(10^10) lightyear. The speed of light is c = 3 * 10^10 cm/sec.
The length of a Church numeral in cm is about the natural number it represents, so it is more than enough to write a term that reduces to the Church numeral for the number 2^(2^(2^(2^(2^2)))). The exponential function for Church numerals is just application, so the term can be (x: x x x x x x) (f, x: f (f x)) which is, in turn, much shorter than requested.
В связи с идеей распределенных сетей взаимодействия, хотелось бы вернуться к проекту компилятора inet, который используется в MLC для механизма read-back. Приложение было реализовано уже после подготовки формального описания проекта и строго следуя проектной документации; имели место лишь мелкие уточнения и исправления по ходу работы.

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

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

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

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

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

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

Наброски )
Кто может скорректировать шестнадцатеричное число?

 A 0 0 B 

Задействуйте свои проверочные колбочки!
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.
module brain (clk, sensor, effect);
	parameter nbit = 12;
	parameter size = 2 ** nbit;
 
	input clk;
	input [7:0] sensor;
	output [7:0] effect;
 
	reg sig [0:size - 1];
	reg trace [0:size - 1];
	reg [nbit - 1:0] ram [0:size - 1];
 
	assign effect[3:0] = {sig[3], sig[2], sig[1], sig[0]};
	assign effect[7:4] = {sig[7], sig[6], sig[5], sig[4]};
 
	integer i;
 
	initial for (i = 0; i < size; i = i + 1) begin
		trace[i] = 0;
		sig[i] = 0;
		ram[i] = i;
	end
 
	always @(posedge clk) begin
		for (i = 0; i < 8; i = i + 1)
			sig[ram[i]] <= sensor[i];
 
		for (i = 0; i < size; i = i + 1) begin
			case ({trace[i], sig[ram[i]]})
			2'b00: ram[i] <= ram[i] + 1;
			2'b01: sig[i] <= 1;
			2'b10: sig[i] <= 0;
			2'b11: ram[i] <= ram[i] - 1;
			endcase
 
			trace[i] <= sig[ram[i]];
		end
	end
endmodule
 
`ifdef SIM
module sim;
	reg clk = 0;
	reg [7:0] key;
	wire [7:0] led;
 
	brain core(clk, key, led);
 
	integer c;
 
	always begin
		c = $fgetc(32'h8000_0000);
		if (-1 == c)
			$finish;
 
		key = c[7:0];
		#1 clk = ~clk;
		#1 clk = ~clk;
		$displayb(led);
	end
endmodule
`endif
`define OPZ 4'b1111
`define OPA 4'b0001
`define OPL 4'b0010
`define OPN 4'b0100
`define OPS 4'b1000

`define BIT 15
`define SIZE (2 ** `BIT)

module ram0 (clk, op, led);
	input clk;
	input [3:0] op;
	output [7:0] led;

	reg [`BIT - 1:0] ram [0:`SIZE - 1];
	reg [`BIT - 1:0] n, z;

	assign led = z[7:0];

	always @(posedge clk) begin
		case (op)
		`OPZ: z = 0;
		`OPA: z = z + 1;
		`OPL: z = ram[z];
		`OPN: n = z;
		`OPS: ram[n] = z;
		endcase
	end
endmodule

`ifdef SIM
module sim;
	reg clk = 0;
	reg [3:0] op;
	wire [7:0] led;

	ram0 core(clk, op, led);

	integer ch;

	always begin
		ch = $fgetc(32'h8000_0000);
		case (ch)
		"z", "Z": op = `OPZ;
		"a", "A": op = `OPA;
		"l", "L": op = `OPL;
		"n", "N": op = `OPN;
		"s", "S": op = `OPS;
		-1: $finish;
		default: op = 0;
		endcase

		if (op) begin
			#1 clk = ~clk;
			#1 clk = ~clk;
			$displayb(led);
		end
	end
endmodule
`endif

Profile

Anton Salikhmetov

November 2018

S M T W T F S
    123
45678 910
11121314151617
18192021222324
252627282930 

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 3rd, 2025 05:52 pm
Powered by Dreamwidth Studios