?

Log in

No account? Create an account

Previous Entry | Next Entry

(Disclaimer: не то чтобы я в этом что-то понимал, будьте готовы к куче неточностей и ошибок)
Итак, допустим, ваш ребенок приходит из школы в слезах и говорит, что учитель зачеркнул 9*2 и вписал 2*9, "но ведь это одно и то же!"
А вы, будучи подкованы в современных веяниях науки, отвечаете так. Математика - это лишь прикладная теория типов, поэтому данный вопрос стоит рассмотреть с точки зрения этой теории. В теории типов у нас есть базовые суждения вроде "нечто является типом", "нечто является термом (выражением)" и "такой-то терм имеет такой-то тип" ("a : A"). Потом возникают индуктивные определения, состоящие из посылок и заключений. Например, "если A тип и В тип, то A -> B тоже тип". Еще: "если терм f имеет тип A -> B и терм x имеет тип A, то f x - это валидный терм, и он имеет тип В". Вводятся разные способы построения типов и термов: функция, произведение, сумма... Вводятся базовые типы. И вот тут первый ключевой момент. Если у нас есть терм
mul : Nat -> Nat -> Nat
то
mul 9 2 : Nat
Т.е. терм mul 9 2 - полноправный элемент типа Nat. Не число в привычной нам форме, не результат вычисления функции mul, а само выражение. Кажется, в этом одно из отличий типов от множеств. Никто не скажет, что выражение 9*2 входит в множество натуральных чисел, а вот в тип натуральных оно входит. И терм mul 2 9 тоже имеет тип Nat, и всякому очевидно, что mul 9 2 и mul 2 9 - это разные термы. А еще есть терм 18 того же типа, он на них совсем не похож, но все трое как-то связаны, они "равны". Что это значит? Если бы мы в нашей теории только вводили способы конструирования термов и типов, толку от нее было бы немного. Но у нее есть и вычислительное содержание. Подобно тому, как просветленный ум имеет два аспекта: это союз блаженства и пустоты, т.е. сострадания и мудрости, т.е. ясности и осознавания, т.е. конструирования ментальных образов и их познания, синтеза и анализа, в логике и теории типов всякое конструирование сопровождается способом разбора: если есть создание пары, есть и разбирающие ее на части fst и snd, если есть конструирование списка, есть и его разбор на части, head и tail, если есть конструирование натуральных чисел, есть и их элиминатор, рекурсор - математическая индукция. И вот эти элиминаторы обычно сопровождаются суждениями о равенстве термов. Мы не только говорим, что ежели р : (А,В) то fst p : A, но сопровождаем правилом:
fst (a,b) = a
Именно тут появляется равенство по определению, definitional equality. Именно оно позволяет утверждать, что fst (18, 3) = 18, именно благодаря ему и именно в этом смысле мы говорим, что термы fst (18, 3) и 18 равны. Аналогичное правило есть для рекурсора натуральных чисел, и через него мы определяем функциии на них, вроде той же mul.

Получается такая картина, что в том же типе Nat у нас куча разнообразных термов, и некоторые из них связаны между собой равенствами.

Связанные термы образуют направленные графы (с т.з. вычислений definitional equality связывает термы в определенном направлении - что во что вычисляется). Если мы не успели наделать в теории глупостей (вроде некоторых вредных аксиом), то каждый такой граф будет сходиться в одной точке, канонической форме. Это хорошее свойство, оно позволяет компилятору без труда убедиться, что термы mul 2 9, mul 9 2 и fst (18, 'x') равны по определению, достаточно каждый из них вычислить, пробежавшись по графу до канонической формы, и убедиться, что получился тот же терм (с точностью до переименования переменных, если они в нем есть). Более того, компилятор даже понимает, что 0 + x = x. Но вот что x + 0 = x он уже не понимает, термы x + 0 и x не definitionally equal, не равны в этом смысле, их не связывает путь в том графе. Потому что сложение у нас определено матчингом по первому аргументу; когда первый аргумент Z или S n, у нас есть какие-то равенства на этот счет, но когда первый аргумент - переменная, все, приехали. Тем более выражения x * y и y * x не равны definitionally. "Но ведь это одно и то же!"

