Доброе утро, Андрей и Александр!
Андрей описал «нижнюю границу» для отношения эквивалентности: копии одного
значения должны быть равны между собой.
Но для эквивалентности функций можно определить и верхнюю границу:
значения-функции, реализующие различные частичные функции, должны быть не равны:
f == g → ∀x . f(x) == g(x)
∃x . f(x) ≠ g(x) → f ≠ g
В презентации эта граница описана на слайде 49 «Про фазы луны». Слайд оказался
неочевидным, поэтому я попробую сформулировать другими словами.
Пусть у нас есть два исходника:
/* F1.ref */
$ENTRY F {
s.F s.G e.Arg, <Eq s.F s.G> : True = <s.F e.Arg>;
s.F s.G e.Arg = "!=";
}
Eq {
t.X t.X = True;
t.Y t.Z = False;
}
/* F2.ref */
$ENTRY F {
s.F s.G e.Arg, <Eq s.F s.G> : True = <s.G e.Arg>;
s.F s.G e.Arg = "!=";
}
Eq {
t.X t.X = True;
t.Y t.Z = False;
}
В первом исходнике F1.ref, если первые два символа аргумента равны, вызывается
первый символ как функция. Во втором F2.ref — второй символ. Отличия между
исходниками выделено красным цветом.
При правильной реализации равенства должен быть верен инвариант: в любой
программе, которая использует исходник F1.ref, его можно заменить на F2.ref (и
наоборот) и поведение программы не изменится. Т.е. если s.F и s.G равны (могут
сопоставиться с одноимёнными переменными), то функции, реализуемые ими, должны
быть идентичны: в одинаковой среде при одинаковых аргументах должны возвращать
одинаковый результат и иметь одинаковый побочный эффект, либо обе
зацикливаться, либо обе завершаться аварийно.
Написать, что если s.F и s.G равны, то <Eq (<s.F e.Arg>) (<s.G e.Arg>)> будет
равно True нельзя, т.к. в Рефале функции могут быть нечистыми (представьте, что
s.F ≡ s.G ≡ &Get, функция чтения файла, тогда два последовательных вызова
прочитают две разные строчки). Поэтому в докладе пришлось привлекать
астрономическое явление, а здесь говорить о взаимозаменяемости исходников.
Поэтому такие простые отношения «равенства», как все замыкания равны друг другу
и все замыкания не равны друг другу, выходят за рамки этих граничных условий.
Если все замыкания друг другу не равны, значит копии будут не равны друг другу.
Если все замыкания друг другу равны, то равны окажутся различные функции.
С уважением,
Александр Коновалов
From: Александр Гусев gusev_aleksandr_AT_mail.ru <[email protected]>
Sent: Tuesday, May 18, 2021 11:24 PM
To: refal <[email protected]>
Subject: Re: В защиту ссылок в Рефале – Was: Рефал-семинар 17 мая 2021 в 10:30
в Zoom'e
Спасибо, Андрей!
Всё замечательно выражено. Действительно, если даны правильные определения,
дискутировать становится подчас не о чем.
Я, конечно, подразумевал именно адресные ссылки, которые наблюдал в языках
высокого уровня и остался ими недоволен. А вот математически описанные Вами
ссылки - это отлично, проходит!
Отправлено из мобильной Почты Mail.ru
вторник, 18 мая 2021 г., 23:01 +0300 от refal <[email protected]
<mailto:[email protected]> >:
После семинара между двумя Александрами (Гусевым и Коноваловым) возникла
переписка с ограничеснной рассылкой только тем, кто был на семинаре. Я захотел
встрять и посылаю письмо в refal@botik c надеждой, что это обсуждение будет
интересно всем. Также я указал в BCC тех, кто был на семинаре, но на нашу
рассылку не подписан, и еще некоторых коллег.
Оба Александра выразили свою нелюбовь к понятию ссылки как к кандидату к
включению в область данных Рефала. А я выступлю в защиту этого понятия, в том
числе с математической точки зрения.
Подозреваю, нарушения эквивалентности при наивных преобразованиях в Рефале с
лямбда-выражениями, о которых на семинаре рассказывал Александр, произошло
именно потому, что семантика равенства по ссылке, "ссылочного равенства", была
не до конца осознана. Она действительно нетривиальна. Эквивалентные
преобразования, по определению, должны сохранять семантику. А для этого
семантика должна быть понята и сформулирована.
From: Александр Гусев <[email protected] <mailto:[email protected]>
>
Sent: Monday, May 17, 2021 11:17 PM
Лично я - противник использования ссылок в Рефале. Оставьте их языкам близким к
машинному уровню. Здесь же «ссылка» должна быть просто отсылкой к функции или
объекту, но не адресом. Даже если в низкоуровневой основе это и адрес. Это как
использование goto в императивных языках понижает качество кода. Goto - это для
низкоуровневого кода, ассемблера и естественно присутствует в любой программе,
но на машинном уровне.
On Tue, 18 May 2021 at 14:53, Александр Коновалов <[email protected]
<mailto:[email protected]> > 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>
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!
Андрей Климов
