http://penrose.ink/siggraph20
我们介绍了一个名为Penrose的系统,用于创建数学图表(mathematical diagrams)。它的基本功能是用类似数学的表示法编写的抽象语句翻译成一个或多个可能的可视化表示。可视化表示不是依赖于固定的可视化工具库,而是使用由用户定义的基于约束的规范语言;然后通过约束数值优化(constrained numerical optimization)自动生成图表。该系统可由用户扩展到许多数学领域,并且速度足够快,可用于迭代设计探索。与通过直接操作或低级图形编程确定图表的工具不同,Penrose能够快速创建和探索图表,忠实地保留潜在的数学意义。我们通过展示如何使用该系统来说明数学和计算机图形学中的一组不同概念,来证明该系统的有效性和通用性。
CCS Concepts :
Human-centered computing ; Visualization toolkits
Software and its engineering ; Domain specific languages
“Mathematicians usually have fewer and poorer figures in their papers and books than in their heads.”
–William Thurston
数学思想的有效交流是学生、教育者和研究者面临的一个重大挑战。尽管现代数学对形式语言有着强烈的文化偏见,但可视化和图解无疑对数学进步有着同样深远的影响。然而,将抽象概念转化为具体插图的能力往往局限于少数对数学有深刻理解并熟悉图形工具的人。因此,图表在数学写作中相当稀少,例如,最近来自 arXiv 的数学论文平均每十页只有一个图像。这项工作的中心目标是降低将数学思想转化为有效、高质量的可视化图表的障碍。正如 TEX 和 LATEX 通过算法编纂专业排版的最佳实践,使数学写作平民化一样,Penrose旨在将数学插图画家的最佳实践编纂成可重用且可广泛访问的格式。
我们的方法植根于数学中抽象定义和具体表示之间的自然分离。尤其是,Penrose系统以数学对象到视觉图标的映射规范为中心(第2节)。此类映射通过反映熟悉数学符号的领域特定语言(DSL)表示,并可用于实现使用现有工具难以实现的新功能(第2.4节)。一个关键区别是Penrose程序编码一系列可能的可视化,而不是一个特定的图表。因此,在图表设计中投入的精力可以很容易地重用、修改和推广。这种方法有几个广泛的好处:
除了描述Penrose的实现之外,本文的目的是探索设计图表生成系统的一般挑战。因此,我们首先讨论系统设计的目标和权衡(第2节)。读者也可能会发现,定期参考第三、四节中给出的更详细但纯粹描述性的系统描述会有所帮助。
“One must be able to say at all times—instead of points, straight lines, and planes—tables, chairs, and beer mugs.”
–David Hilbert
我们的目标是建立一个系统,将抽象的数学思想转化为可视化的图表。关于系统设计的选择受到几个具体目标的指导,其中许多目标都得到了我们与图表工具用户进行的采访的支持:
为了实现这些目标,我们从通常手工绘制图表的方式中获得灵感。在数学的许多领域中,每种类型的对象都非正式地与一个标准的视觉图标相关联。例如,点是小点,向量是小箭头等等。为了生成图表,符号被系统地转换成图标;然后,一个图表绘制工具将这些图标以连贯的方式呈现在页面上。我们将此过程形式化,以便可以通过计算而不是手工生成图表。
Penrose的两个组织原则是:
- 通过从数学对象到可视图标的映射指定图表,以及
- 通过解决相关的约束优化问题来合成图表。
正如塞尔“中文室”的主人实际上并不懂一门外语一样,以这种方式设计的系统不需要对数学进行深入的推理,而只需要进行翻译。因此,我们并不期望我们的系统能够解决所有的图表设计难题。比如说,用户仍然要对,
同样,不能期望系统为了构造图表而解决困难的计算或数学问题(例如,停止问题或费马最后定理)。然而,尽管推理水平很浅,彭罗斯还是能够生成相当复杂的图表。事实上,即使在缺乏这种推理的情况下,单纯的可视化通常也能提供有用的观察结果
生成的系统将图表生成有效地建模为一个编译过程,其中编译目标是一个约束优化问题,而不是(比如)二进制可执行文件或静态图像。一旦编译完成,这个问题就可以用来生成可视化的图表;图3示出了高级系统流程。从编程语言的角度来看,在这个框架中表达的映射定义了一个可执行的可视语义。也就是说,它对以前只是抽象的逻辑关系给出了具体的、可视的和可计算的解释。
Penrose的一个主要决定是使用编程语言来指定数学对象(第2.1.2节)及其可视化表示(第2.1.3节)。图形化(例如,基于草图的)规范要求用户已经知道如何将抽象想法可视化,并将数学内容与特定的视觉表示联系起来,这与目标3相冲突。基于语言的规范提供了将内容与可视化分离所需的抽象级别。这项技术支持目标1,因为语言是表达数学思想最常用的手段。从系统设计的角度来看,基于语言的编码为识别和转换整个管道中的数学对象提供了统一的表示。此外,基于语言的接口使Penrose能够轻松地提供一个平台,在该平台上可以构建其他图表工具(如第4.5节或第5.7节)。一个权衡是,基于语言的方法要求用户用正式的数学或计算语言表达自己,这使得(比如)视觉艺术家和设计师更难做出新的表现。
第二个决定是将数学内容和可视化的规范划分为两种特定领域的语言:内容语言和风格语言。一个很好的类比是HTML和CSS之间的关系,前者指定内容,后者描述内容的呈现方式。名为Domain的模式(类似于XML或JSON模式)定义了感兴趣的数学域,支持目标2。根据目标3,该划分允许对不同的内容重复使用相同的样式,同样,相同的内容也可以以许多不同的样式显示。我们的目标是让这个部门支持一个生态系统,在这个生态系统中,新手用户可以从经验丰富的开发人员编写的包中获益(图5)。最后,与数学一样,采用用户定义的领域特定符号(第2.1.1节)的能力能够以简洁易懂的方式高效表达复杂关系[Kosar等人,2012]。直接在问题域的习惯用法中编码思想通常比在通用语言中(比如)一系列库调用能更好地理解程序[Van Deursen et al.2000]。我们将在第6节讨论我们语言的范围和局限性。
我们的主要目标之一(目标2)是建立一个统一的图表系统,而不是专注于特定领域(比如GraphViz或GroupExplorer)。统一的设计使来自不同域的对象能够共存于同一个图中,通常只需连接源文件即可(图6)。此外,投入(比如)改善系统性能或渲染质量的努力在许多不同领域中分摊。
用户可以通过编写所谓的Domain模式(第3.1节)在数学的任何领域工作,该模式定义了为给定域定制的DSL。这种设计还允许用户采用自己的符号和约定来对域进行建模。领域和用户特定符号的使用反映了数学写作中的常见做法,在数学写作中,符号的含义经常因上下文而过载。重要的是,域模式纯粹是抽象的:它不定义对象的内部表示,也不定义函数或谓词。这种抽象级别对于目标3至关重要,因为它允许多个视觉表示稍后应用于同一领域的对象。
要定义图表的内容,必须能够指定(i)图表中的对象,以及(ii)这些对象之间的关系。与目标1一致,Substance使用类似于标准数学散文的简明断言(例如见图7)。在形式上,它可以对任何可以用类型、函数和谓词组成的组合语言表达的域进行建模,这些是传统数学符号中的基本结构[Ganesalingam 2013]。正如定义在数学中通常是不变的一样,Substance从对象是无状态的强类型函数式语言(如ML[Milner et al.1997])中获得灵感。这种选择还简化了系统实现,因为编译器可以采用固定的定义。根据目标3,一个深思熟虑的设计决策是从Substance中排除所有图形数据(坐标、尺寸、颜色等),因为其唯一目的是指定抽象关系,而不是定量数据。所有这些数据都以Style指定或通过优化确定。这种划分将用户从繁琐和重复的图形编程中解脱出来,而且可以分解为可重用的Style代码。
现有的语言很难代替Substance使用,因为它们缺乏编码复杂逻辑关系所需的语义,并且不提供语言级别的可扩展性。例如,TEX和MathML标记提供的信息仅足以将纯文本转换为数学符号;像Mathematica和Maple这样的计算机代数系统有有限的类型系统,或者只提供一小部分固定谓词(例如,断言一个数字是实的)。相反,自动定理证明者和证明助手(如Coq[Bertot and Castéran 2013]和Lean[de Moura et al.2015])使用的更为丰富的语言对于简单地指定图表来说是过分的。自定义语言提供简单、熟悉的语法和清晰的错误消息。然而,我们确实采纳了Coq的一些想法,例如定制语法糖的能力(第3.1节)。
图表的意义主要通过相对关系而不是绝对坐标来表达。此外,图表通常是欠约束的:传达预期含义所需的关系决定了一系列可能的解决方案,而不是一个唯一的图表。因此,Style本着Sketchpad[Sutherland 1964]的精神,采用了基于约束的图形规范方法:图表是根据必须满足的硬约束和最小化的软惩罚(第3.3.6节)构建的,然后通过数值优化(第4节)解决未指定的数量。尽管仍然可以使用过程定义,但程序员不需要提供绝对坐标(如PostScript或OpenGL等命令式语言)。虽然隐式规范会使输出难以预测,但Penrose的部分魅力在于有可能找到有趣或令人惊讶的例子。此外,该方法产生更简洁的代码;例如,样式程序比它们生成的SVG文件要短得多。
另一种设计可能是使用应用程序编程接口(API),尽管从历史上看,规范语言出于很好的理由避免使用API。语言提供了更为简洁的复杂关系表达——想象一下通过DOM API的getElementById()和setStyle()方法设计整个网站的样式,而不是使用几行CSS。可视化编程语言(如LabView[Elliott et al.2007]或Grasshopper[McNeel et al.2010])可能足以满足基本规范(例如,向量应绘制为箭头),但不能扩展到更复杂的概念,这些概念很容易通过语言表达[Burnett et al.1995]。
一个关键的设计挑战是识别Substance程序中出现的对象。在一个给定的数学宇宙中,对象不仅可以通过其类型来区分,还可以通过它们与其他对象的关系来区分。一种广泛使用的指定这种关系的机制是通过类似CSS的选择器。Style采用类似的机制,对域模式中出现的类型、函数和谓词执行模式匹配(第3.3.1节)。
Penrose的第二个主要设计决策是使用约束优化来合成满足给定规范的图(第4节)。这种方法再次受到人们经常手工绘制图表(例如,使用基于GUI的工具)的启发:视觉图标被放置在画布上,并反复调整,直到无法进一步改进为止。在困难的情况下,图表绘制者可能会在细化最终设计之前尝试几种全局安排,但通常不会超过几个。自动化这个过程使得手工完成单调乏味的布局任务变得容易(图8)。
有充分的理由相信,基于优化的方法可以扩展到非常复杂的图。首先,有吸引力的图表不需要是全局最优的图表,它们不应该允许明显的局部改进,例如可以很容易地移动到它标记的项目附近的文本。事实上,不同的局部极小值可以提供有用的例子,帮助建立直觉(图9)。第二,与许多现代优化问题相比,即使是复杂的图表也有令人惊讶的少自由度(例如,数十或数百,而不是数千或数百万)。最后,专业图表设计人员使用的策略可以用于管理复杂性,例如独立优化图表的小组件(类似于非线性高斯-赛德尔),而不是同时优化所有自由度。
根据目标2和3,基于优化的方法可以通用地、自动地应用于任何用户定义的域和可视化表示,而无需程序员考虑布局过程的细节。在我们的系统中,优化问题是使用以Style定义的common-sense keywords(第3.3.6节),并将基本操作(如算术)链接在一起。由于图规范与解算器的细节无关,因此可以在系统的未来版本中更改和改进优化策略,同时保持与现有代码的兼容性。基于优化的方法的主要成本是它将系统设计的需求置于“上游”:用于定义视觉样式的所有表达式都必须是可微的。如第节所述。4.2,通过标准技术(例如,通过使用自动微分)基本上满足了这些要求。
一般来说,图优化本身就是一个具有挑战性的问题,我们当然不打算在本文中最终解决这个问题。目前,我们只使用一个通用的约束下降解算器(第4.2节)。然而,我们很高兴地发现,这种简单的方法可以处理来自不同领域的各种各样的示例,而不需要特定领域的策略。
Penrose中的最终设计决策是通过插件接口提供系统级的可扩展性,以调用Substance和Style上的外部代码。提供插件系统对于用户集成专门用于解决特定逻辑或图形挑战的外部代码至关重要。事实上,许多系统(例如TEX、Adobe Illustrator和TikZ的图形布局算法插件系统[Ellson et al.2001])已经提供了用于集成外部代码的此类接口。Penrose插件的接口设计为在Penrose系统和插件之间定义一个清晰而简单的边界,同时使每个组件能够专注于自己的优势。插件可以分析和扩充实质上定义的抽象对象集,也可以分析和扩充样式上的数字信息。这个简单的接口允许插件以任何语言编写(或从其他系统重新调整用途),并独立于Penrose的实现细节进行操作。然而,插件不能改变现有的实体或样式程序,也不能直接生成静态图形内容,因为这样的插件将放弃Penrose提供的好处,例如重新设置内容样式和避免使用绝对坐标的能力。图4说明了一个简单的插件如何利用实体和样式信息创建“响应”图。
在这里,我们考虑我们的系统设计如何与将抽象数学思想转换为可视化图表的其他系统相关联。其他类别的工具,如通用绘图工具(如Adobe Illustrator)也可用于绘制图表,但很快就会遇到障碍,例如用于大规模图表生成或改进现有大量图表的样式。我们在一项关于人们如何使用图表工具的试点研究中,对相关工作进行了更广泛的讨论。
有三种主要的系统可以将抽象形式的输入(例如,方程式或代码)转换为可视化表示。基于语言的系统,如TikZ[Tantau[n.d.](构建于TEX之上)是领域无关的,为视觉表示提供了极大的灵活性。他们对“数学式”语言的使用影响了Substance的设计。然而,现有的系统并不打算将数学内容与视觉表现分开。例如,TikZ与域和表示无关,因为它要求在较低级别(例如,单独的坐标和样式)指定图表,使得程序很难修改或重用。此外,由于只有肤浅的数学语义,因此很难在域级别对程序进行推理。
基于绘图的系统,如Mathematica和GeoGebra能够将标准数学表达式用作输入,并自动生成有吸引力的图表。正如图形计算器对于大多数数学专业的学生来说很容易挑选和使用一样,这些工具启发我们为Penrose提供了一种“分层”的方法,使得插图中专业知识较少的用户可以使用它(图5)。然而,很像一个图形计算器,这些系统中的视觉表示在很大程度上是“固定的”,容易访问的域集在很大程度上是固定的。例如,Mathematica不允许用户定义类型,要超越系统提供的可视化工具,必须提供低级指令(与TikZ等工具的精神相同)。
最后,graphviz和Geometry Constructions Language[Janičić2006]等系统将熟悉的领域特定语言转换为高质量的图表。在这里,领域相当狭窄,几乎没有机会扩展语言或定义新的可视化。然而,这些系统对各自领域的方便性和强大性启发我们构建一个具有更大可扩展性的系统。更广泛地说,虽然所有这些系统都与我们有一些共同的设计目标,但一个关键的区别是Penrose从一开始就被设计为一个可扩展的平台,用于构建图表工具,而不是一个单一的用户终端工具。
Penrose语言框架由三种扮演不同角色的语言组成:
由一个DOMAIN和一个或多个兼容STYLE程序组成的包可用于illustrate来自给定域的SUBSTANCE程序(图3)。尽管为第5节中讨论的示例提供了一些初学者软件包。Style和Domain的真正力量在于它们使PENROSE易于扩展。在本节中,我们通过线性代数包的运行示例来说明这些语言(图10到图12)。补充材料中给出了这三种语言的正式语法。
Domain schema通过定义可由相关Substance和Style程序使用的对象和符号来描述数学领域。线性代数的部分示例如图10所示(补充材料中提供了完整的模式)。type
行定义可用对象类型,function
行定义可用函数集的域和余域(其中*表示笛卡尔积),predicate
行定义对象之间可能的关系,包括一元谓词。重要的是,Domain schema纯粹是抽象的:它不为对象定义特定的表示,也不为函数或谓词定义主体。例如,我们这里没有说向量是由坐标列表编码的,也没有在这样的坐标上写加法运算。样式程序给出了这些定义的具体视觉解释(第3.3节)。可以通过构造函数为字段指定类型。比如说
constructor MakeInterval: Real min * Real max -> Interval
将min
和max
字段指定给可以从实体或样式程序访问的Interval
(例如,用于断言端点之间的关系)。通过Subtype <: Type
进行语法子类型化有助于通用编程。最后,notation
行定义了可简化代码的可选语法糖(如图11所示)。
Substance语言中的每个语句要么(i)声明一个对象,(ii)指定一个对象的属性,要么(iii)指定某个Domain模式中对象之间的关系。在数学中,并非所有属性都需要完全指定。例如,一个人可以谈论一个点而不给它明确的坐标。这些语句一起描述了一个包含所有已定义的数学对象和关系的上下文。
图11示出了Substance代码为一对向量指定属性和关系的示例。重要的是,这些陈述不会导致任何类型的数值计算。例如,没有为x1指定坐标以使其成为单位。事实上,向量空间X甚至没有显式维度。相反,语句指定持久和纯粹的符号关系,为可视化提供线索;具体坐标和属性稍后由布局引擎确定(第4节)。最后一行指定样式程序要使用的标签字符串,这里使用TEX表示法。图11,中心显示了该程序的“糖化”版本,使用域模式中定义的符号(图10)。用户可以任意方式编写程序,具体取决于其编辑器的功能(例如,对Unicode输入的支持)。
样式指定如何将Substance程序中的表达式转换为图形对象和关系。它是一种声明性规范语言,与CSS共享许多特性。核心原则是勾勒出基本规则(例如,基本类型的可视图标),然后通过级联(第3.3.2节)细化这些规则。每个规则都使用一个选择器对Substance代码中出现的对象和关系进行模式匹配(第3.3.1节)。然后,一系列声明指定了相应的可视化,例如,通过发出图形原语或强制执行约束。每个声明要么为字段赋值(第3.3.5节和第3.3.3节),要么指定约束或目标(第3.3.6节)。图12中显示了一个示例,它定义了图11中Substance程序使用的部分样式(补充材料中给出了完整样式)。我们将使用这个例子来强调该语言的基本特征。
选择器使用模式匹配来指定哪些对象将由规则设置样式。与正则表达式不同,选择器不匹配Substance代码的文字字符串,而是匹配此代码定义的上下文中的对象和关系。一个简单的例子是一个选择器,它匹配一个类型的每个实例,由forall
关键字表示。例如,第1行匹配所有向量空间。在随后的声明中,U
指的是来自Substance程序的向量空间X
。where
关键字将匹配限制为满足一个或多个关系的对象;例如,第37行匹配所有正交向量对。还可以使用倒勾按名称进行匹配;例如,第48行仅匹配向量x2
。选择器可以在将来进行丰富,以允许来自一阶逻辑的其他语句(例如∃, 析取和连接)。
布局引擎将Penrose代码转换为图像(图13)。有两个主要阶段:编译器(第4.1节)将代码转换为描述可能的图表的优化问题,然后求解器(第4.2节)生成该问题的解决方案。这些值用于呈现最终图表(第4.4节)。为了简单起见,我们的目标是自动生成一个静态图,但同样的管道可以扩展以支持交互等功能。
编译器的输入是三个文件:包含实体和样式程序的域模式。输出是一个约束优化问题,用计算图表示。
我们将每个输入文件解析为抽象语法树(AST),应用静态类型检查以确保类型格式正确,变量类型正确。我们首先对域程序进行类型检查,因为它定义了Substance和Style程序的有效类型,然后使用这些类型检查Substance程序和Style代码中的选择器。
AST被组合以定义对定义最终图的操作进行编码的计算图(图14)。为了构建这个图,我们应用了一个标准的模式匹配和级联过程:迭代样式程序中的规则,找到与选择器模式匹配的物质变量元组,然后根据匹配规则中的声明修改该图。例如,当来自图12的第一选择器VectorSpace U
与来自图11的变量X
匹配时,我们将节点添加到对该向量空间的轴进行编码的图中。通常,声明还可以从图中删除节点或连接以前添加的节点。一旦这个转换完成,我们就用具体的图形表示替换了所有抽象的数学描述。剩下的就是确定待定值(即由?
标记的值)和依赖于它们的值,这将由解算器完成。
为了对优化问题进行编码,我们将计算图中的术语收集到目标和约束图中(图15)。然后,用相应的数学表达式替换每个ensure
和encourage
语句。例如,ensure equal(x,y)
转换为约束
x
−
y
=
0
x−y=0
x−y=0,解算器会精确执行,而成encourage equal(x,y)
为目标
(
x
−
y
)
2
(x−y)^2
(x−y)2,解算器会尽可能将其最小化。总体约束集是所有约束的交集,总体目标是目标项的总和。目前Penrose提供了一组固定的约束和目标,尽管扩展样式以允许用户定义的内联表达式是很简单的。
编译器生成的优化图以标准形式描述了优化问题,即受等式和不等式约束的目标函数最小化[Boyd和Vandenberghe 2004,第4.1节]。这些问题可以用许多标准方法来解决。我们目前使用的是一种外部点法[Yamashita and Tanabe 2010],该方法从一个不可行点开始,并通过逐步严格的惩罚函数将其推向一个可行的配置,该惩罚函数反映了通常手动使用的过程(第2.2节)。此外,外部点方法是一个合适的选择,因为(i)可行的起点通常未知(图16),并且(ii)通过将约束转化为逐渐严格的惩罚函数,我们可以使用不直接支持约束优化的下降算法。特别是,我们使用L-BFGS和适合非光滑目标的线搜索策略[Lewis and Overton 2009]。鉴于我们的优化图结构丰富,可以链接回程序语义,因此有很多机会改进这一通用策略,例如将问题分解为可独立优化的较小部分,或使用SMT解算器找到可行的初始状态。
就像一个人类图表绘制者可能会考虑几个初始布局一样,我们随机抽取几个配置并只优化最有希望的配置,即在外部点问题中总体能量最小的配置。初始值从与其类型相关的范围内随机均匀采样;例如,RGB颜色值从[0,1]中采样。
由于我们的语言框架非常通用,程序员可能会定义困难或不可能的优化问题。因此,我们不能保证Penrose生成有效的图表。但是,如果任何约束值不为零,系统可以通过模拟打印错误消息来提供反馈。由此产生的无效图表甚至可以提供样式程序失败原因的有用视觉直觉(图2)。
在本文中,我们着重于生成二维矢量图形,但在原则上,我们的系统设计并没有将我们限制在这个特定的目标上。例如,基于约束的方法同样适用于(比如)生成可通过照片级真实感光线跟踪(Pharr et al.2016)渲染的3D对象排列,甚至可用于虚拟现实的约束交互图。在我们当前的实现中,图形原语通过React.js[Facebook 2020]转换为SVG本机原语,标签使用MathJax[Cervone 2012]从原始TEX路径后处理为SVG路径。由于Penrose代码通常非常简洁,因此我们将其作为元数据嵌入到SVG中,从而简化了可复制性。我们还嵌入了物质名称作为工具提示,以提高可访问性。
Penrose系统用Haskell编写,渲染前端用Typescript编写。我们使用Haskell库ad[Kmett 2015]编写了自己的求解器,以执行自动微分。我们提供一个输出目标和渲染器(SVG),以及一组固定的图形原语,这些原语松散地基于SVG(例如,圆和路径),以及SVG用户通常手动添加的功能,如箭头。我们还提供了一组固定的目标和约束,用于指定空间布局,例如形状包含和邻接关系,以及用于执行空间查询的其他函数,例如计算边界框和成对距离。用户社区的持续使用可能为标准库指明了方向。