Александр, спасибо за лестный отзыв. Я рад, что мои писательские труды не были даром. ;-) Андрей
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! > > Андрей Климов > >