Чтобы выразить эту однуитужесть, придумали propositional equality. В теории типов мы в типах можем выражать утверждения конструктивной математики, теоремы, а в термах их доказательства. Получилось построить терм нужного типа, населить тип - доказали теорему. Не получилось, тип остался пустым - теорема не доказана. Так вот, мы можем выразить утверждение "x = y" в виде типа, так называемого identity type. Терм такого типа будет доказательством, конструктивным обоснованием почему x = y. Подобно спискам и натуральным числам, опишем его в виде индуктивного типа (это должен быть инициальный объект в определенной категории), выражающего определенный принцип минимальности, в данном случае это "least reflexive relation", минимальное рефлексивное отношение. Задать его можно так:
если А - некоторый тип, то для него опишем семейство типов, индексированное двумя термами этого типа:
Id_A : A -> A -> Type
id_a : (a : A) -> Id_A a a
т.е. если мы возьмем два объекта x и y типа А, то Id_A x y будет типом, выражающим утверждение x = y. В Агде и Идрисе такой тип так и записывается, "x = y". У этого индуктивного типа один конструктор id_a, который для всякого значения a из A дает терм id_a(a) типа Id_A a a, т.е. служит доказательством того, что а=а. В Агде и Идрисе такой терм известен как refl. Все, что мы пока умеем им доказывать, что это отношение рефлексивно, а=а. Теперь, чтобы этот тип был минимальным рефлексивным отношением, он должен служить инициальным объектом в категории себе подобных, и выражается это так. Для любого типа А и любых его значений x и y, для любого утверждения D, опирающегося на равенство x=y, и его доказательства d(a) должна существовать стрелка J из нашего identity type в D, дающая это самое доказательство D. При этом D получается зависимым от Id_A x y типом, а стрелка J - его сечением (пи-типом). Т.е. если
D : {x,y : A} -> Id_A x y -> Type
d : (a : A) -> D a a id_a
то существует
J(D,d) : {x,y :A} -> (p : Id_A x y) -> D x y p
с таким свойством, что
J(D, d, id_a) = d(a)

Выглядит с непривычки сложно, но это просто один из стандартных способов описания произвольных индуктивных типов в теории с зависимыми типами - через dependent elimination. В результате у нас появляется способ конструировать какие-то следствия. Например, если положить
D(x, y, p) = Id_A y x и
d = \x -> id_x : (x : A) -> D(x, x, id_x)
то J дает нам
J(D,d,x,y,p) : Id_A y x для каждого p : Id_A x y. Тогда inv = J(D,d,x,y) это функция из Id_A x y в Id_A y x. А вычислительное правило для J дает inv(id_x) = id_x. Мы получили симметричность отношения.
Аналогично можно получить функцию композиции
(о) : Id_A y z -> Id_A x y -> Id_A x z
дающую транзитивность. Мы получили тройку рефлексивность-симметричность-транзитивность, т.е. отношение эквивалентности. Причем симметричность и транзитивность оказались выведены как свойства, следствия из минимальной рефлексивности.

Пользуясь таким понятием равенства, мы можем показать, что x*y равно y*x, т.е. тип Id_Nat (x*y) (y*x) населен. Это то, что делается в библиотеках Агды, Идриса и других языков этого уровня. Леммы про коммутативность умножения там имеют такой тип. Однако если мы возьмем две функции f,g : Nat -> Nat
f x = 2 * x
g x = x * 2
то доказать их равенство, не только definitional, но даже propositional, мы не сможем! "Но это же одно и то же!"

Для этого нам требуется function extensionality - принцип, гласящий, что если для всякого аргумента две функции дают одинаковые результаты, то сами эти функции равны. В интенсиональной теории типов, что тут пока излагалась, этот принцип невыводим. И это разумно: мы вовсе не обязательно хотим считать равными функциями те, что дают одинаковые результаты, нам ведь может быть небезразлично их внутреннее устройство. Если одна вычисляет результат за константное время, а вторая за экспоненциальное, мы можем захотеть не считать их равными и взаимозаменяемыми. Если же допустить function extensionality, то они становятся равны, неразличимы. Поскольку этот принцип сам собой не выводится, его, если он нужен, можно ввести через дополнительные аксиомы. И тут возможны варианты. Можно его просто в явном виде ввести как аксиому. Можно пойти чуть в обход и, аксиоматизировав uniqueness of identity proofs (UIP), сделать теорию типов экстенсиональной, там function extensionality уже выводится. Но оба подхода имеют проблемы. Перестает работать теорема о канонических формах. Что означает, например, что у нас может возникнуть терм типа Bool, вычисление которого застревает, и в результате не получается ни True, ни False. Кроме того, в экстенсиональной теории из пропозиционального равенства следует вычислительное, из-за чего проверка типов становится неразрешимой. Ну и UIP делает теорию одномерной (об этом позже), неинтересной. Однако есть и другой способ получить function extensionality, не постулируя ее и сохраняя теорию интенсиональной. Для этого нам пригодится топология.

