Александр, спасибо за лестный отзыв.
Я рад, что мои писательские труды не были даром. ;-)
Андрей

On Tue, 18 May 2021 at 23:23, Александр Гусев gusev_aleksandr_AT_mail.ru <
refal@botik.ru> wrote:

> Спасибо, Андрей!
> Всё замечательно выражено. Действительно, если даны правильные
> определения, дискутировать становится подчас не о чем.
> Я, конечно, подразумевал именно адресные ссылки, которые наблюдал в языках
> высокого уровня и остался ими недоволен. А вот математически описанные Вами
> ссылки - это отлично, проходит!
>
>
>
> Отправлено из мобильной Почты Mail.ru
>
>
> вторник, 18 мая 2021 г., 23:01 +0300 от refal <refal@botik.ru>:
>
> После семинара между двумя Александрами (Гусевым и Коноваловым) возникла
> переписка с ограничеснной рассылкой только тем, кто был на семинаре. Я
> захотел встрять и посылаю письмо в refal@botik c надеждой, что это
> обсуждение будет интересно всем. Также я указал в BCC тех, кто был на
> семинаре, но на нашу рассылку не подписан, и еще некоторых коллег.
>
> Оба Александра выразили свою нелюбовь к понятию ссылки как к кандидату к
> включению в область данных Рефала. А я выступлю в защиту этого понятия, в
> том числе с математической точки зрения.
>
> Подозреваю, нарушения эквивалентности при наивных преобразованиях в Рефале
> с лямбда-выражениями, о которых на семинаре рассказывал Александр,
> произошло именно потому, что семантика равенства по ссылке, "ссылочного
> равенства", была не до конца осознана. Она действительно нетривиальна.
> Эквивалентные преобразования, по определению, должны сохранять семантику. А
> для этого семантика должна быть понята и сформулирована.
>
>
> *From: Александр Гусев <gusev_aleksa...@mail.ru <gusev_aleksa...@mail.ru>>
> Sent: Monday, May 17, 2021 11:17 PM*
>
> Лично я - противник использования ссылок в Рефале. Оставьте их языкам
> близким к машинному уровню. Здесь же «ссылка» должна быть просто отсылкой к
> функции или объекту, но не адресом. Даже если в низкоуровневой основе это и
> адрес. Это как использование goto в императивных языках понижает качество
> кода. Goto - это для низкоуровневого кода, ассемблера и естественно
> присутствует в любой программе, но на машинном уровне.
>
> *On Tue, 18 May 2021 at 14:53, Александр Коновалов
> <a.v.konovalo...@mail.ru <a.v.konovalo...@mail.ru>> wrote:*
>
> В общем-то я тоже. Поэтому в компиляторе до сих пор нет ссылочных типов
> данных вроде динамических ящиков. Единственные ссылочные данные, которые
> есть — это замыкания и они иммутабельны. В Рефале-2, Рефале Плюс
> и Рефале-6 мутабельные ссылочные данные есть.
>
> Давайте сразу договоримся, что ни о каких адресах речи не идет. Рефал –
> язык высокого уровня, и его (достаточно простая) семантика должна быть
> сформулирована в терминах абстрактного вычислителя. Ссылки – это понятие
> высокого уровня.
>
> Ссылки вызывают у нас протест, на мой взгляд, только потому, что они
> выходят за теоретико-множественный мир значений, привычный из обычной
> научной деятельности, выученной из школы и университетского мат-анализа.
> Пойди наука, математика и логика по-другому (скажем, в другой, неземной
> цивилизации), мы (инопланетяне) считали бы привычные землянам значения
> некоей ограниченной формой данных и информации. Ведь в жизни мы без труда
> наивно используем понятие "тот же самый". Посмотрим, например, на такой
> диалог:
>
>    - Мама: На столе лежит *то же самое *яблоко, что я оставила тебе на
>    ужин? Ты не съел?
>    - Вовочка: Я его съел. А на стол положил *такое же* из сумки, чтобы ты
>    утром поела.
>
> На Рефале и других функциональных языках мы можем говорить только про
> "такое же" яблоко. Поди отличи вчерашнее и сегодняшнее яблоки по их
> фотоснимкам на Рефале! Не сможете. А как видите, наш наивный мозг без труда
> использует понятие "то же самый", который формализуется уникальной ссылкой
> на вчерашний объект-яблоко, а сегодняшний объект-яблоко будет
> идентифицироваться другой, новой ссылкой. Это значит, что цивилизация, не
> испорченная математикой XIX (Фреге, Кантор) и XX (Гильберт, Бурбаки) веков,
> в принципе, могла бы сразу породить языки программирования с объектами и
> ссылками на них, а не идти долгим путем от Фортрана и Алгола-60 через Лисп
> и Рефал к Симуле-67 и затем к осознанию фундаментальности
> объектно-ориентированного программирования.
>
> Занятно, что в английском языке нет слов для такого четкого различения
> этих понятий, как в русском. Слово "the same" означает и "такой же", и "тот
> же самый". Интересно, труднее ли носителям английского языка понимать эту
> разницу, чем русским?
>
> В "Феномене науки" Турчин пишет, что "предметы", выделяемые "указателем
> внимания", и предикаты, признаки, значения – это разные сущности. У него
> это погружено в более широкое обсуждение и разбросано в нескольких местах.
> Я сейчас нашел их гуглением по слову "кинолента", поскольку помнил, что он
> использует эту метафору. Почитайте вот эти разделы и обратите внимание на
> приведенную во втором пункте цитату:
>
>    - *6.11. Физический предмет и логический объект*
>    http://www.refal.net/turchin/phenomenon/chapter06.htm#06.11
>    - *7.5. Феноменологическое определение семантики*
>    http://www.refal.net/turchin/phenomenon/chapter07.htm#07.05
>    «Теперь, когда мы ввели понятие указателя внимания, мы можем *определить
>    предмет как киноленту ситуаций с одной непрерывной линией указателя
>    внимания*.»
>    - *10.10. Платонизм в ретроспективе*
>    http://www.refal.net/turchin/phenomenon/chapter10.htm#10.10
>
> Турчин вводит понятие предмета в мире со временем. И в истории
> программирования понятие объекта появилось как обобщение изменяемой
> сущности в императивных языках. Но оказывается, все-таки есть возможность в
> логике и в языках программирования ввести понятие ссылки раньше понятия
> времени, то есть еще сохраняя чистую функциональность. А раз *можно*, то
> и *нужно *так поступить, чтобы построить адекватную иерархию понятий, –
> сначала формализовать понятие ссылки, а уже потом, и лишь только когда
> требуется, ввести понятие времени.
>
> Посему я хотел бы иметь такой универсальный метаязык (пусть это будет
> расширенный Рефал), в котором есть такие фундаментальные понятия нашего
> познания мира как предмет, уникальное имя предмета, а значит и
> программистское понятие объекта, про который говорят, используя слова "тот
> же самый". А также есть формализация этих слов в понятии ссылки,
> уникального имени. Отсюда возникает потребность внести это понятие в Рефал.
>
> Что имеется в виду? Ссылки порождаются оператором генерации новой, свежей,
> уникальной ссылки *new* или *fresh* – называйте по вкусу. Первое – из
> объектно-ориентированных языков, второе более распространено в
> математических текстах и используется в работах группы Andrew Pitts
> <https://www.cl.cam.ac.uk/~amp12>'а и их чисто функциональных языках *FreshML
> *и *Fresh Objective Caml*:
> https://www.cl.cam.ac.uk/~amp12/freshml/
>
> Формальное понятие ссылки можно (а значит и *нужно* – по Бритве Оккама)
> ввести до понятия того, на что она ссылается. Здесь слово "ссылка", "имя"
> сбивает с толку: "ссылка на что? имя чего?". А вот "ничего" – сама по себе.
> В работах группы Pitts'а для таких абстрактных ссылок и имен самих-по-себе
> используется менее двусмысленное слово "*атом*".
>
> Атом, сгенерированный оператором *new*, обладает единственным свойством: *он
> равен самому себе и не равен всему остальному в момент порождения*. При
> копировании – например, в вызове f(new) функции, возвращающей пару:
> f(x)=(x,x) – сохраняется тождественность атома самому себе в каждом его
> вхождении.
>
> Теоретико-множественный математик сойдет с ума от термов, использующих
> оператор new, как f(new), поскольку для них не выполняется *референциальная
> прозрачность *(*referential transparency*), пронизывающая основания
> нынешней логики и математики, а именно:
>
> Повторное вычисление может давать неравные результаты,
> например, для f выше:
> f(new) =/= f(new)
>
>
> Вот это и есть сущностная причина нелюбви функциональных программистов к
> ссылкам. И отношения математиков к ним как к низкоуровневому машинному
> понятию, вносящему "низменную грязь" в их "идеально чистый" математический
> мир.
>
> Но те, кто хочет иметь формальные языки, отражающие и моделирующие
> реальный мир, должны с ними смириться и строить для них "хорошие теории",
> чтобы было комфортно думать о ссылках и именах. В этом деле нам, "слабым
> программистам", за последние 30 лет пришли на помощь "сильные математики"
> во главе с Andrew Pitts <https://www.cl.cam.ac.uk/~amp12>'ом. Но еще
> много работы впереди, и мы без нее не останемся.
>
> На закуску порассуждаем математически, почему понятие ссылки, атома со
> связанным с ними равенством (назовем его *ссылочным*) – самое
> "фундаментальное". Напомним, что даже потеряв референциальную прозрачность,
> мы сохраняем упомянутое выше свойство, что при копировании равенство
> сохраняется:
>
>    - *let* x := *new*; y := *new in* x =/= y
>    - *let* x := *new*; y := x *in* x == y
>
> Теперь заметим, что все виды равенств, все отношения эквивалентности
> частично упорядочены импликацией: влечет ли одно равенство (обозначим =1=)
> другое (=2=):
>
>    - x =1= y  =>  x =2= y
>
> *Утверждение*. Из ссылочного равенства следуют все другие отношения
> равенства / эквивалентности, то есть:
>
>    - для ссылочного равенства R и любого отношения эквивалентности E:
>    x R y => x E y
>
> Говоря языком логики, ссылочное равенство – самое "сильное". Оно
> связывает равенством минимальное число сущностей. Меньше не придумаешь, не
> нарушая сохранения равенства при копировании. А без этого уж никуда!
>
> Говоря языком теории категорий, в категории равенств, категории отношений
> эквивалентности, ссылочное равенство – *инициальное *(*initial*). Это
> заумное слово означает в точности вышеприведенное утверждение и
> ничего больше.
>
> Вот поэтому, ссылки – это вовсе не адреса в памяти машины, а
> фундаментальное математическое понятие. Enjoy it!
>
> Андрей Климов
>
>
  • В з... Andrei Klimov andrei_AT_klimov . net
    • ... Александр Гусев gusev_aleksandr_AT_mail . ru
      • ... Andrei Klimov andrei_AT_klimov . net
      • ... Александр Коновалов a . v . konovalov87_AT_mail . ru
        • ... Александр Гусев gusev_aleksandr_AT_mail . ru
          • ... Александр Коновалов a . v . konovalov87_AT_mail . ru
    • ... Boyko Bantchev boykobb_AT_gmail . com

Ответить