کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4951437 1364355 2016 21 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Equational reasoning with lollipops, forks, cups, caps, snakes, and speedometers
ترجمه فارسی عنوان
استدلال معادلاتی با نوشابه، چنگال، فنجان، کلاه، مار، و سرعت سنج
ترجمه چکیده
اثبات در تئوری طبقه بندی ابتدایی معمولا شامل چسباندن دیاگرام رفت و آمد یا استدلال محاسباتی با استفاده از زنجیره ای از مساوی است. بخش عمده ای از تلاش های این سبک ها می تواند با گام های مدیریتی ناخوشایند شامل فیزیکدان بودن، طبیعی بودن و مدیریت هویت ها مورد استفاده قرار گیرد. به عنوان یک جایگزین ما از استفاده از نمودارهای رشته، یک فرم دو بعدی از نشانه حمایت می کنیم که سکوت با این مراحل حسابداری منحرف می شود. در حالی که در ابتدا به منظور تشریح فاکتورها و تحولات طبیعی به کار گرفته شده است، نشان می دهیم که نمودارهای رشته نیز می توانند به راحتی اشیاء و فلش ها را جایگزین کنند. در طول مقاله ما تاکید می کنیم که چگونه آزادی توپولوژی ذاتی در علامت گذاری می تواند برای کمک به استفاده از شهود هندسی در توسعه اثبات استفاده شود. در واقع، رسم نمودارهای ریاضی کمی از هنر است: انتخاب های نمودار خوب می تواند تمام تفاوت ها را ایجاد کند.
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
چکیده انگلیسی
Proofs in elementary category theory typically involve either the pasting together of commuting diagrams or calculational reasoning using chains of equalities. Much of the effort in these styles can be consumed with trivial administrative steps involving functoriality, naturality, and the handling of identities. As an alternative, we advocate the use of string diagrams, a two-dimensional form of notation which silently deals with these distracting bookkeeping steps. While originally developed to reason about functors and natural transformations, we show that string diagrams can also easily accommodate objects and arrows. Throughout the paper we emphasize how the topological freedom inherent in the notation can be exploited to aid the use of geometric intuition in the development of proofs. Indeed, drawing string diagrams is a bit of an art: good diagrammatic choices can make all the difference.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 85, Issue 5, Part 2, August 2016, Pages 931-951
نویسندگان
, ,