کد مقاله کد نشریه سال انتشار مقاله انگلیسی ترجمه فارسی نسخه تمام متن
4662874 1345202 2016 29 صفحه PDF ندارد دانلود رایگان
عنوان انگلیسی مقاله
Bridging Curry and Church's typing style
ترجمه فارسی عنوان
ایجاد پیوند سبک تایپ کردن کاری و چرچ
کلمات کلیدی
سبک تایپ کردن چرچ. سبک تایپ کردن کاری . تایپ دامنه کامل ؛ تایپ بدون دامنه
Church-style typing; Curry-style typing; Domain-full typing; Domain-free typing
موضوعات مرتبط
مهندسی و علوم پایه ریاضیات منطق ریاضی
چکیده انگلیسی

There are two versions of type assignment in the λ  -calculus: Church-style, in which the type of each variable is fixed, and Curry-style (also called “domain free”), in which it is not. As an example, in Church-style typing, λx:A.xλx:A.x is the identity function on type A  , and it has type A→AA→A but not B→BB→B for a type B different from A  . In Curry-style typing, λx.xλx.x is a general identity function with type C→CC→C for every type C. In this paper, we will show how to interpret in a Curry-style system every Pure Type System (PTS) in the Church-style without losing any typing information. We will also prove a kind of conservative extension result for this interpretation, a result which implies that for most consistent PTSs of the Church-style, the corresponding Curry-style system is consistent. We will then show how to interpret in a system of the Church-style (a modified PTS, stronger than a PTS) every PTS-like system in the Curry style.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Applied Logic - Volume 18, November 2016, Pages 42–70
نویسندگان
, , ,