麻省理工为高性能计算机开发新的编程语言

据悉，Liu 与加州大学伯克利分校博士后 Gilbert Louis Bernstein、MIT 副教授 Adam Chlipala 和助理教授 Jonathan Ragan-Kelley 一道，描述了他们最近开发的“张量语言”（A Tensor Language）。

ATL 语言旨在产生一个数字或张量，所谓张量就向向量和矩阵的泛化。
向量是一维对象（通常由单独的箭头表示），矩阵是相对脸熟的二维数字数组。
而张量是 n 维数组，例如可用 3×3×3 的数组形式、或更高 / 更低的维度。

a verified framework for optimizing tensor programs（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，我们有望遵循一种更具原则的方法来重写这些程序 —— 且这么做更加容易，也更能保证程序的正确性。

推荐阅读