Коиндукция и актуальная бесконечность

[Vantus]

Someone в сообщении #1227727 писал(а):

(Vantus)

По-моему, я о Вас лично ни одного слова не сказал. Я просто хотел сказать, что учёные степени и звания не гарантируют компетентности. Но Вы же сами о них заговорили.

(Оффтоп)

Вот вы, например, всяко похвалялись в той ветке про странного дфмн, я прочитал. А актуальная бесконечность - вполне реальная вещь, я уже упомянул коданные - то бишь абстракцию стримов разных ЯП, например std::basic_ostream. Это бесконечные последовательности, которые, по сути своей, доступны не с начала, а с дальнего конца.

[Vantus]

arseniiv в сообщении #1227743 писал(а):

Vantus
Вот вы тут какую-то ерунду про связь коданных, актуальной бесконечности и пересчёта бесконечной последовательности с её конца пишете, честно. Первое и третье никак не связаны, второе вообще не термин, и третье непонятно что должно означать вычислительно. Можете привести источник, где было бы про пересчёт с другого конца?

Видна прям надменность естественника))) Но я отвергну алгебраическую гнусь и начну с простого примера.
Вот у вас есть обычный поток символов в обычном C++. Вот скажите, как вы с ним работаете? Его начало все время идет от вас, конца у него в принципе нет. Вот есть обычная строчка в обычном С++. У нее все с точностью наоборот - у нее есть начало и конец и вы проходите ее от начала до конца. Согласны?

[Vantus]

arseniiv в сообщении #1227743 писал(а):

Vantus
Вот вы тут какую-то ерунду про связь коданных, актуальной бесконечности и пересчёта бесконечной последовательности с её конца пишете, честно.

Пересчет, кстати, не обязательно обязан означать "присвоение натуральных номеров". Эта затея ничем хорошим не закончится. Я лично полагал, что всем понятно, что разумеется итерирование (то бишь использование итераторов). Кажется, что с "ерундой" вы погорячились.

[Vantus]

arseniiv в сообщении #1227753 писал(а):

Vantus
Можете отбросить введения, я в курсе того, что такое поток в смысле data Stream a = Cons a (Stream a). Давайте дальше. В обратном порядке было бы очень интересно. (Но если у вас есть ссылка, вам не нужно даже утруждать себя пересказом. Она ведь есть, так?)

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

arseniiv в сообщении #1227753 писал(а):

Vantus в сообщении #1227749 писал(а):

Пересчет, кстати, не обязательно обязан означать "присвоение натуральных номеров". Эта затея ничем хорошим не закончится. Я лично полагал, что всем понятно, что разумеется итерирование (то бишь использование итераторов).

Всё же итераторы не могут перечислять бесконечную последовательность с конца.

Ну, проитерировать циклом - не сможете (так как у вас нет начала, откуда итерировать), а конструкцией функциональных языков типа Map[function, stream] - отчего нет, если б существовал такой компьютер, где помещались бы бесконечные стримы.

[arseniiv]

Vantus в сообщении #1227757 писал(а):

Ну, проитерировать циклом - не сможете (так как у вас нет начала, откуда итерировать), а конструкцией функциональных языков типа Map[function, stream] - отчего нет, если б существовал такой компьютер, где помещались бы бесконечные стримы.

По-моему, вы всё же не разбираетесь в том, о чём говорите. Давайте вы дадите ссылку и разойдёмся на том до окончания её анализа.

[Vantus]

arseniiv в сообщении #1227761 писал(а):

Vantus в сообщении #1227757 писал(а):

Ну, проитерировать циклом - не сможете (так как у вас нет начала, откуда итерировать), а конструкцией функциональных языков типа Map[function, stream] - отчего нет, если б существовал такой компьютер, где помещались бы бесконечные стримы.

По-моему, вы всё же не разбираетесь в том, о чём говорите. Давайте вы дадите ссылку и разойдёмся на том до окончания её анализа.

Я думаю, что разбираюсь существенно лучше вашего, ибо 12 лет проработал программистом. Нельзя сказать, чтоб я был этому рад, но с тех пор я вполне хорошо пишу свои классы генераторов для своих нужд, как и реализации map. Но если вы мне все время намекаете, что я идиот, зачем вам моя ссылка? Как кажется, вы уже решили, кто прав.

[arseniiv]

Я ничего не решал. Просто вы так и не ответили, какое отношение map имеет к итерации с конца бесконечной последовательности.

[Vantus]

Вот статья The Church-Scott representation of inductive and coinductive data. Я лично начинал разбираться с нее. Хотя, неясно, что это может сказать людям, заранее считающими себя правыми, но выражения в этой статье типа

