2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу 1, 2  След.
 
 Унивалентные основания математики. HoTT. Coq.
Сообщение21.01.2015, 13:13 


26/11/13
29
Есть замечательная книга, которую можно бесплатно скачать отсюда:
http://homotopytypetheory.org/book/
(28(!!) человек её писали, в том числе Мартин-Лёф, Кокан и Воеводский)

Моя цель:
изучить полностью хотя бы первую главу книги.
решить упражнений в конце главы с помощью формальной системы в приложении "A2 The second presentation" на стр.537

Мотивация:
1) очень широкий круг математических объектов возможно будет аксиоматизировать и лучше понимать
2) напрямую это связано с машинной проверкой теорем (язык Сoq)

Проблема:
Никто из знакомых мне математиков не занимается этим.

Вопросы:

Я буду крайне признателен, если доказательтво хотя бы одного номера из упражнений кто-либо, кто разбирается, проведёт через подстановки, описанные в приложении А2.

Пример: ассоциативность композиции - элементарна на бумаге
$(f \circ (g\circ h))(x)=f((g\circ h)(x))=f(g(h(x)))=(f\circ g)(h(x))=((f\circ g)\circ h)(x)$,
но как её осуществить через ту формальную систему?
Далее тип функции композиции:
$\circ : \Pi_{A,B,C:U_0} (A \rightarrow B)  \rightarrow (B \rightarrow C)  \rightarrow(A \rightarrow C)  $
Учитывая, что по определению
$(A \rightarrow B) \equiv \Pi_{a:A} B $
$\Pi_{x_1,x_2:X} Y \equiv \Pi_{x_1:X}\Pi_{x_2:X} Y$, то можно перейти к совершенно страшной формуле со множество букв $\Pi$ .

Определяем композицию как
$\circ(g, h, x) := g(h(x))$

Вопрос 1: как это всё в формальном виде написать в контекст Г?
(контекст как я понял - просто список утверждений)

Вопрос 2: Как, используя описанные в А2 правила подстановки доказать ассоциативность композиции?
(в Википедии есть доказательство на Coq, но оно пока вне моего понимания, не могу связать с формальной системой, описанной в книге)

Вопрос 3: Кто-нибудь этим занимается или хочет(а это, полагаю, очень круто для развития своего математического аппарата) заняться за компанию?

Вопрос 4: Можно привести любые(желательно побольше) простые содержательные пример, когда мы что-то определеяем в этой системе, но не отступаем от её строгости.

Заранее спасибо.

 Профиль  
                  
 
 Re: Унивалентные основания математики. HoTT. Coq.
Сообщение21.01.2015, 16:21 
Заслуженный участник
Аватара пользователя


06/10/08
6422
Я читал HoTT поверхностно, сейчас тоже хочу подробно проработать, но времени нет.

Композицию с тем типом, который Вы указали, можно определить в пустом контексте как $\circ = \lambda (A, B, C : \mathcal{U})  .\, \lambda (g : A\to B) .\, \lambda (h : B\to C) .\, \lambda (x : A) .\, h(g(x))$. Получить это можно, применяя правила $\Pi$-elim и $\Pi$-intro из контекста $A,B,C : \mathcal{U}, g : A\to B, h : B\to C, x : A$. Если все расписывать, то получится вот так:

1. $A : \mathcal{U}, B : \mathcal{U}, C : \mathcal{U}, g : A\to B, h : B\to C, x : A\ \mathrm{ ctx}$
2. $A : \mathcal{U}, B : \mathcal{U}, C : \mathcal{U}, g : A\to B, h : B\to C, x : A \vdash x : A$ (из 1, правило Vble)
3. $A : \mathcal{U}, B : \mathcal{U}, C : \mathcal{U}, g : A\to B, h : B\to C, x : A \vdash g : A\to B$ (из 1, правило Vble)
4. $A : \mathcal{U}, B : \mathcal{U}, C : \mathcal{U}, g : A\to B, h : B\to C, x : A \vdash g(x) : B$ (из 2 и 3, правило $\Pi$-elim с учетом определения $A\to B = \Pi (x : A). B$)
5. $A : \mathcal{U}, B : \mathcal{U}, C : \mathcal{U}, g : A\to B, h : B\to C, x : A \vdash h : B\to C$ (из 1, правило Vble)
6. $A : \mathcal{U}, B : \mathcal{U}, C : \mathcal{U}, g : A\to B, h : B\to C, x : A \vdash h(g(x)) : C$ (из 5 и 6, правило $\Pi$-elim с учетом определения $B\to C = \Pi (x : B). C$)
7. $A : \mathcal{U}, B : \mathcal{U}, C : \mathcal{U}, g : A\to B, h : B\to C \vdash \lambda (x:A).h(g(x)) : A\to B$ (из 6, правило $\Pi$-intro с учетом определения $A\to C = \Pi (x : A). C$)
и так далее, с помощью $\Pi$-intro вводим кучу лямбд, в итоге получаем
$\vdash \lambda (A {:} \mathcal{U}).\lambda (B {:} \mathcal{U}). \lambda (C {:} \mathcal{U})  .\, \lambda (g : A\to B) .\, \lambda (h : B\to C) .\, \lambda (x : A) .\, h(g(x)) : \Pi (A : \mathcal{U}). \Pi (B : \mathcal{U}). \Pi (C : \mathcal{U}). (A\to B) \to ((B\to C) \to (A\to C))$