В топологии мы рассматриваем пространства, где у точек бывают соседи, что связывает разные области пространства и позволяет по ним мысленно перемещаться. Две точки в одной связной области мы можем соединить путем, определяемым как непрерывное отображение интервала [0,1] на это пространство. Если один путь заканчивается в некоторой точке, а другой в ней начинается, мы можем из них составить композицию путей. Кроме того, всякий путь мы можем развернуть, пройти его в обратном направлении, оказавшись в исходной точке. Имея два пути p и q из точки х в точку y, мы можем рассмотреть непрерывное отображение одного пути в другой.

Это уже будет непрерывное отображение интервала [0,1] на пространство путей, или, что то же самое, отображение квадрата [0,1]х[0,1] на исходное пространство, двумерная такая поверхность. Такое отображение называется гомотопией. И если рассматривать не исходное пространство Х, а уже пространство путей в нем, то гомотопии в Х будут служить путями в этом пространстве путей. Их тоже можно отображать друг в друга, получая уже трехмерные штуковины, их - дальше, в четырехмерные и т.д. до бесконечности. При этом когда мы гомотопией непрерывно превращаем один путь в другой, нам важно, чтобы его начальная и конечная точки оставались на месте, а все другие мы можем шевелить свободно, лишь бы это делалось плавно, непрерывно. Если возьмем некоторый путь p из х в y, возьмем обратный к нему p-1, полученный просто сменой направления, и возмьмем их композицию p-1 . р, получим путь из х в х. Он будет отличен от тривиального пути из х в х - стояния на месте. Однако теперь, когда точка y перестала быть концом, мы можем наш составной путь начать шевелить, и плавно и непрерывно можем его стянуть до стояния на месте, тривиального пути из х в х, построить гомотопию из p-1 . р в id_x. Говорят, что такие пути равны с точностью до гомотопии.

Теперь вернемся к теории типов. Если мы посмотрим на описанные выше identity types, то увидим, что они ведут себя в точности как пути в топологии! Тип IdA x y "соединяет" точки x и y в пространстве (типе) А. У него всегда есть обратный путь IdA y x, мы можем строить композиции. Более того, тип IdA x y мы можем рассматривать как пространство и задуматься о пропозициональном равенстве элементов этого пространства, т.е. путей в нем. Если p и q - доказательства того, что x=y, они оба имеют тип IdA x y. Утверждение о том, что они сами равны, будет типом
IdIdA x y p q
Если a и b - доказательства того, что p = q, то утверждение, что a = b будет типом
IdIdIdA x y p q a b
и т.д. до бесконечности.
Итак, допустим у нас есть путь p из x в y и тривиальные пути id_x из х в х и id_y из y в y. Как связаны p и p . id_x? Оказывается, они не равны definitionally, но равны propositionally, т.е. из p в p . id_x есть путь, мы его можем построить конструктивно, пользуясь индуктивным определением IdA y x и его элиминатором J. Так мы можем доказать следующие утверждения, т.е. представить конкретные функции этих типов:

1) reflRight: p ~~> (p o id_x)
2) invLeft : p-1 o p ~~> id_x и invRight : p o p-1 ~~> id_y
3) invTwice : (p-1)-1 ~~> p (исправлено, тут была ошибка)
4) assoc : r o (q o p) ~~> (r o q) o p

