Немножко про всякие равенства

[deniok]

 

В современной теории типов выделяют два основных класса равенств: Definitional equality и Propositional equality. 

 

Definitional equality

Definitional equality можно перевести как равенство-по-определению. Пример:

two = suc (suc zero)

Таким равенством мы выражаем идею интенсиональности, вкладывая в него представление об одинаковости смысла левой и правой частей. Равенство-по-определению задаёт полный синоним, его можно использовать подстановочным образом при переписывании термов. Ещё один (тривиальный) пример - переименование связанных переменных, часто называемое альфа-конверсией.

 

Ещё один класс равенств, которые часто рассматривают как подвид равенств-по-определению, это вычислительные равенства (computational equality), то есть равенство, основанное на редукциях

(λx. x + x) two = two + two = suc (suc (suc (suc zero)))

 

Propositional equality

 

Прямые вычислительные правила не подходят для того, чтобы показать, что для двух произвольных натуральных x и y имеет место равенство

x + y = y + x

Это утверждение описывает экстенсиональное равенство, то есть вычислительно оно выполняется на каждой конкретной паре натуральных аргументов. Фактически это не определение, а теорема; если определять сложение рекурсивно, то можно дать индуктивное доказательство (которое, однако, далеко не тривиально).

 

В теории типов экстенсиональное равенство это суждение (judgment, суждение в логике - это высказывание на мета-языке), а не высказывание (proposition, последнее понимается как часть формальной системы, а не мета-языка). Можно, однако, включить его в формальную систему, введя высказывание об идентичности (identity type) :

_≡_ : ℕ → ℕ → Proposition

То есть

∀ x y → x + y ≡ y + x

выражает пропозициональное равенство, конкретно - высказывание о том, что сложение натуральных коммутативно. Терм, населяющий такой тип, служит доказательством этого высказывания. Для Агды, например, такое доказательство можно посмотреть здесь или в модуле  Data.Nat.Properties стандартной библиотеки, однако во втором случае требуется понимание того, как работает модуль ≡-Reasoning.

 

 

Ссылки

 

Хороший небольшой туториал про равенства в Агде: Andreas Abel, Agda: Equality.

 

Ну и первоисточник (не считая Пера нашего Мартин-Лёфа), в котором гораздо больше полезных идей по сравнению с моим конспективным изложением:  nLab, Equality. 

Comments

[nivanych.livejournal.com]

А как же observational?...

[deni-ok.livejournal.com]

Пускай Epigram 2 выкатывают, тогда и напишу :)

[nponeccop.livejournal.com]

К перу ещё надо бы Бенгта нашего Норстрома присовокупить:

http://www.cse.chalmers.se/research/group/logic/book/

Там как раз идея интенсиональности-экстенсиональности в деталях разобрана.

[deni-ok.livejournal.com]

Да, я сейчас посмотрел - полезная книжка. Мне их терминология не нравилась, они называют set то, что стоило бы называть type.

[nponeccop.livejournal.com]

А я наоборот считаю, что Пер зачем-то назвал типами то, что всегда было множествами.

Педагогически это уменьшит путаницу в типах 1-5 (см. http://nponeccop.livejournal.com/297483.html), привьет мысль о том, что типы - это абстрактные метки произвольной природы.