Дальше с помощью $\circ(A, B, C, g, h, x) \equiv h(g(x)) : C$ (это равенство доказывается многократным применением $\Pi$-comp), Subst и $\Pi$-uniq можно доказать ассоциативность.

В общем, это долго и нудно, такими вещами пусть занимаются компьютеры. Если хотите заниматься формализованными вещами, лучше разберитесь с coq или agda.

 Профиль  
                  
 
 Re: Унивалентные основания математики. HoTT. Coq.
Сообщение23.01.2015, 16:25 


26/11/13
29
Планирую, чтобы разобраться:
а) написать доказательство полностью и строго
б) постепенно писать программу для вывода выражений.(уже немного автоматизировал процесс: см. код сообщения. Код данного сообщения виден, если его цитировать)

Вопросы:
1) что-нибудь не нравится в приведённом ниже коде? (Я не использовал Vble; номера используемых строк в скобках, в порядке записи "числителя" правил в книге; def значит заданы изначально в контексте Г)

2) в правиле П-form для вывода необходимо существование в контексте Г семейства типов "из A в U". По-простому - множество функций. Как получить такое(см строки 4 и 5) выражение(терм)? По-моему необходимо просто существование элемента в A и существование множества в U, например самого А.
Я не понимаю, в чём сокровенный смысл именно такой записи через запятую. (Почему нельзя просто сделать так:
$A:U_i$
$B:U_{i+1\mbox{(правильно?)}}$
$a:A$ (т.е. типы непустые)
$b:B$,
следовательно существует П-тип $\Pi(x:A)B:U_i$)

\def\mylan#1{\newcounter{myl#1}}
\def\myit{\stepcounter{mya}\arabic{mya}}
\def\myla#1{\setcounter{myl#1}{\value{mya}}}

\newcounter{mya}
\mylan{1}\mylan{2}\mylan{3}\mylan{4}

\begin{tabular}{llclcp{6cm}}
 %\mys{\Gamma,x:A,ctx-EMP}  %%\\
 %\myit & \mbox{ctx-EMP}&$=>$& $\Gamma \vdash A:U_0$\\
 \myit & def &$\Rightarrow$& $\Gamma$&$\vdash$&$ A:U_0$\myla{1}\\ 
 \myit & def &$\Rightarrow$& $\Gamma$&$\vdash$&$ B:U_0$\\ %\setcounter{myl1}{\value{mya}}
 \myit & def &$\Rightarrow$& $\Gamma$&$\vdash$&$ C:U_0$\\ %\myla ,
 \myit & def? &$\Rightarrow$& $\Gamma , x:A $&$\vdash$&$ B:U_0$\myla{2}\\
 \myit & def? &$\Rightarrow$& $\Gamma , x:A $&$\vdash$&$ C:U_0$\myla{4}\\
 \myit & $\Pi$-$form(\arabic{myl1},\arabic{myl2})$&$\Rightarrow$& $\Gamma$&$\vdash$&$ \Pi(a:A).B:U_0$\\ 
\myit & $\Pi$-$form(\arabic{myl1},\arabic{myl4})$&$\Rightarrow$& $\Gamma$&$\vdash$&$ \Pi(a:A).C:U_0$\\ 
 \myit & def &$\Rightarrow$& $\Gamma$&$\vdash$&$ x:A$\myla{1}\\
 \myit & def &$\Rightarrow$& $\Gamma$&$\vdash$&$ g:\Pi(a:A).B$\myla{3}\\
 \myit & $\Pi$-$elim(\arabic{myl3},\arabic{myl1})$ &$\Rightarrow$& $\Gamma$&$\vdash$&$ g(x):B$\myla{1}\\
 \myit & def &$\Rightarrow$& $\Gamma$&$\vdash$&$ h:\Pi(a:B).C$\myla{3}\\
 \myit & $\Pi$-$elim(\arabic{myl3},\arabic{myl1})$ &$\Rightarrow$& $\Gamma$&$\vdash$&$ h(g(x)):B$\myla{3}\\
 \myit & $\Pi$-$intro(\arabic{myl3})$ &$\Rightarrow$& $\Gamma$&$\vdash$&$ \lambda(z:A).h(g(z)):\Pi(a:A).C$\myla{3}\\