Тут (q o p) - композиция путей, как описана ранее, а "x ~~> y" - синоним для IdA x y, такое обозначение проще и лучше отражает идею пути из х в y.
Подобно тому, как в топологии композиция пути с обратным ему не тождественна тривиальному пути, но равна с точностью до гомотопии, пути более высокого измерения, так и композиция idenity type с обратным не равна-по-определению тривиальному (id_x a.k.a. refl), но равна с точностью до idenity type более высокого порядка, пути более высокого измерения. Заметим, что перечисленные свойства очень похожи на определение группы, где есть пространство некоторых элементов (здесь это пути), есть ассоциативная бинарная операция "умножения" (в данном случае это композиция), есть нейтральный элемент, который при участии в умножении не меняет результата (тут тривиальный путь), у каждого элемента есть обратный (тут обратный путь), умножение на который дает нейтральный элемент. Только в группе это все должны быть прямые равенства, не "с точностью до". Есть еще понятие группоида - это категория, где все стрелки - изоморфизмы, тогда если там взять стрелки как элементы группы, а их композицию как умножение, все законы группы выполняются, но опять же там равенства более строгие. Когда же равенства в группоиде выполняются с точностью до путей более высокого измерения, которые сами опять образуют такую псевдогруппу, где законы выполняются с точностью до путей еще более высокого измерения и т.д. до бесконечности, такая конструкция называется ∞-группоид. Так вот, выходит, что и типы в интенсиональной теории типов, и топологические пространства имеют одну и ту же алгебраическую структуру ∞-группоида. Вот мы и приехали к гомотопической теории типов (HoTT), теперь название такое должно быть понятно откуда берется.

Гомотопия в HoTT определяется чуть иначе, чем в топологии, она как бы повернута на 90 градусов. Если у нас есть две функции f и g типа A -> B, то гомотопия между ними определяется как
H = (x : A) -> f x ~~> g x
Это функция, которая для каждого х из А производит доказательство того, что f x = g x. Тип такой функции, пространство всех гомотопий между f и g обозначается f ~ g.
Имея арсенал зависимых типов и путей, можно рассуждать о таких топологических вещах, как стягиваемость пространств и их эквивалентность. Пространство А стягиваемо, если в нем существует такой элемент а, что любой элемент х из А ему равен:
isContr(A) := Exists (a:A), (x:A) -> x ~~> a
т.е. для доказательства стягиваемости пространства А мы должны предъявить зависимую пару, где первый элемент - значение а из А, а второй - функция, которая для каждого х производит доказательство того, что х = а, конкретный путь из х в а. В частности, несложно показать, что тип unit стягиваемый. Стягиваемый тип обязан быть непустым, иначе мы не сможем предъявить а.
Эквивалентность пространств можно определять немного по-разному, есть альтернативные подходы. Например, если у нас есть функция f : A -> B и точка b в B, можно сначала определить homotopy fiber
hFiber(f,b) := Exists (a:A), f a ~~> b
Это тип пар, где первый элемент - значение из А, а второй - доказательство того, что f его отображает в значение, равное b. Фактически, это обратный образ для f в точке b. Утверждение, что функция f - это эквивалентность, это такой тип:
isEquiv(f) := (b : B) -> isContr( hFiber(f,b) )
Т.е. если для каждой точки b из B существует ее праобраз в А (относительно f). Очень похоже на биекцию, только равенства везде пропозициональные. Отдельно доказывается, что всякая функция-эквивалентность это изоморфизм и наоборот.
Ну а дальше мы говорим, что пространства (типы) А и В эквивалентны, если существует такая функция f для которой населен isEquiv(f). Эквивалентность пространств А и В будем обозначать А ~= B.

Теперь, мы можем рассмотреть пространство всех типов Type (не включая его самого, делаем стандартную иерархию вселенных а-ля Агда и подкапотный Идрис). Обычные типы, вроде Nat и (Int -> Int), будут его элементами. Тогда для двух элементов типа Type, для двух типов А и В, мы можем задуматься: а когда они равны? Утверждение о равенстве двух типов А и В будет типом
IdTypeA B
или в нашем новом обозначении A ~~> B. Это тип, т.е. тоже пространство, точки в котором - это доказательства равности А и В, пути в Type. Утверждение об эквивалентности простанств А и В, А ~= B, это тоже тип, тоже пространство. Мы можем построить конструктивно функцию
v(A,B) : (A ~~> B) -> (A ~= B)
которая логически означает, что из пропозиционального равенства двух типов следует их эквивалентность. При этом сама v - это функция из пространства (A ~~> B) в пространство (A ~= B). Что можно сказать об этих двух пространствах? Тут приходит Воеводский и говорит: давайте добавим одну аксиому, аксиому унивалентности:
univalence : {A, B : Type} -> isEquiv( v(A,B) )
т.е. постулируем, что такая v - это эквивалентность. Другими словами,
(A ~~> B) ~= (A ~= B)
пространство путей между двумя типами эквивалентно пространству эквивалентностей (и изоморфизмов) между этими типами. Бах!

