Немножко про всякие равенства
В современной теории типов выделяют два основных класса равенств: 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.
Originally posted at http://deniok.dreamwidth.org/48850.html. Feel free to comment here or there.