...\\
 ?& ? &$\Rightarrow$& $\Gamma$&$\vdash$&$ \lambda(A:U_0).\lambda(B:U_0).\lambda(C:U_0).\lambda(z:A).h(g(z)):\Pi(a:A).C$\\
$?& ? &$\Rightarrow$& $\Gamma$&$\vdash$& $\circ(A, B, C, g, h, x) \equiv h(g(x)) : C$
\\
\end{tabular}
Спасибо.

 Профиль  
                  
 
 Re: Унивалентные основания математики. HoTT. Coq.
Сообщение23.01.2015, 20:18 
Заслуженный участник


27/04/09
28128
Строку, например, 4 можно получить так:$$\frac{\Gamma\vdash A:\mathcal U_0\quad\quad\Gamma\vdash B:\mathcal U_0}{\Gamma,x:A\vdash B:\mathcal U_0}\;\mathsf{Wkg}_1$$из ваших гипотез 1 и 2. Только зачем вам гаммы? Гамма — это метатеоретическое обозначение контекста; в конкретном выводе и контексты конкретные. Хотя можно, конечно, сразу «схемы выводов» делать, только я пока не вижу плюсов, кроме как производные правила вывода получать.

-- Пт янв 23, 2015 22:45:24 --

Yorick в сообщении #967222 писал(а):
Я не понимаю, в чём сокровенный смысл именно такой записи через запятую. (Почему нельзя просто сделать так:
$A:U_i$
$B:U_{i+1\mbox{(правильно?)}}$
$a:A$ (т.е. типы непустые)
$b:B$,
следовательно существует П-тип $\Pi(x:A)B:U_i$)
Не понял вопрос, но спрошу о другом: разве тип $\Pi(x:\mathbf0).\mathbf1$ не существует и не содержит элемент $\lambda(x:\mathbf0).\star$? :wink: Для образования Π-типа наличие элементов в типе аргумента функции не обязательно!

 Профиль  
                  
 
 Re: Унивалентные основания математики. HoTT. Coq.
Сообщение25.01.2015, 21:48 


26/11/13
29
Вопросы:
1) В определении композиции я использую "вселенную" $\mathcal{U}_i$, однако уже в $\mathcal{U}_{i+1}$ могут быть множества(они же типы), для которых не определена композиция. Как тогда её определять в общем случае для всех юнивёрсумов?
2) Допустимо ли следующее применение правила П-comp? И как тогда понимать замену $\mathcal{U}_0[x/z]$?
$$(1)\Gamma,  z:A \vdash B:\mathcal{U}_0$$\\
$$(2)\Gamma \vdash x:A$$\\
$$(3)\Pi-comp(\myr{1},\myr{2}) \Rightarrow \Gamma \vdash (\lambda(z:A).B)(x)\equiv B[x/z]:\mathcal{U}_0[x/z]$$
3) Я правильно понял, что формальная система, описанная в книге - творчески переработанный Мартин-Лёф и поэтому маловероятно найти более подробное её рассмотрение? (в библиографии пока не нашёл)
4) Что означает правило ctx-emp?
5) Как понимать точки в правилах $\Sigma-elim$ и $\Sigma-comp$? Похоже на лямбда-абстракции.
Книга говорит:
Цитата:
The expression $\Sigma(x:A).B$ binds free occurrences of x in B. Furthermore,
because $ind_{\Sigma(x:A).B}$ has some arguments with free variables beyond those
in Г, we bind (following the variable names above) z in C, and x and y
in g. These bindings are written as z.C and x.y.g, to indicate the names
of the bound variables. In particular, we treat $ind_{\Sigma(x:A).B}$ as a primitive,
two of whose arguments contain binders; this is superficially similar to,
but different from, $ind_{\Sigma(x:A).B}$ being a function that takes functions as ar-
guments.
(раздел A.2.5)

6*) В доказательстве ниже есть грубые логические ошибки?

