کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4662043 | 1633471 | 2013 | 32 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Combinatorial realizability models of type theory
ترجمه فارسی عنوان
مدل های قابل تحقق ترکیبی از نظریه نوع
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
امکان اجرا؛ چسب؛ روابط منطقی؛ نظریه نوع هموتوپی؛ تئوری نوع Martin-Löf؛ معناشناسی Groupoid
موضوعات مرتبط
مهندسی و علوم پایه
ریاضیات
منطق ریاضی
چکیده انگلیسی
We introduce a new model construction for Martin-Löf intensional type theory, which is sound and complete for the 1-truncated version of the theory. The model formally combines, by gluing along the functor from the category of contexts to the category of groupoids, the syntactic model with a notion of realizability. As our main application, we use the model to analyse the syntactic groupoid associated to the type theory generated by a graph G, showing that it has the same homotopy type as the free groupoid generated by G.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Annals of Pure and Applied Logic - Volume 164, Issue 10, October 2013, Pages 957–988
Journal: Annals of Pure and Applied Logic - Volume 164, Issue 10, October 2013, Pages 957–988
نویسندگان
Pieter Hofstra, Michael A. Warren,