Внезапно, наличие такой аксиомы сразу дает очень много плюшек и многое упрощает. В том числе из нее автоматом получается следствие
ndfe : {f,g : A -> B} -> (f ~ g) -> (f ~~> g)
- это наивная независимотиповая function extensionality; из гомотопии между f и g можно получить доказательство равности f и g. Возвращаясь ближе к началу поста, у нас были
f x = 2 * x
g x = x * 2
доказать равенство которых мы не могли. Мы можем построить гомотопию
H : (x : A) -> f x ~~> g x
которая для каждого x произведет доказательство того, что 2 * x = x * 2 (это банальное упражнение для агда-программистов), и теперь ndfe H нам даст значение типа f ~~> g, т.е. доказателство равности этих двух функций. В случае зависимых типов, доказывается, что из унивалентности также следует weak function extensionality:
wfe : ((x:A) -> isContr(P x)) -> isContr( (x:A) -> P x )
а еще ранее, безо всякой унивалентности, можно было показать, что из нее следует strong function extensionality:
sfe : (f,g : (x:A) -> P x) -> isEquiv( hApply(f,g) )
где
hApply : (f, g : (x:A) -> P x) -> (f ~~> g) -> (f ~ g)
т.е. для всяких зависимых функций из (х:А) в (Р х) пространство гомотопий между ними эквивалентно пространству путей между ними.

Вот так, добавив одну аксиому, можно сохранить интенсиональность теории типов, ее многомерную структуру и получить доказательство равности f x = 2 * x и g x = x * 2.

К слову о многомерности. В этой теории типы можно классифицировать по уровням. Чтобы было интересней, в классической гомотопической теории они нумеруются начиная с -2. Тип уровня -2 - это любой стягиваемый тип, например unit, он же () в хаскеле.
Тип уровня -1 - это h-prop, он характеризуется формулой A -> isContr(A): он стягиваем если населен. Его еще называют proof-irrelevant, любые два значения его пропозиционально равны, но в отличие от уровня -2 они могут и не существовать вовсе. Такой тип используется для записи многих логических утверждений.
Тип уровня 0 - это h-set, тип множеств. В таком типе может быть много разных значений, но любые доказательства равности его элементов сами между собой равны, т.е. справедлив принцип uniqueness of identity proofs. В ETT, экстенсиональной теории типов, все типы - это такие одномерные множества.
Тип уровня 1 - это группоид, в нем могут быть нетривиальные морфизмы, но все 2-морфизмы тривиальны. И т.д. Категорно, n-типы соответствуют n-группоидам.
Получаются такие типы обрезанием ∞-группоида, когда мы выбираем некоторый уровень n и объявляем все пути более высокого порядка равными.

Вот, как-то так обстоят дела с 2*9=9*2.

Tags:

Comments

( 69 comments — Leave a comment )
kodt_rsdn
May. 24th, 2013 04:01 am (UTC)
От такого содержательного поста - только завидки берутся и штампы говорятся:
- tl;dr (честное слово, пытался осилить, но где-то после гомотопий сломался)
- папа, ты сейчас с кем разговаривал?

Кстати говоря, учителка ругается не на (*) :: Nat->Nat->Nat, а на (*) :: Foo Nat -> Bar Nat -> FooBar Nat.
Девять женщин по две сумки у каждой - это не то же самое, что две женщины по девять сумок. В первом случае - шопинг, во втором - безумный шопинг.
w00dy
May. 24th, 2013 05:48 am (UTC)
> Девять женщин по две сумки у каждой - это не то же самое, что две женщины по девять сумок. В первом случае - шопинг, во втором - безумный шопинг

