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.
Я тут задумался об обратимых вычислениях. Как они могли бы выглядеть в сетях взаимодействия? Но прежде всего, в каком смысле надо понимать обратимость, если отношение редукции обладает свойством ромба? И что из этого будет следовать?

Пока у меня ничего толком не устоялось, рабочее определение обратимой системы взаимодействия такое: 1) для любой подсети Ν должно быть не более одной активной пары α><β, которая редуцируется к N, и 2) если две подсети M и N - результы взаимодействия активных пар α><β и γ><δ, соответственно, то M и N не пересекаются. Речь идет лишь о подсетях и активных парах, так как об обратимости конфигураций говорить нельзя, когда в сети больше одной активной пары. Не уверен, что это исчерпывающий список условий, но уже их достаточно, чтобы заметить пару-тройку следствий.

Одно из следствий такого определения немедленно накладывает ограничения на правила взаимодействия. В частности, правая часть каждого правила обязана быть связной сетью. Доказательство от противного: строим простой контрпример с двумя одинаковыми активными парами, взаимодействие которых приводит к двум неразличимым сверткам для каждой активной пары, нарушая условие (2). Также потребуется асимметрия правой части правила для α><β, если α и β различны. Продолжу думать в этом направлении позже, хотя уже предчувствую трудности с интерпретацией обратимых систем взаимодействия в исчислении взаимодействия. Например, придется как-то выкручиваться с разыменованием (indirection), применение которого сугубо неоднозначно.

Но самое интересное свойство обратимых систем взаимодействия - это, наверное, обратное свойство ромба. Получается, если такие системы вообще существуют, они одновременно будут обладать и прямым (strong confluence), и обратным (strong upward confluence) свойствами ромба. Это, конечно, мне напомнило об упражнении 3.5.11 (vii) у Барендрегта. Когда я бегло проходил по упражнениям к нескольким главам три года назад, мне не удалось быстро его решить. Было обидно.

Задача была показать, что для термов (λx.b x (b c)) c и (λx.x x) (b c), принадлежащих Плоткину, не существует общей β-экспансии, хотя они оба редуцируются к b c (b c). Эти два терма служат контрпримером для "обратного свойства Черча-Россера" β-редукции. Сегодня я решил поискать, как именно выводить противоречие из существования их общей β-экспансии, и нашел "An Easy Expansion Exercise" (Vincent van Oostrom). Там предлагается использовать теорему о стандартизации. Правда, я не очень понял, как ограничиться материалом конкретно третьей главы.

Update. In a reversible interaction system (RIS), the right-hand side (RHS) of each rule needs to include at least one agent, that is RHS cannot be a wiring: RHS of α[x, x]><β is ambiguous, α[x]><α[x] violates condition (1) in the definition of RIS, and more than one wire make a disconnected net, violating condition (2). As a consequence, in the interaction calculus, each name in an interaction rule needs to have at least one of its two occurrences in a term that is not a name; otherwise we have a disconnected subnet in its RHS. Now it is easy to see strong upward confluence in RIS.
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
$ 

Most Popular Tags

Syndicate

RSS Atom

November 2018

S M T W T F S
    123
45678 910
11121314151617
18192021222324
252627282930 
Powered by Dreamwidth Studios