عنوان فارسی:دانلود مقاله ترجمه شده یک الگوریتم ثابت شده برای محاسبه میانگین اعداد شناور اعشاری

دانلود مقاله ترجمه شده یک الگوریتم ثابت شده برای محاسبه میانگین اعداد شناور اعشاری – ۲۰۱۸ IEEE:الگوریتم‌های به درستی گرد شده برای محاسبه میانگین دو عدد نقطه شناور در محاسبات مبنای ۲ وجود دارند. متاسفانه، این الگوریتم‌ها در محاسبات مبنای ۱۰ درست نیستند. در این مقاله نشان داده‌ایم که احتمالات مختلف ساده، ناموفق هستند و میانگین به درستی گرد شده‌ای را نمی‌دهند. بنابراین، الگوریتمی را برای میانگین گرفتن از دو عدد نقطه شناور اعشاری با گردسازی درست ارائه داده و اثبات کردیم. الگوریتم ما ممکن است در مقایسه با فرمول‌های خط مستقیم، به دلیل ۶ فلاپ الگوریتم TwoSum، پر هزینه به نظر برسد. با این حال، نسبتا کوتاه است، و شناخت و اصلاح آن برای هر دقت ساده است.

مقاله انگلیسی+ترجمه فارسی

فهرست مطالب

چکیده
۱- پیشگفتار
۲- الگوریتم‌های میانگین مبنای ۲
۳- الگوریتم‌های ناموفق میانگین مبنای ۱۰
۴- الگوریتم برای میانگین اعداد نقطه شناور اعشاری
۵- برهان رسمی
۶- نتیجه‌گیری و چشم‌اندازها

چکیده

برخی از پردازنده‌های مدرن شامل واحدهای نقطه-شناور اعشاری، با تایید پیاده‌سازی استاندارد IEEE-754 2008 هستند. متاسفانه بسیاری از الگوریتم‌های ارائه شده در تحقیقات محاسبات کامپیوتری هنگام انجام محاسبات بر مبنای ۱۰، دیگر درست نیستند. این امر به ویژه در مورد محاسبه میانگین دو عدد نقطه شناور اتفاق می‌افتد. چند الگوریتم مبنای ۲، از جمله الگوریتمی که گرد کردن صحیح را فراهم می‌سازد، قابل دسترس هستند، اما در مبنای ۱۰ درست نیستند. برای تضمین سطح اطمینان بالاتر، همچنین برهان رسمی Coq از قضایای خود را فراهم می‌کنیم که پاریز تدریجی را ملاحظه می‌کند. توجه کنید که برهان رسمی ما برای حصول اطمینان از درست بودن این الگوریتم هنگام انجام محاسبات در هر مبنای زوجی تعمیم داده می‌شوند.

Abstract

Some modern processors include decimal floating-point units, with a conforming implementation of the IEEE-754 2008 standard. Unfortunately, many algorithms from the computer arithmetic literature are not correct anymore when computations are done in radix 10. This is in particular the case for the computation of the average of two floating-point numbers. Several radix-2 algorithms are available, including one that provides the correct rounding, but none hold in radix 10.

This paper presents a new radix-10 algorithm that computes the correctly-rounded average. To guarantee a higher level of confidence, we also provide a Coq formal proof of our theorems, that takes gradual underflow into account. Note that our formal proof was generalized to ensure this algorithm is correct when computations are done with any even radix.

نمونه ترجمه مقاله:

1. پیشگفتار

محاسبات نقطه-شناور[1] (FP) در هر جایی از زندگی ما وجود دارند. این محاسبات در نرم‌افزارهای کنترل و برای محاسبه پیش‌بینی‌های آب و هوایی مورد استفاده قرار می‌گیرند و بلوک اساسی بسیاری از سیستم‌های هیبرید (ترکیبی) – سیستم‌های تعبیه شده که محاسبات پیوسته، مانند نتایج حسگرها، و محاسبات گسسته، مانند محاسبات ساعت-محدود[2]، را ترکیب می‌کنند – هستند. محاسبات کامپیوتری [1، 2]، عمدتا به عنوان نادرست شناخته می‌شوند (اگر اصلا شناخته شوند)، زیرا تنها تعداد محدودی رقم برای جزء اعشاری نگه داشته می‌شوند. علاوه‌براین، تنها تعداد محدودی رقم برای نما حفظ می‌شوند. این امر، انتظارات سرریز و پاریز را ایجاد می‌کند که اغلب نادیده گرفته می‌شوند. در اینجا بیشتر علاقمند به بررسی پاریز هستیم.

این که کدام اعداد قابل دسترس هستند و عملیات روی آن‌ها چگونه رفتار می‌کنند در استاندارد IEEE-754 [3] سال 1895، که در سال 2008 اصلاح شده است [4]، استانداردسازی شد. این اصلاحیه به ویژه شامل محاسبات و اعدادا نقطه شناور مبنای 10 است. پردازنده‌های مرکزی با واحدهای نقطه شناور اعشاری در حال حاضر قابل دسترس هستند. این منجر به شاخه جدیدی از محاسبات کامپیوتری اختصاص داده شده به محاسبات اعشاری برای توسعه هر دوی نرم افزار و سخت افزار می‌شود.

مثال انتخاب شده بسیار ساده است: میانگین دو عدد نقطه شناور اعشاری چگونه محاسبه می‌شود:

که در اینجا  گرد کننده به نزدیک‌ترین عدد، به عنوان مثال با شکستن گره در عدد زوج، است. این محاسبه در مبنای 2 به نظر ساده می‌رسد، اما به دلیل سرریز دروغین، آنقدر هم ساده نیست. برای مراجع الگوریتم‌های میانگین مبنای 2، بخش 2 را ببینید. این سوال محاسبه میانگین، قبلا به ندرت در مبنای 10 مورد مطالعه قرار گرفته بود. فرمول ساده  نسبتا درست است اما همیشه نتیجه درست در مبنای 10، یعنی گرد کردن به نزدیک‌ترین میانگین ریاضی (برای الگوریتم‌های نادرست اضافی، بخش 3 را ببینید)، را ارائه نمی‌دهد. ب

به منظورِ داشتن تضمین بالا در مورد این نتیجه ریاضی، بر روش‌های رسمی تکیه خواهیم کرد. محاسبات نقطه شناور از سال 1989 به منظور اثبات رسمی الگوریتم‌ها و مولفه‌های سخت افزاری، رسمی شده است [5، 6، 7]. از تجزیه و تحلیل برهان Coq [8] و کتابخانه Flocq [9] استفاده خواهیم کرد. Flocq، رسمی‌سازی چند-مبنایی و چند-دقتی را برای فرمت‌های مختلف نقطه شناور و نقطه ثابت (از جمله نقطه شناورِ با یا بدون پاریز تدریجی) با کتابخانه جامعی از قضایا ارائه می‌دهد. کاربردپذیری و قابلیت اجرای آن، در برابر موارد-آزمون اثبات شده‌اند [10].

همه قضایای بیان شده در این مقاله متناظر با قضایای Coq قابل دسترس در https://www.lri.fr/∼sboldo/files/Average2n.v هستند.

[1] Floating-point

[2] clock-constrained