Вот самое правильное объяснение, а те 5 экранов текста никто читать не будет :)
(no subject) - thedeemon - May. 27th, 2013 07:25 am (UTC) - Expand
(no subject) - bik_top - May. 24th, 2013 05:59 am (UTC) - Expand
(no subject) - sassa_nf - May. 24th, 2013 08:42 am (UTC) - Expand
(no subject) - afa_at_work - Jun. 6th, 2013 06:19 am (UTC) - Expand
(Deleted comment)
enerjazzer
May. 24th, 2013 05:08 am (UTC)
боюсь, они будут закрыты, а дыхание будет ровным и глубоким
theiced
May. 24th, 2013 05:44 am (UTC)
зачем ты это написал? как теперь жить дальше?
nivanych
May. 24th, 2013 08:54 am (UTC)
Тебе-то чего?
Типы не нужны и всё написанное тебе следует проигнорировать.
(no subject) - sassa_nf - May. 24th, 2013 09:35 am (UTC) - Expand
(no subject) - nivanych - May. 24th, 2013 10:13 am (UTC) - Expand
(no subject) - sassa_nf - May. 24th, 2013 10:43 am (UTC) - Expand
(no subject) - nivanych - May. 24th, 2013 11:18 am (UTC) - Expand
(no subject) - ex_juan_gan - May. 25th, 2013 02:45 am (UTC) - Expand
(no subject) - sassa_nf - May. 25th, 2013 04:30 am (UTC) - Expand
(no subject) - thedeemon - May. 25th, 2013 07:26 am (UTC) - Expand
(no subject) - sassa_nf - May. 25th, 2013 07:41 pm (UTC) - Expand
(no subject) - thedeemon - May. 25th, 2013 07:35 am (UTC) - Expand
(no subject) - sassa_nf - May. 25th, 2013 07:46 pm (UTC) - Expand
(no subject) - deni_ok - May. 25th, 2013 08:44 am (UTC) - Expand
(no subject) - sassa_nf - May. 25th, 2013 08:04 pm (UTC) - Expand
iigoncharenko
May. 24th, 2013 07:36 am (UTC)
Это ты не по мотивам выступления Харпера из Орегонской школы?
thedeemon
May. 24th, 2013 07:53 am (UTC)
Да, во многом по нему.
(no subject) - iigoncharenko - May. 24th, 2013 07:56 am (UTC) - Expand
(no subject) - thedeemon - May. 24th, 2013 08:08 am (UTC) - Expand
(no subject) - iigoncharenko - May. 24th, 2013 08:10 am (UTC) - Expand
(no subject) - iigoncharenko - Jun. 13th, 2013 04:58 am (UTC) - Expand
(no subject) - thedeemon - Jun. 13th, 2013 06:08 am (UTC) - Expand
(no subject) - iigoncharenko - Jun. 13th, 2013 06:43 am (UTC) - Expand
(no subject) - kurilka - May. 24th, 2013 03:07 pm (UTC) - Expand
(no subject) - thedeemon - May. 24th, 2013 03:18 pm (UTC) - Expand
(no subject) - kurilka - May. 24th, 2013 03:20 pm (UTC) - Expand
akuklev
May. 24th, 2013 07:43 am (UTC)
Какое приятное введение в HoTT!
Ещё бы объяснение на пальцах, почему OTT это одномерное обрезание HoTT с сохранением канонiчности.
ex_juan_gan
May. 25th, 2013 02:36 am (UTC)
А, ну вот и ответ на мой немой вопрос, хотя бы и в виде вопроса.
sassa_nf
May. 24th, 2013 08:51 am (UTC)
"d : (a : A) -> D a a id_a"

а не нужен ли здесь

d : (a : A) -> D a a (id_a a)
thedeemon
May. 24th, 2013 10:06 am (UTC)
Да, если считать id_a функцией, так было бы правильнее. Но создаст путаницу дальше; скорее, стоит id_a иначе определить.
Там должно быть id : (a : A) -> Id_A a a
И тогда id_a будет означать id a.
(no subject) - sassa_nf - May. 24th, 2013 10:44 am (UTC) - Expand
(no subject) - thedeemon - May. 24th, 2013 11:03 am (UTC) - Expand
sassa_nf
May. 24th, 2013 08:59 am (UTC)
"Леммы про коммутативность умножения там имеют такой тип. Однако если мы возьмем две функции f,g : Nat -> Nat
f x = 2 * x
g x = x * 2
то доказать их равенство, не только definitional, но даже propositional, мы не сможем!"