Ниже, в утверждении 20 - решётка(#) обозначает, нужный для использования данного правила терм находится в "посыле" , т.е. до символа $\vdash$. (Кстати, как он называется?)

Определение композиции:
\def\mylan#1{\newcounter{myl#1}\setcounter{myl#1}{0}}
\def\myit{\stepcounter{mya}\arabic{mya}}
\def\myla#1{\setcounter{myl#1}{\value{mya}}}

\def\GammKI{\Gamma}
\def\Un\mathcal{U}
\newcounter{mya}\setcounter{mya}{0}
\mylan{1}\mylan{2}\mylan{3}\mylan{4}\mylan{5}\mylan{6}\mylan{7}\mylan{8}\mylan{9}\mylan{10}
\mylan{11}\mylan{12}\mylan{13}\mylan{14}\mylan{15}\mylan{16}\mylan{17}\mylan{18}\mylan{19}\mylan{20}
\mylan{21}\mylan{22}\mylan{23}\mylan{24}\mylan{25}\mylan{26}\mylan{27}\mylan{28}\mylan{29}\mylan{30}
\mylan{31}\mylan{32}\mylan{33}\mylan{34}\mylan{35}\mylan{36}\mylan{37}\mylan{38}\mylan{39}\mylan{30}
\begin{tabular}{llclcp{7cm}}
 \myit & def &$\Rightarrow$& $\GammKI$&$\vdash$&$ A:\mathcal{U}_0$\myla{1}\\ 
 \myit & def &$\Rightarrow$& $\GammKI$&$\vdash$&$ B:\mathcal{U}_0$\myla{2}\\ %\setcounter{myl1}{\value{mya}}
 \myit & def &$\Rightarrow$& $\GammKI$&$\vdash$&$ C:\mathcal{U}_0$\myla{3}\\ 
 \myit & $wkg_1(1,2)$ &$\Rightarrow$& $\GammKI,  z:A $&$\vdash$&$ B:\mathcal{U}_0$\myla{4}\\
 \myit & $wkg_1(1,3)$ &$\Rightarrow$& $\GammKI,  z:A $&$\vdash$&$ C:\mathcal{U}_0$\myla{5}\\
 \myit & $wkg_1(2,3)$ &$\Rightarrow$& $\GammKI,  z:B $&$\vdash$&$ C:\mathcal{U}_0$\myla{6}\\

 \myit & $\Pi$-$form({1},{4})$&$\Rightarrow$& $\GammKI$&$\vdash$&$ \Pi(w:A).B:\mathcal{U}_0$\myla{7}\\ 
 \myit & $\Pi$-$form({1},{5})$&$\Rightarrow$& $\GammKI$&$\vdash$&$ \Pi(w:A).C:\mathcal{U}_0$\myla{8}\\ 
 \myit & $\Pi$-$form({2},{6})$&$\Rightarrow$& $\GammKI$&$\vdash$&$ \Pi(w:B).C:\mathcal{U}_0$\myla{9}\\ 
 \myit & $wkg_1({1},{8})$ &$\Rightarrow$& $\GammKI, f:\Pi(z:B).C$&$\vdash$&$ \Pi(z:A).C :\mathcal{U}_0$\myla{10}\\

 \myit & $\Pi$-$form({9},{10})$ &$\Rightarrow$& $\GammKI$&$\vdash$&$ \Pi(f:\Pi(a:B).C).\Pi(z:A).C :\mathcal{U}_0$\myla{11}\\
 \myit & $wkg_1({7},{11})$ &$\Rightarrow$& $\GammKI, g:\Pi(z:A).B$&$\vdash$&$ \Pi(f:\Pi(a:B).C).\Pi(z:A).C :\mathcal{U}_0$\myla{12}\\

 \myit & $\Pi$-$form({7},{12})$ &$\Rightarrow$& $\GammKI$&$\vdash$&$ \Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C :\mathcal{U}_0$\myla{13}\\
 \myit & $wkg_1({3},{13})$ &$\Rightarrow$& $\GammKI, C:\mathcal{U}_0$&$\vdash$&$ \Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C :\mathcal{U}_0$\myla{14}\\
 \myit & $\Pi$-$form({3},{14})$ &$\Rightarrow$& $\GammKI$&$\vdash$&$ \Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C :\mathcal{U}_0$\myla{15}\\

 \myit & $wkg_1({2},{15})$ &$\Rightarrow$& $\GammKI, B:\mathcal{U}_0$&$\vdash$&$ \Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C :\mathcal{U}_0$\myla{16}\\
 \myit & $\Pi$-$form({2},{16})$ &$\Rightarrow$& $\GammKI$&$\vdash$&$ \Pi(B:\mathcal{U}_0).$\\&&&&&$\Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C :\mathcal{U}_0$\myla{17}\\

 \myit & $wkg_1({3},{17})$ &$\Rightarrow$& $\GammKI, A:\mathcal{U}_0$&$\vdash$&$ \Pi(z:A).C :\mathcal{U}_0$\myla{18}\\
 \myit & $\Pi$-$form({3},{18})$ &$\Rightarrow$& $\GammKI$&$\vdash$&$ 
\Pi(A:\mathcal{U}_0).\Pi(B:\mathcal{U}_0).$\\&&&&&$\Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C :\mathcal{U}_0$\myla{19}\\ %A.3 p545
\end{tabular}
\def\myit{\stepcounter{mya}\arabic{mya}}
\def\myla#1{\setcounter{myl#1}{\value{mya}}}
\def\GammKI{\Gamma}
\def\Un\mathcal{U}
\newcounter{mya}\setcounter{mya}{19}
\begin{tabular}{llclcp{7cm}}
\myit\myla{20} & $\Pi$-$elim({4}, \mbox{\#})$ &$\Rightarrow$& $\GammKI, z:A $&$\vdash$& $g(z):B$\\
\myit\myla{21} & $\Pi$-$elim({6}, \mbox{20})$ &$\Rightarrow$& $\GammKI, z:A $&$\vdash$& $h(g(z)):C$\\
\myit & $\Pi$-$intro({21})$ &$\Rightarrow$& $\GammKI $&$\vdash$& $\lambda(z:A).h(g(z)):\Pi(z:A).C$\myla{22}\\
\myit & $\Pi$-$wkg({10},{22})$ &$\Rightarrow$& $\GammKI, f:\Pi(a:B).C $&$\vdash$&$\lambda(z:A).h(g(z)):\Pi(z:A).C$\myla{23}\\

\myit & $\Pi$-$intro({23})$ &$\Rightarrow$& $\GammKI  $&$\vdash$& $\lambda(f:\Pi(a:B).C).\lambda(z:A).h(g(z)):
$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\myla{24}\\
\myit & $\Pi$-$wkg({12},{24})$ &$\Rightarrow$& $\GammKI, g:\Pi(a:A).B$&$\vdash$&$\lambda(f:\Pi(a:B).C).\lambda(z:A).h(g(z)):$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\myla{25}\\

\myit & $\Pi$-$intro({25})$ &$\Rightarrow$& $\GammKI $&$\vdash$& $\lambda(g:\Pi(a:A).B).\lambda(f:\Pi(a:B).C).$\\&&&&&$\lambda(z:A).h(g(z)):
$\\&&&&&$\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\myla{26}\\
 \myit & $\Pi$-$wkg({3},{26})$ &$\Rightarrow$& $\GammKI, C:\mathcal{U}_0$&$\vdash$&$\lambda(g:\Pi(a:A).B).\lambda(f:\Pi(a:B).C).$\\&&&&&$\lambda(z:A).h(g(z)):\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\myla{27}\\

\myit & $\Pi$-$intro({27})$ &$\Rightarrow$& $\GammKI$&$\vdash$&$ \lambda(C:\mathcal{U}_0).\\ &&&&&\lambda(g:\Pi(a:A).B).\lambda(f:\Pi(a:B).C).$\\&&&&&$\lambda(z:A).h(g(z)):
$\\&&&&&$\Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\myla{28}\\

 \myit & $\Pi$-$wkg({2},{28})$ &$\Rightarrow$& $\GammKI, B:\mathcal{U}_0$&$\vdash$&$\lambda(C:\mathcal{U}_0).\\ &&&&&\lambda(g:\Pi(a:A).B).\lambda(f:\Pi(a:B).C).$\\&&&&&$\lambda(z:A).h(g(z)):
$\\&&&&&$\Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\myla{29}\\
%A:\mathcal{U}_0
 \myit & $\Pi$-$intro({29})$ &$\Rightarrow$& $\GammKI $&$\vdash$&$ \lambda(B:\mathcal{U}_0).\lambda(C:\mathcal{U}_0).\\ &&&&&\lambda(g:\Pi(a:A).B).\lambda(f:\Pi(a:B).C).$\\&&&&&$\lambda(z:A).h(g(z)):
\Pi(B:\mathcal{U}_0).$\\&&&&&$\Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\myla{30}\\

 \myit & $\Pi$-$wkg({1},{30})$ &$\Rightarrow$& $\GammKI, A:\mathcal{U}_0$&$\vdash$&$ \lambda(B:\mathcal{U}_0).\lambda(C:\mathcal{U}_0).\\ &&&&&\lambda(g:\Pi(a:A).B).\lambda(f:\Pi(a:B).C).$\\&&&&&$\lambda(z:A).h(g(z)):
\Pi(B:\mathcal{U}_0).$\\&&&&&$\Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\myla{31}\\

 \myit & $\Pi$-$intro({31})$ &$\Rightarrow$& $\GammKI$&$\vdash$&$ \circ \equiv \lambda(A:\mathcal{U}_0).\lambda(B:\mathcal{U}_0).\lambda(C:\mathcal{U}_0).\\ &&&&&\lambda(g:\Pi(a:A).B).\lambda(f:\Pi(a:B).C).$\\&&&&&$\lambda(z:A).h(g(z)):
\Pi(A:\mathcal{U}_0).\Pi(B:\mathcal{U}_0).$\\&&&&&$\Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\\ %A.3 p545
\end{tabular}

 Профиль  
                  
 
 Re: Унивалентные основания математики. HoTT. Coq.
Сообщение25.01.2015, 23:28 
Заслуженный участник


27/04/09
28128
Yorick в сообщении #968299 писал(а):
Ниже, в утверждении 20 - решётка(#) обозначает, нужный для использования данного правила терм находится в "посыле" , т.е. до символа $\vdash$.
Таким способом это не работает. :-) Можно выводить только из того, что выше, тем более что контекст не является утверждением.

Yorick в сообщении #968299 писал(а):
(Кстати, как он называется?)
Да вроде просто контекст (context), посмотрите A.2.1.

Yorick в сообщении #968299 писал(а):
1) В определении композиции я использую "вселенную" $\mathcal{U}_i$, однако уже в $\mathcal{U}_{i+1}$ могут быть множества(они же типы), для которых не определена композиция. Как тогда её определять в общем случае для всех юнивёрсумов?
Ровно так же, меняя индексы у $\mathcal U_i$ на нужные (в конкретном выводе все универсумы имеют конкретные индексы, а если там везде $i+k$, то это уже схема, генерирующая по выводу для каждого конкретного $i$ с соответствующими разницами во встречающихся типах).

Yorick в сообщении #968299 писал(а):
2) Допустимо ли следующее применение правила П-comp? И как тогда понимать замену $\mathcal{U}_0[x/z]$?
$$(1)\Gamma,  z:A \vdash B:\mathcal{U}_0$$$$(2)\Gamma \vdash x:A$$$$(3)\Pi-comp(\myr{1},\myr{2}) \Rightarrow \Gamma \vdash (\lambda(z:A).B)(x)\equiv B[x/z]:\mathcal{U}_0[x/z]$$
Если я сравнил аккуратно, то всё в порядке. А $\mathcal{U}_0[x/z]$ — это просто $\mathcal U_0$, т. к. переменная $z$ в терме $\mathcal U_0$ не встречается.

Yorick в сообщении #968299 писал(а):
4) Что означает правило ctx-emp?
Это правило утверждает, что пустой контекст — это контекст. :-) Без него нельзя было бы вывести никакое утверждение вида $\vdash a:A$ или $\vdash a\equiv b:A$, и, кроме того, без изменений в правилах вывода, вообще никакое утверждение, т. к. не к чему было бы применять ctx-EXT.

