کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
435428 689906 2009 14 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Pedagogical second-order λλ-calculus
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Pedagogical second-order λλ-calculus
چکیده انگلیسی

The present work introduces the notion of pedagogical natural deduction systems, i.e. natural deduction systems for which hypotheses occurring in a proof must be motivated by an example. In formal terms, we replace the rule (Hyp): by the rule (P-Hyp): where σσ denotes a substitution which replaces all variables of ΓΓ with an example. This substitution is called the motivation   of ΓΓ. These systems are in essence negationless. In the present paper, we study second order propositional calculus, since it is a simple non-trivial natural deduction system in which negation can be defined. We present a Curry–Howard version of pedagogical second-order propositional calculus, i.e.  λλ-calculus bearing the pedagogical constraint. We establish that this system has the usual properties of typed calculi (subject reduction and strong normalization) and that it can type all second-order terms of λμλμ-calculus using a CPS translation. Furthermore, the main novelty is that all functions are useful: each polymorphic function has an instance which can be applied to a closed term.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 410, Issue 42, 28 September 2009, Pages 4190–4203
نویسندگان
, ,