, стверджує, що розробляє прототип нової мови програмування.){kind=link}
محاسبات با کارایی بالا برای حل کارهای بیشتر و بیشتر مورد نیاز است - مانند پردازش تصویر یا برنامه های مختلف یادگیری عمیق در شبکه های عصبی - که در آن شما نیاز به پردازش حجم عظیمی از داده ها و انجام آن به اندازه کافی سریع دارید، در غیر این صورت ممکن است مقدار باورنکردنی طول بکشد. زمان. باور عمومی بر این است که هنگام انجام چنین عملیاتی، سازش بین سرعت و قابلیت اطمینان اجتناب ناپذیر است. بر اساس این تفکر، اگر سرعت در اولویت باشد، احتمالاً قابلیت اطمینان آسیب خواهد دید و بالعکس.
با این حال، گروهی از محققان مستقر در مؤسسه فناوری ماساچوست (MIT) این مفهوم را به چالش می کشند و استدلال می کنند که شما واقعاً می توانید همه آن را داشته باشید. به گفته آماندا لیو، دانشجوی سال دوم کارشناسی ارشد در آزمایشگاه علوم کامپیوتر و هوش مصنوعی MIT (CSAIL)، با زبان برنامه نویسی جدیدی که به طور خاص برای محاسبات با کارایی بالا نوشتند، «سرعت و صحت لازم نیست با هم رقابت کنند. برعکس، در برنامه‌هایی که می‌نویسیم، می‌توانند کنار هم باشند». لیو و تیمش ماه گذشته در کنفرانس اصول زبان های برنامه نویسی در فیلادلفیا در مورد پتانسیل زبان تازه ایجاد شده A Tensor Language (ATL) صحبت کردند.
لیو می‌گوید: «همه چیز در زبان ما برای به دست آوردن یک عدد یا یک تانسور است.» تانسورها به نوبه خود تعمیم بردارها و ماتریس ها هستند. در حالی که بردارها اشیاء یک بعدی هستند (اغلب با فلش های منفرد نشان داده می شوند) و ماتریس ها آرایه های دو بعدی آشنا از اعداد هستند، تانسورها آرایه های n بعدی هستند که می توانند به شکل یک آرایه 3×3×3، به عنوان مثال، یا حتی شکل بگیرند. بعد بالاتر (یا کم)
ماهیت یک الگوریتم یا برنامه کامپیوتری شروع یک محاسبه خاص است. اما راه‌های مختلفی برای نوشتن این برنامه وجود دارد - همانطور که لیو و همکارانش در مقاله خود می‌نویسند، «تنوع شگفت‌انگیز اجرای کدهای مختلف» - که برخی از آنها به طور قابل توجهی سریع‌تر از بقیه هستند. او توضیح می‌دهد که دلیل اصلی پشت ATL این است: «با توجه به اینکه محاسبات با کارایی بالا بسیار نیازمند منابع است، شما می‌خواهید بتوانید برنامه‌ها را به شکلی بهینه تغییر دهید یا بازنویسی کنید تا سرعت کارها افزایش یابد. اغلب با برنامه‌ای شروع می‌کنید که نوشتن آن راحت‌تر است، اما ممکن است سریع‌ترین راه برای اجرای آن نباشد، بنابراین هنوز باید تنظیمات بیشتری انجام دهید."
زبان دستوری جدید مبتنی بر زبان Coq موجود است که شامل یک کمک کننده اثبات است. دستیار اثبات نیز به نوبه خود توانایی اثبات دقیق اظهارات خود را به صورت ریاضی دارد. Coq دارای ویژگی دیگری است که آن را برای گروه MIT جذاب کرده است: برنامه هایی که به آن زبان نوشته می شوند یا اقتباسی از آن همیشه پایان می یابند و نمی توانند به طور نامحدود در حلقه های بی نهایت اجرا شوند.
اکنون این اولین و تاکنون تنها زبان تانسور با بهینه‌سازی‌های رسمی تایید شده است. با این حال، تیم MIT هشدار می دهد که ATL هنوز فقط یک نمونه اولیه است - البته امیدوارکننده - که روی تعدادی از برنامه های کوچک آزمایش شده است.
همچنین بخوانید: