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

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

关键词：科学探索麻省理工为高性能计算机开发新的编程语言