کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4950700 1364300 2017 35 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
The vectorial λ-calculus
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
The vectorial λ-calculus
چکیده انگلیسی
We describe a type system for the linear-algebraic λ-calculus. The type system accounts for the linear-algebraic aspects of this extension of λ-calculus: it is able to statically describe the linear combinations of terms that will be obtained when reducing the programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We prove that the resulting typed λ-calculus is strongly normalising and features weak subject reduction. Finally, we show how to naturally encode matrices and vectors in this typed calculus.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 254, Part 1, June 2017, Pages 105-139
نویسندگان
, , ,