не знаю :) в упражнениях к BrutalDepTypes коммутативность умножения доказывается через function extensionality

ну хм, или я чего путаю. Вообще-то речь там о равенстве типов двух функций, а не равенстве функций; но поскольку типы функций зависят от значений аргументов, ...это намекает на function extensionality. Или как?

Edited at 2013-05-24 01:21 pm (UTC)
thedeemon
May. 24th, 2013 10:07 am (UTC)
Если у нас уже есть function extensionality, то доказать равенство тех функций мы можем, об этом и речь. Вопрос в том, откуда взять function extensionality. Вот Агда откуда берет?
(no subject) - sassa_nf - May. 24th, 2013 10:38 am (UTC) - Expand
voidex
May. 24th, 2013 10:07 am (UTC)
Спасибо за пост
ex_juan_gan
May. 25th, 2013 02:39 am (UTC)
Ну это вообще праздник. Читал мелкими кусочеками, смаковал. Ну конечно, надо будет и лекции послушать.

Меня как категорщика тут немножко удивляет, как это - бац, и стрелки ввели в типах; да ещё такое есть мрачное подозрение, что и аксиома выбора прячется (эпиморфизмы секутся). Но это прекрасно, прекрасно. Остаётся, действительно, покрыть вопрос ОТТ... ну и также расписать вот эту вот категорность типов чуток поподробнее (так чтоб не выглядело как чёртик из табакерки).

Роскошно.
thedeemon
May. 25th, 2013 03:44 am (UTC)
Спасибо. :)
Честно говоря, категорную интерпретацию зависимых типов я еще сам не осилил. С простыми типами все кажется просто, а вот с зависимыми..

Про ОТТ пойду пока почитаю.
(no subject) - ex_juan_gan - May. 25th, 2013 03:56 am (UTC) - Expand
(no subject) - sassa_nf - May. 25th, 2013 04:45 am (UTC) - Expand
(no subject) - ex_juan_gan - May. 25th, 2013 01:08 pm (UTC) - Expand
migmit
May. 25th, 2013 04:19 am (UTC)
> Математика - это лишь прикладная теория типов

А вот хамить не надо.
ex_juan_gan
May. 25th, 2013 01:09 pm (UTC)
Тут ещё интересный вопрос - а что, геометрические теории тоже покрываются? Нет такого ощущения у меня.
smartdiver
Jun. 8th, 2013 06:45 am (UTC)
согласен - 2 мужика * 9 литров водки != 9 мужиков * 2 литра :)
однако как быть с выражением:
2 мужика * 9 литров == 9 литров * 2 мужика
???
os80
Jan. 11th, 2014 04:39 am (UTC)
>3) invTwice : (p-1)-1 ~~> id_y
Но как? Как "путь" из x в y может быть "~~>" пути из y в y?
thedeemon
Jan. 11th, 2014 05:41 am (UTC)
Это у меня ошибка копипасты, спасибо. Там должно быть
(p-1)-1 ~~> p
uhbif19
Jun. 17th, 2018 08:03 pm (UTC)
Вот я не понял, экзистенциональность теории типов <=> выполнению function extensionality или это разные вещи?

Алсо читал у Воеводского, что одной из главных мотиваций к построению HoTT была невозможность в теории множеств нормально говорить об "одноитожести", то подменять друг-другом изоморфные обьекты. Я правильно понимаю, что экстенсиональность это оно и есть или нет?
thedeemon
Jun. 19th, 2018 03:08 am (UTC)
Это несколько разные вещи. function extensionality это свойство, которое может быть как в экстенсиональной, так и в интенсиональной теории типов, просто получается оно разными путями.
В экстенсиональной теории типов нет описываемой тут иерархии "вот два разных доказательства, что а=б, а вот доказательство, что те два доказательства равны между собой", всех этих Id_Id_A. Там все Id_A уникальны или автоматически равны. См. https://ncatlab.org/nlab/show/extensional+type+theory Такая теория "плоская", без башни уровней типов.
( 69 comments — Leave a comment )