Yorick в сообщении #968299 писал(а):
5) Как понимать точки в правилах $\Sigma-elim$ и $\Sigma-comp$?
Эти точки указывают, что некоторые переменные терма, не связанные другим образом ($\lambda,\Pi,\Sigma$), связаны, чтобы подстановка вместо одноимённой переменной их не заменяла.

 Профиль  
                  
 
 Re: Унивалентные основания математики. HoTT. Coq.
Сообщение09.03.2015, 00:52 


08/03/11
273
Не обязательно использовать Coq. Можно использовать DFG, TPTP и пруверы первопорядковой логики и получать доказательства.

 Профиль  
                  
 
 Re: Унивалентные основания математики. HoTT. Coq.
Сообщение17.05.2015, 12:44 


26/11/13
29
Вот, допустим такой лист выкладок
\def\GammKI{\Gamma}
\begin{tabular}{llclcp{7cm}}
1 & def &$\Rightarrow$& $\GammKI$&$\vdash$&$ A:\mathcal{U}_0$\\ 
2 & def &$\Rightarrow$& $\GammKI$&$\vdash$&$ B:\mathcal{U}_0$\\ 
3 & $wkg_1(1,2)$ &$\Rightarrow$& $\GammKI, z:A$&$\vdash$&$ B:\mathcal{U}_0$\\ 
4 & $\Pi-form(1,3)$ &$\Rightarrow$& $\GammKI$&$\vdash$&$\Pi(z:A).B:\mathcal{U}_0$\\ 
\end{tabular}$$

