麻省理工為高性能計算機開發新的編程語言
在上月於費城舉辦的編程語言原理大會上，麻省理工學院（MIT）計算機科學與人工智能實驗室（CSAIL）二年級博士生Amanda Liu 表示，使用他們專為高性能計算而設計的新編程語言，可以很好地兼顧速度與正確性。此前人們普遍認為，速度與可靠性存在不可避免的權衡。
據悉，Liu 與加州大學伯克利分校博士後Gilbert Louis Bernstein、MIT 副教授Adam Chlipala 和助理教授Jonathan Ragan-Kelley 一道，描述了他們最近開發的“張量語言”（A Tensor Language）。
ATL 語言旨在產生一個數字或張量，所謂張量就向向量和矩陣的泛化。
向量是一維對象（通常由單獨的箭頭表示），矩陣是相對臉熟的二維數字數組。
而張量是n 維數組，例如可用3×3×3 的數組形式、或更高/ 更低的維度。
一個經過驗證的優化張量程序的框架（via）
計算機算法或程序的全部意義，在於啟動特定的計算。不過想要實現目的，可用諸多不同的方式來編寫。正如該研究團隊在即將發表的會議論文中所寫的那樣：
各種不同的代碼實現方式讓人眼花繚亂，某些方案的速度要快得多。
但鑑於高性能計算的資源開銷極其誇張，ATL 希望用更高效的方式來修改或重寫程序。
普通開發者習慣從最容易著手的地方開始編程，但這顯然沒有考慮到最佳的運行效率，因而需要進一步調整優化。
假設圖像由100×100 的數字數組表示，每個數字對應一個像素，且希望獲得這些數字的均值。
這項工作可通過兩階計算完成，首先確定每行的平均值，然後獲取每列的平均值。
ATL 提供了一個相關的工具包—— 計算機科學家稱之為“框架”—— 能夠展示如何將這兩個步驟轉換為更快的一步過程。
Liu 補充道：我們可藉助所謂的“證明助手”（proof assistant），來確保這種優化的正確性。
有鑑於此，團隊在現有的Coq 語言的基礎上構建了新語言。而其中包含的證明助手，具有以數學嚴謹的方式證明其斷言的內在能力。
不過在MIT 團隊看來，Coq 有另一個值得稱道的內在特性—— 用它編寫或適配的程序，是無法在無限循環中無止境地運行的。
舉個例子，用Java 編寫的程序，可能會發生這種狀況。我們運行一個程序來得到一個單一的答案—— 一個數字、或一個張量。
一個永不終止的程序，對我們說來毫無用處，但終止（terminate）是我們可使用Coq 免費獲得的一項特性。
只得一提的是，ATL 項目結合了Ragan-Kelley 和Chlipala 兩項研究的成果，前者長期持續關注著高性能計算背景下的算法優化。
與此同時，Chlipala 更關注算法優化的形式化（例如基於數學的驗證），但ATL 是兩者都首次合作—— Bernstein 和Liu 與去年攜手，並產出了ATL 這個成果。
據悉，ATL 是首個、也是迄今唯一一個具有正式驗證優化的張量語言。目前ATL 仍處於原型階段，但研究團隊已在許多小程序上展開了測試，可知其具有相當光明的前景。
展望未來，他們的主要目標之一是提升ATL 的可擴展性，以便它能夠用於我們在現實世界中看到的更大型的程序。
此前這些程序的優化工作，通常需要人工來完成。除了總有臨時需要解決的問題、還總涉及反复實驗，因而難免發生大量的錯誤。
好消息是，借助ATL，我們有望遵循一種更具原則的方法來重寫這些程序—— 且這麼做更加容易，也更能保證程序的正確性。