Overly algebraic

[thedeemon]

Вот список имеет вид
data List a = Nil | Cons a (List a)
т.е.
F(x) = 1 + x * F(x)
а значит
F(x) - x * F(x) = 1
(1-x) * F(x) = 1
F(x) = 1 / (1-x)
и действительно, если мы такую функцию разложим в ряд, то получим
F(x) = 1 + x + x*x + x*x*x + x*x*x*x + ...
т.е. как раз тип описывает списки из х разной длины.

Но вот что любопытно,
F(F(F(x))) = 1 / (1 - (1 / (1 - 1 / (1 - x)))) = ... = x
можете на бумажке проверить или вот тут увидеть.
Это что же значит, [[[a]]] = a? ;)

Comments

[juan_gandhi]

Какое-то очень странное открытие. До нелепости странное. Как это осознать-то? Что бинарные деревья - это то ли корни многочленов, то ли корни из единицы третьего порядка. Но тут просто абсурд. Что происходит-то? И как понимать это открытие?

А на твитере спросить? Там самые разные люди есть.

[sassa_nf]

Well, if we follow the rabbit hole far enough, we end up with a requirement that may not hold in arbitrary categories?

Eg what is "-x"? If we were to apply algebra directly, it is such a type y such that x+y=0. I think non-trivial types never add up to 0, so "-x" cannot be defined for arbitrary categories.

[juan_gandhi]

See, you don't need negation. All you have is a property of a series, the equation that it satisfies.

[sassa_nf]

I am not certain of that. First you need to ensure that division does not introduce undefined.

Say, F(x)=1+x*F(x) holds for all x, including x=1. Then F(x)-x*F(x)=1 - is this still so for x=1? There are infinities involved, so it's beyond my level of understanding how to do the subtraction in such a way that the difference is 1 (and, say, not 0, and not 2). Maybe not only Ramanujan knows.

Or is (1-x)*F(x)=1? Even for x=1? Why is it ok to divide by (1-x)? Before we get to representation of 1/(1-x) as a series.

[vit_r]

В матричном виде это записать можно?

[deniok]

Можно задать более простой вопрос, какой формальный рад соответствует списку списков F(F(x))?

[juan_gandhi]

1/(1-1/(1-x)) = 1/((1-x-1)/(1-x)) = (x-1)/x = 1-1/x

Трудно сообразить, что это вообще значит. Еще можно понять x^n/n!.

[deniok]

Это не порождает при обратной сборке рекурсивного уравнения, вот в чем беда: 1 + x * F(F(x)) = x.

[migmit]

Хех. Если x=0, то списков [Void] — ровно один, а вот списков [[Void]] — бесконечно много. Поэтому свободный член такого рядо должен быть бесконечным.

[deniok]

Вот-вот.

[chaource]

The series F(x) = 1 + x + x*x + ... converges only for |x| < 1. When we write F(F(x)), we write F(1 + x + x*x + ...). So, the argument of F is 1 + x + x*x + ..., which is not less than 1 if x > 0. So, we cannot interpret F(F(x)) as a power series in x. Similarly for F(F(F(x))). It is not justified to write out a power series in x for this function and to substitute. So, the counterpart of F(F(F(x))) in the type system is not List[List[List[X]]]. It is just X.

[juan_gandhi]

It converges ok in a category with unlimited unions and finite products.

[chaource]

I doubt it. If it converges in that category, you would then have no trouble interpreting [[[x]]] = x.

[juan_gandhi]

Have to figure out. Need a Ramanujan.

[migmit]

Ну, вообще нет (хотя бы по соображениям мощности), но есть вот такие занятные штуки:

A. Blass. Seven trees in one. — множество бинарных деревьев (без дополнительных данных) устроено как T = 1 + T^2, откуда формально T^6 = 1 (очевидный бред) и T^7 = T. Бласс строит биекцию между T^7 и T, которая работает за O(1). Он выдвигает предположение, что это часть более общей схемы.

Marcelo Fiore, Tom Leinster. Objects of Categories as Complex Numbers. — отвечает на вопрос Бласса, доказывая, по сути, следующее: пусть многочлен p с положительными коэффициентами имеет ненулевой свободный член и степень как минимум 2, а многочлены q_1 и q_2, тоже с положительными коэффициентами, имеют степень как минимум 1, и пусть в Z[X] разность q_1(X) - q_2(X) делится на p(X) - X. Тогда в любой дистрибутивной категории из изоморфизма T <-> p(T) получается изоморфизм q_1(T) <-> q_2(T).

[thedeemon]

Про T^7 я помню, видел когда-то. Но про продолжение истории не слышал.