Что значит выражение $\Gamma, z:A \vdash B:\mathcal{U}_0$ в интерпретации теории множеств?
(Я понимаю как "в контексте гамма существует правило под названием B, которое сопоставляет каждому элементу z множества A подмножество множества U". Правда пока не совсем ясно как это правило записывать)

$$a:A,\quad A:\mathcal{U}_0,\quad \mathcal{U}_0:\mathcal{U}_1, ...$$
"Вселенная" это тоже тип или между ними есть разница? Вроде тоже тип, просто другого уровня: элемент 'a' - тип 1го уровня. множество 'A' - 2го, вселенная 'U' - 3го.

arseniiv в сообщении #968363 писал(а):
Yorick в сообщении #968299 писал(а):
4) Что означает правило ctx-emp?
Это правило утверждает, что пустой контекст — это контекст. :-) Без него нельзя было бы вывести никакое утверждение вида $\vdash a:A$ или $\vdash a\equiv b:A$, и, кроме того, без изменений в правилах вывода, вообще никакое утверждение, т. к. не к чему было бы применять ctx-EXT.

Но что такое пустой контекст?(типа некого глобального, берущийся по умолчанию?) Мне кажется, что уместно делать несколько контекстов, называть их Г1, Г2, ..., ГN, и при каком-либо доказательстве "подключать" их, используя
$$\frac{\Gamma\vdash a:A \quad \Gamma,x:A,\Delta\vdashb:B}{\Gamma,\Delta\lbrack a/x \rbrack\vdash b\lbrack a/x \rbrack : B \lbrack a/x \rbrack}Subst_1,$$
где заменяются те переменные, которые объявлялись как "def".