$$\lambda n.\mathrm{CoIt}(\lambda x.x)\mathrm{Succ} n$$

и есть бесконечный ряд, записанный "с другого конца".

-- 21.06.2017, 01:24 --

Хотя, с map, for_each и т.д., я, возможно, и не прав. Мои реализации все были довольно низкого уровня, когда никакого стрима уже не было, как я поглядел, и на деле там просто итерировалась в отдельном потоке строчка. И по каждому добавлению символа в стрим вызывался этот поток и дообрабатывал добавленный символ. Да, чудес не бывает. Но давно было и я уверовал, что это не так работает, а мистически.

[arseniiv]

Vantus в сообщении #1227774 писал(а):

Хотя, неясно, что это может сказать людям, заранее считающими себя правыми

Ну, это же к вам относится, а не ко мне. Понимаете, если человек говорит, что map для потока не эквивалентно циклу с соответствующим итератором, и что там где-то может вестись перебор откуда-то из бесконечности к началу — это совершенно не «заранее». Это «по веской причине».

Статью посмотрю, спасибо.

[arseniiv]

В статье достаточно опечаток, но можно видеть, что

Vantus в сообщении #1227774 писал(а):

$$\lambda n.\mathrm{CoIt}(\lambda x.x)\mathrm{Succ} n$$

— это вовсе не

Vantus в сообщении #1227774 писал(а):

есть бесконечный ряд, записанный "с другого конца"

Это просто функция, которая по числу $n$ строит поток $[n,n+1,n+2,\ldots]$. Никакого другого конца тут не видно, это банальная конструкция потока.

[Vantus]

Но, поскольку мне от лямбда-исчисления, теории категории и подобного злогна хочется немедленно оправиться, изгоним его и упростим, ибо еллинское это все бесование. Вот есть пример с сайта питона
def firstn(n):
... num = 1
... while num < n:
... ... yield num
... ... num += 1

Это есть простейший генератор, который выдает последовательность

$$1,\dots, N$$

при вызове firstn(N). При этом он не генерирует список, как можно было подумать, а при каждом обращении вычисяет 1, 1+1, 1+2 и т.п.

Вот пример, тождественный вышенаписанной мною ламбда-категорной абракадабре
def generator(first):
... def wrap(func):
... ... def seq():
... ... ... x = first
... ... ... while True:
... ... ... ... yield x
... ... ... ... x = func(x)
... ... return seq
... return wrap

for i in generator(0)(lambda x: x + 1)():
... print(i)

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

Теперь по map и по циклам. С точки зрения реализации - это одно и то же, но с точки зрения языка - нет, нет, и еще раз нет. Откройте свои учебники по отвратительной теории категорий и узрите, что это принципиально разные вещи.

-- 21.06.2017, 03:16 --

Цитата:

Никакого другого конца тут не видно, это банальная конструкция потока.

Интересно, а какой другой "другой конец" вы хотите увидеть?! Эта штуковина сама по себе является "концом потока". Я ж говорю о generator(0)(lambda x: x + 1)(), а не о том, что он выдает.

-- 21.06.2017, 03:21 --

Или вы ждали, что в конце будут кардинальные числа? Упаси меня Б-г от такой скверны, как кардинальные числа в моем компьютере! Он этого не переживет и я ничего такого в виду не имел.

-- 21.06.2017, 03:38 --

Люди, неужто вы не видите разницы между
def generator(first):
... def wrap(func):
... ... def seq():
... ... ... x = first
... ... ... while True:
... ... ... ... yield x
... ... x = func(x)
... return seq
return wrap

for i in generator(0)(lambda x: x + 1)():
... print(i)

и
x = 0
while True:
... print(x)
... x = x + 1

Неужто отвращение к философии мешает видеть принципиальную разницу между имеющим актуальное бытие generator(0)(lambda x: x + 1)() и последовательно исполняющимся бесконечным циклом, который лишь потенциально бесконечен???

[arseniiv]

Vantus в сообщении #1227787 писал(а):

Вот пример, тождественный вышенаписанной мною ламбда-категорной абракадабре

Используется синтаксис Python

def generator(first):
    def wrap(func):
        def seq():
            x = first
            while True:
                yield x
                x = func(x)
        return seq
    return wrap

for i in generator(0)(lambda x: x + 1)():
    print(i)

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

Стоит признать, что код делает то, что сказано, да и актуальную бесконечность оставим на вашей совести, а вот где отсчёт с конца? Жду его, жду, знаете ли, а он всё не приходит и не приходит.

Vantus в сообщении #1227787 писал(а):

но с точки зрения языка - нет, нет, и еще раз нет

