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

[Mental]

(Оффтоп)

Vantus, а вы случаем ТБ не изучали?

[arseniiv]

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

Вы, видимо, неявно отождествляете generator(0)(lambda x: x + 1)() и результат его деятельности

Что значит «результат его деятельности»? Вот есть вот такое выражение, оно вычисляется в объект-итератор, и на этом конец. Если его засунуть в цикл, он начнёт, во-первых, менять своё внутреннее состояние и, во-вторых, выдавать элементы, с которыми тело цикла что-то может делать. Ни там, ни там нет никаких бесконечностей. Код с таким циклом может не завершиться, конечно, но (1) опять нет никаких актуальных бесконечностей, (2) это зависит и от тела цикла, и от того, что выдаёт итератор, а не от одного итератора.

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

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

Вообще о разнице map и for вы первым заговорили, и, честно говоря, непонятно почему. Как-то внезапно. Видимо, чтобы отвлечь внимание от пересчёта с бесконечности, который вы так неудачно упомянули, а просто взять и отказаться от этих слов почему-то не хотите.

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

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

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

Короче, вас очаровали генераторы. Ну так мало ли кого что очаровало, не надо пытаться придать этому смысл, которого у него нет.

-- Ср июн 21, 2017 19:36:38 --

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

[Aritaborian]

arseniiv, можете объяснить мне разницу между map и for, о которой идёт речь? Ибо из сумбура Vantus ничего внятного вычленить не могу, а всё же любопытно. Примеры можно приводить для Wolfram Language, Си/C++, Python, VBA. (В вашем любимом Хаскеле, есличо, я ничего не смыслю.)

[arseniiv]

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

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

ghci> map succ "shift me"
"tijgu!nf"

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

[george66]

Однажды сделал "рекурсию вверх", сейчас попробую объяснить. Пусть у нас есть тип данных $A$. Возьмём тип данных $B=A^{\omega}$ (элементами этого типа будут бесконечные последовательности $<a_0,a_1,a_2\cdots>$ элементов $A$). Предположим, что любая функция $f\colon B\to B$ имеет неподвижную точку. Тогда я докажу, что тип $A$ предполный в смысле Ершова. Это значит, любую функцию из чего угодно в $A$, определённую на полуразрешимом подмножестве, можно продолжить до всюду определённой. Например, так обстоят дела, если $A$ -- тип всех частично рекурсивных функций. Выразим предполноту некоторой формулой. Пусть есть разрешимое множество натуральных чисел, заданное формулой $\varphi(n)$
$\forall n(\varphi(n)\vee\neg\varphi(n))$
Пусть есть некое подмножество $A$, задаваемое формулой $\psi(a)$. Пусть верна формула
$\exists n\varphi(n)\Rightarrow\exists a\psi(a)$
(если верно полуразрешимое условие $\exists n\varphi(n)$, то существует $a$ со свойством $\psi(a)$)
Тогда предполнота означает, что
$\exists a(\exists n\varphi(n)\Rightarrow\psi(a))$
Итого, запишем предполноту одной формулой
$\forall n(\varphi(n)\vee\neg\varphi(n))\wedge(\exists n\varphi(n)\Rightarrow\exists a\psi(a))\Rightarrow\exists a(\exists n\varphi(n)\Rightarrow\psi(a))$
Теперь докажем, что из свойства неподвижной точки для $B$ следует эта формула. Пусть верна посылка
$\forall n(\varphi(n)\vee\neg\varphi(n))\wedge(\exists n\varphi(n)\Rightarrow\exists a\psi(a))$
Для всякого $n$ мы можем проверить, истинно или нет $\varphi(n)$. Если истинно, мы можем найти $a$ со свойством $\psi(a)$. Можно определить функцию $g\colon N\to A$, которая по $n$ находит $a$, причём
$\varphi(n)\Rightarrow\psi(g(n))$ для всех $n$
Дальше определяем функцию $f\colon N\to A$ "рекурсией вверх"
$f(n)=g(n)$, если $\varphi(n)$
$f(n)=f(n+1)$, если $\neg\varphi(n)$
Для числа $n$ она проверяет условие $\varphi(n)$, если оно верно, выдаёт $a$ со свойством $\psi(a)$, а если нет, переходит к проверке числа $n+1$
Берём $f(0)$ и мы доказали заключение предполноты
$\exists n\varphi(n)\Rightarrow \psi(f(0))$
Это всё я выложил на FOM (где модератор Мартин Девис, ему 89 лет, также туда ходит Дана Скотт). Результатом было долгое молчание, после чего все (совершенно невинные) сообщения, что я пытался слать на FOM, отвергают без объяснения причин.

[george66]

И вот я думаю: то ли я написал фигню, то ли старички выжили из ума, одно другому тоже не мешает.

[Someone]

george66 в сообщении #1229019 писал(а):

И вот я думаю: то ли я написал фигню, то ли старички выжили из ума, одно другому тоже не мешает.

george66 в сообщении #1228296 писал(а):

Пусть у нас есть тип данных $A$. Возьмём тип данных $B=A^{\omega}$ (элементами этого типа будут бесконечные последовательности $<a_0,a_1,a_2\cdots>$ элементов $A$). Предположим, что любая функция $f\colon B\to B$ имеет неподвижную точку. Тогда я докажу, что тип $A$ предполный в смысле Ершова.

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

george66 в сообщении #1228296 писал(а):

Это всё я выложил на FOM (где модератор Мартин Девис, ему 89 лет, также туда ходит Дана Скотт). Результатом было долгое молчание, после чего все (совершенно невинные) сообщения, что я пытался слать на FOM, отвергают без объяснения причин.

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