В чём разница между positive type и negative type?

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

p.s.
исправления в мой последний большой текст(я пока очень не уверен в них)
\def\GammKI{\Gamma}
\begin{tabular}{llclcp{7cm}}
0 & def &$\Rightarrow$& $\GammKI$&$\vdash$&$ \mathcal{U}_0$ //или несколько для общего случая?\\ 
3.5 & def &$\Rightarrow$& $\GammKI$&$\vdash$&$ w:A$\\ 
20 & $\Pi$-$elim({4}, {3.5})$ &$\Rightarrow$& $\GammKI, z:A$&$\vdash$& $g(z):B$\\
21 & $\Pi$-$elim({6}, {20})$ &$\Rightarrow$& $\GammKI, z:A$&$\vdash$& $h(g(z)):C$\\
\end{tabular}

p.p.s.
https://github.com/pcapriotti/hott-exercises
http://blog.ezyang.com/2013/07/hott-exe ... -progress/
к сожалению предлагаемые решения упражнений на Agda и Coq не показывают как сам механизм работает, я бы с удовольствием почитал какие-нибудь машинные выводы, чтобы яснее видеть механизм.

 Профиль  
                  
 
 Re: Унивалентные основания математики. HoTT. Coq.
Сообщение17.05.2015, 15:21 
Заслуженный участник
Аватара пользователя


06/10/08
6422
Yorick в сообщении #1016364 писал(а):
Что значит выражение $\Gamma, z:A \vdash B:\mathcal{U}_0$ в интерпретации теории множеств?

Начнем с того, что у HoTT интерпретации в теории множеств, как я понимаю, нет. Из-за нетривиальности равенства и из-за универсумов. Но если Вам хочется какую-то интуицию из теории множеств, то можно считать, что типы в $U_0$ - это "нечто типа множеств", а типы в $U_1$ - это "нечто типа классов". Соответственно, интерпретация $\Gamma, z\colon A \vdash B\colon U_0$ будет "в контексте $\Gamma$ каждому элементу "множества" $A$ сопоставляется "множество" $B$".

Yorick в сообщении #1016364 писал(а):
"Вселенная" это тоже тип или между ними есть разница?
Тоже тип. Просто элементами его являются типы, а так ничего особенного.

Yorick в сообщении #1016364 писал(а):
Но что такое пустой контекст?(типа некого глобального, берущийся по умолчанию?)
Пустой контекст - это пустой контекст. Это значит, что мы ничего не предполагаем. Например, $\vdash \lambda (A\colon U_0). \lambda (a\colon A). a \colon \Pi (A\colon U_0). (A\to A)$ значит, что у нас есть конкретный обитатель конкретного типа, и нам никаких предположений для этой конструкции не надо.

 Профиль  
                  
 
 Re: Унивалентные основания математики. HoTT. Coq.
Сообщение17.05.2015, 23:28 
Заслуженный участник


27/04/09
28128
Yorick в сообщении #1016364 писал(а):
Буду благодарен за названия хороших источников(желательно русскоязычных, но не обязательно), по которым можно изучать основы этой теории типов.
Основа, как указывается в самой книге HoTT (Introduction § Type theory) — это теория типов Мартина-Лёфа (интенсиональная, если будет выбор между ей и экстенсиональной), так что если видели книги по этой, могут сгодиться (пока там к аксиомам не прибавляют что-нибудь не выводимое при добавлении вместо этого унивалентности, конечно).

 Профиль  
                  
 
 Re: Унивалентные основания математики. HoTT. Coq.
Сообщение24.05.2015, 18:15 


26/11/13
29
Зачем нужно правило 0-Elim и $\mbox{ind}_\mathbf{0}$? У нулевого типа нет элемента, соответственно никогда этим правилом воспользоваться не сможем.
Цитата:
The induction principle for the empty type
$\mbox{ind}_\mathbf{0}:\limits\Pi_{(C:\mathbf{0}\rightarrow\mathcal{U})}\limits\Pi_{(z:\mathbf{0})}C(z)$
gives us a way to define a trivial dependent function out of the empty
type
(?).


Как доказать, что $\mathcal{U}_{\infty}:\mathcal{U}_{\infty}$ неверно и приводит к заселению типа 0?

Если принять, что:
$A:\mathcal{U}_i$,
$a,b:A$,
то почему следующий тип уже не может принадлежать $\mathcal{U}_i$?
$\left(\limits\Pi_{P:A\rightarrow \mathcal{U}_i} P(a) \rightarrow  P(b)\right):\mathcal{U}_{i+1}$
(как прийти к противоречию?)

Предположнение: Если $A:\mathcal{U}_i$ и ... , то тип типа $\mbox{ind}_\Sigma$ принадлежит $\mathcal{U}_{i+1}$, но не $U_i$?