Ну хорошо, sequence_ . map ac, где ac :: a -> IO () (синтаксис хаскеля) — уж точно for.

Vantus в сообщении #1227787 писал(а):

Интересно, а какой другой другой конец вы хотите увидеть?! Эта штуковина сама по себе является "концом потока".

Странная семантика. Это функция, выдающая поток по двум параметрам. Зачем звать её «концом» или там «началом»?

Vantus в сообщении #1227787 писал(а):

Или вы ждали, что в конце будут кардинальные числа?

Нет, конечно. Тут говорили что-то об итерации из бесконечности в начало, вот я и ждал её такую непостижимую, и уж, разумеется, не пытался угадать, подставляя всё подряд, кардинальные ли числа, ординальные ли…

Теперь вернёмся немного в прошлое:

Vantus в сообщении #1227757 писал(а):

Ну, проитерировать циклом - не сможете (так как у вас нет начала, откуда итерировать), а конструкцией функциональных языков типа Map[function, stream] - отчего нет, если б существовал такой компьютер, где помещались бы бесконечные стримы.

Прекрасно ваш стрим и циклом итерируется, и начало, откуда итерировать, там прекрасно присутствует. И это относится не только к коду на Python — у того функционального выражения (точнее, результата применения к нему какого-нибудь числа) тоже «есть начало» (вот оно лежит перед нами, а рядом пара деструкторов, чтобы брать значения и идти дальше).

-- Ср июн 21, 2017 05:52:02 --

Про разницу: ну если ваш цикл оформить, чтобы он вызывал функцию какую, переданную аргументом, и что-нибудь этакое с замыканиями накрутить, уверен, разница может и испариться. А как устроены генераторы, вы наверняка в курсе. Это просто одно-два (уж не помню, сколькими Python обходится) замыкания с общим состоянием, какая уж бесконечность.

[Vantus]

Я обновил. Вы, видимо, неявно отождествляете generator(0)(lambda x: x + 1)() и результат его деятельности (применения к нему числа), что нормально для не-философа. Я полагаю, что это совершенно криво и принципиально неверно. Более того, я утверждаю, что объект лямбда-исчисления до и после application - это невероятно разные сущности. Это как если отождествлять $\sin x \in C^\infty(\mathbb{R})$ и набор точек $\{(x, \sin x)|x\in \mathbb{R}\}$. Одно - элемент функционального пространства со своими свойствами, другое - просто набор точек.

-- 21.06.2017, 04:02 --

arseniiv в сообщении #1227789 писал(а):

Про разницу: ну если ваш цикл оформить, чтобы он вызывал функцию какую, переданную аргументом, и что-нибудь этакое с замыканиями накрутить, уверен, разница может и испариться. А как устроены генераторы, вы наверняка в курсе. Это просто одно-два (уж не помню, сколькими Python обходится) замыкания с общим состоянием, какая уж бесконечность.

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

-- 21.06.2017, 04:07 --

Не, даже не так. $\sin x \in C^\infty(\mathbb{R})$ вы отождествите. А вот $\sin x \in S'(\mathbb{R})$ (из Шварцевского пространства обощенных) - навряд ли (они ведут себя по-разному). А чем generator(0)(lambda x: x + 1)() хуже и за что его надо отождествлять с результатом его работы?

-- 21.06.2017, 04:23 --

Более того, представленная функция сильно отличается от принятых в функциональном анализе, например. Я легко могу помыслить себе, например, $f: \mathbb{N} \rightarrow l^2$, такую что $\|f(N)\|_2<N$. Можно легко показать ее существование. Но наша конструкция, в отличие от обычного обьекта анализа, в качестве значения выдает не готовый бесконечный набор весь сразу, а производит все новые и новые значения, уничтожая предыдущие. Таким образом, это не

Цитата:

Странная семантика. Это функция, выдающая поток по двум параметрам. Зачем звать её «концом» или там «началом»?

а совершенно особый обьект. Он выплевывает все новые и новые числа при использовании, причем если представить числа шариками, то один конец цепочки шариков будет упираться в generator(0)(lambda x: x + 1)(), а второй - в нас, как наблюдателя.

[Karan]

Тема перемещена из форума «Дискуссионные темы (М)» в форум «Computer Science»
Причина переноса: тематика.

[Aritaborian]

Ужас какой. Гвидо-то, поди, не знает, какой жути в своём Питоне наворотил. Видимо, скоро придёт к нему во сне Актуальная Бесконечность и гремя цепями и шевеля тентаклями спросит: «Зачем ты меня реализовал?»
Vantus, вы так и не показали, где тут «отсчёт с конца».