Что можно сказать про тип $(A\rightarrow \mathbf{0})\times((A\rightarrow \mathbf{0}) \rightarrow \mathbf{0})$?
Населён или не населён, если теория типов consistent?
Населён или не населён, если теория типов inconsistent?

p.s. Есть ли примеры необходимости отсутсвия унивалентности какой-либо вселенной для корректного описания какого-либо объекта математики, изначально не относившегося напрямую к теории типов?

 Профиль  
                  
 
 Re: Унивалентные основания математики. HoTT. Coq.
Сообщение24.05.2015, 22:31 
Заслуженный участник


27/04/09
28128
Yorick в сообщении #1019111 писал(а):
Как доказать, что $\mathcal{U}_{\infty}:\mathcal{U}_{\infty}$ неверно и приводит к заселению типа 0?
А что такое $\mathcal U_\infty$? Насколько помню, универсы нумеруются только натуральными числами.

Yorick в сообщении #1019111 писал(а):
Зачем нужно правило 0-Elim и $\mbox{ind}_\mathbf{0}$? У нулевого типа нет элемента, соответственно никогда этим правилом воспользоваться не сможем.
Как же не сможем? Всё, что мы можем вывести без посылки $x:\mathbf0$, мы сможем вывести и с ней. Вот попробуйте вывести recursor $\mathsf{rec}_{\mathbf0}:\Pi(A:\mathcal U).\,\mathbf0\to A$ с помощью этого правила и правила $\Pi$-\textsc{intro}. Он должен получиться равен $\lambda(A:\mathcal U).\,\lambda(y:\mathbf0).\mathsf{ind}_{\mathbf0}(x.\,A,y)$.

 Профиль  
                  
 
 Re: Унивалентные основания математики. HoTT. Coq.
Сообщение28.06.2015, 12:07 


26/11/13
29
Цитата:
The following important principles, called substitution and weak-
ening
, need not be explicitly assumed. Rather, it is possible to show, by
induction on the structure of all possible derivations
, that whenever the
hypotheses of these rules are derivable, their conclusion is also deriv-
able.

Каким образом строго доказываются утверждения по индукции на структуре всех возможных выводов?(например, $wkg_1$)

Цитата:
А что такое $\mathcal U_\infty$? Насколько помню, универсы нумеруются только натуральными числами.

Я просто хочу увидеть как прийти к противоречию из утверждения, что в неком унивёрсуме содержатся все типы, включая его самого.

 Профиль  
                  
 
 Re: Унивалентные основания математики. HoTT. Coq.
Сообщение28.06.2015, 19:06 
Заслуженный участник


27/04/09
28128
А что, это обязательно должно привести к противоречию? Ничего такого про универсумы там не было введено. В изложении мог что-нибудь пропустить или уже забыть, но это необходимо должно быть в начале первой части, большую часть которой я прочитал один раз. Утверждение $\mathcal U_{i+k}\colon\mathcal U_i$ даже не «склеивает» универсумы $\mathcal U_i,\ldots,\mathcal U_{i+k}$, делая находящиеся в них наборы типов одинаковыми, и даже не помещает каждый из них в каждый, потому что нет никакого «правила транзитивности» $\mathcal U_i\colon\mathcal U_j,\mathcal U_j\colon\mathcal U_k\vdash\mathcal U_i\colon\mathcal U_k$. Уж тем более нет каких-то следствий посерьёзнее, в том числе для универсумов с $i+k+1$. Если что-то упускаю, поправляйте.

Если никто не напишет по первому вопросу, соберусь.

P. S. Ерунда с формулами поправлена.

 Профиль  
                  
 
 Re: Унивалентные основания математики. HoTT. Coq.
Сообщение28.06.2015, 19:33 
Заслуженный участник
Аватара пользователя


06/10/08
6422
arseniiv в сообщении #1031889 писал(а):
А что, это обязательно должно привести к противоречию?
Парадокс Жирара (Girard). Там нетривиально, Yorick, почитайте где-нибудь описание этого парадокса.

arseniiv в сообщении #1031889 писал(а):
Утверждение $\mathscr U_{i+k}\colon\mathscr U_i$ даже не «склеивает» универсумы $\mathscr U_i,\colon\mathscr U_{i+k}$, делая находящиеся в них наборы типов одинаковыми, и даже не помещает каждый из них в каждый, потому что нет никакого «правила транзитивности» $\mathscr U_i\colon\mathscr U_j,\mathscr U_j\colon\mathscr U_k\vdash\mathscr U_i\colon\mathscr U_k$. Уж тем более нет каких-то следствий посерьёзнее, в том числе для универсумов с $i+k+1$. Если что-то упускаю, поправляйте.
Там в книжке кумулятивные универсумы, есть правило, по которому из $T:\mathcal{U}_i$ выводится $T:\mathcal{U}_{i+1}$.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 17 ]  На страницу 1, 2  След.

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: YandexBot [bot]


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group