使用sequent calculus作为编译器中间语言

32 浏览量更新于2024-07-14 收藏 477KB PDF 举报

"Sequent Calculus as a Compiler Intermediate Language - ICFP (2016) - 计算机科学" 这篇论文探讨了将sequent calculus（sequent演算）作为一种编译器中间语言的可能性。通常，λ-calculus（lambda演算）被广泛用作实践编译器的中间表示。然而，在逻辑学领域，还有一种与λ-calculus同时诞生但相对较少为人知的理论，即sequent calculus。作者Paul Downen、Luke Maurer、Zena M. Ariola以及Simon Peyton Jones提出了这个想法，探索sequent calculus是否也能作为有效的中间语言。 sequent calculus是逻辑学中的一个重要概念，它提供了一种形式化的推理系统，用于证明命题逻辑的正确性。与λ-calculus相比，sequent calculus在处理逻辑推理时具有不同的结构和规则，这可能使其在编译优化方面展现出独特的优点。论文中，作者设计了一个以sequent calculus为基础的实践导向的核心计算模型——Sequent Core。他们使用Sequent Core重新实现了Glasgow Haskell Compiler（GHC）的一部分功能。这表明，sequent calculus可以作为一种实用的中间表示，用于编译过程。文章的分类和主题包括编程语言的处理器部分——编译器，关键词涉及中间表示、自然推理、sequent calculus、编译器优化、延续和Haskell。 1. 引言 Steele和Sussman在他们的“Lambda是终极”系列论文中强调，λ-calculus不仅是计算的理论模型，而且是一种非常强大且实用的中间语言。论文作者受到这一观点的启发，研究如何将sequent calculus应用于实际编译器中，以测试其在编译和优化方面的潜力。通过Sequent Core，作者能够展示sequent calculus如何处理常见的编译任务，如控制流分析、优化和代码生成。这种新的中间语言可能会提供一种更直接的方式，来表达和操作程序的逻辑结构，从而在编译器优化过程中带来新的可能性。在后续的讨论中，论文可能详细分析了sequent calculus与λ-calculus在编译器设计中的差异，以及如何利用这些差异进行优化。此外，可能还讨论了在实现Sequent Core时遇到的挑战、解决方案以及与现有编译技术的比较。这篇论文为编译器设计提供了一个新颖的角度，探索了sequent calculus作为编译器中间语言的潜力，这对于编译器优化和语言设计的研究具有重要意义。

2.2 The Language

Having seen how Sequent Core is a language resembling an abstract

machine, let’s look more closely at the new linguistic concepts that

it introduces and how Sequent Core compares to Core. On closer

inspection, Sequent Core can be seen as a nuanced variation on

Core, separating the roles of distinct concepts of Core syntactically

as part of the effort to split calculations across the two sides of a cut

pair. More speciﬁcally, each construct of Core has an exact analogue

in Sequent Core, but the single grammar of Core expressions

divided among terms

, continuations

, and commands

in Sequent

Core. Additionally, Sequent Core has special support for labels and

direct jumps, which are not found in Core.

2.2.1 Terms and Continuations

Core expressions

, as shown in Figure 1, include a variety of

values (more speciﬁcally weak-head normal forms) which require

no further evaluation: lambdas (both small

and big

) and

applied constructors. Along with variables, these are all terms in

Sequent Core, as they do not involve any work to be done and they

immediately produce themselves as their result.

On the other hand, Core also includes expressions which do

require evaluation: function applications

e e

, polymorphic instan-

tiations

e τ

, and

case

expressions. Each of these expressions uses

something to create the next result, and thus these are reﬂected as

continuations

in Sequent Core. As usual, Sequent Core contin-

uations represent evaluation contexts that receive an input which

will be used immediately. For example, the application context

 1

where “



” is the hole where the input is placed, corresponds to the

call stack

1 · ret

. Furthermore, we can apply the curried function

λx.λy.x

to the arguments

and

by running it in concert with the

stack 1 · 2 · ret, as in:

hλx.λy.x || 1 · 2 · reti = hλy.1 || 2 · reti = h1 || reti

where ret signals a stop, so that the result 1 can be returned.

Since we are interested in modeling lazy functional languages,

we also need to include the results of arbitrary deferred computations

as terms in themselves. For example, when we perform the lazy

function composition

f (g x)

in Core,

g x

is only computed when

demands it. This means we need the ability to inject computations

into terms, which we achieve with

-abstractions. A

-abstraction

extracts a result from a command by binding the occurrences of

ret

in that command, so that anything passed to

ret

is returned from

the

-abstraction. However, because we are only modeling purely

functional programs, there is only ever one

ret

available at a time,

making it a rather limited namespace. Thus,

µret. hg || x · reti

runs

the underlying command, calling the function

with the argument

, so that whatever is returned by

pops out as the result of the

term. So lazy function composition can be written in Sequent Core

as hf || (µret. hg || x · reti) · reti.

Notice that every closed command must give a result to

ret

if it

ever stops at all. Another way of looking at this fact is that every

(ﬁnite) continuation has

ret

“in the tail”; it plays the role of “nil”

in a linked list. However, the return structure of continuations is

more complex than a plain linked list, since the terminating

ret

of a continuation may occur in several places. By inspection, a

continuation is a sequence of zero or more type or term applications,

followed by either

ret

itself or by a

case

continuation. But in the

latter case, each alternative has a command whose continuation must

in turn have

ret

in the tail. Unfortunately, this analogy breaks down

in the presence of local bindings, as we will see. Luckily, however,

viewing

ret

as a static variable bound by

-abstractions tells us

exactly how to “chase the tail” of a continuation by following the

normal rules of static scope. So we may still say that every closed

computation hv || ki eventually returns if it does not diverge.

2.2.2 Bindings and Jumps

There is one remaining Core expression to be sorted into the Sequent

Core grammar:

let

bindings. In Sequent Core,

let

bindings are

commands, as they set up an enclosing environment for another

command to run in, forming an executable code block. In both

representations,

let

bindings serve two purposes: to give a shared

name to the result of some computation, and to express (mutual)

recursion. Thus in the Sequent Core command

, we can share

the results of terms through

let x = v in c

and we can share a

continuation through

hµret.c || ki

. But something is missing. How

can we give a shared label to a command (i.e., to a block of code)

that we can go to during the execution of another command? This

facility is critical for maintaining small code size, so that we are not

forced to repeat the same command verbatim in a program.

For example, suppose we have the command

hz || case of Left(x) → c, Right(x) → ci

wherein the same

is repeated twice due to the

case

continuation.

Now, how do we lift out and give a name to

, given that it contains

the free variable

? We would rather not use a lambda, as in

λx.µret.c

, since that introduces additional overhead compared to

the original command. Instead, we would rather think of

as a sort

of continuation whose input is named

during execution of

. In

the syntax of

λµ˜µ

[

], this would be written as

˜µx.c

, the dual of

-abstractions. However, this is not like the other continuations we

have seen so far! There is no guarantee that

˜µx.c

uses its input

immediately, or even at all. Thus, we are not dealing with an

evaluation context, but rather an arbitrary context. Furthermore,

we might (reasonably) want to name commands with multiple

free variables, or even free type variables. So in actuality, we are

looking for a representation of continuations taking multiple values

as inputs of polymorphic types, corresponding to general contexts

with multiple holes.

This need leads us to multiple-input continuations, which we

write as

˜µ[a

, . . . , a

, x

, . . . , x

].c

in the style of

λµ˜µ

. These con-

tinuations accept several inputs (named

. . . x

), whose types are

polymorphic over the choice of types for

. . . a

, in order to run a

command

. Intuitively, we may also think of these multiple-input

continuations as a sequence of lambdas

Λa

. . . a

.λx

. . . x

except that the body is a command because it does not return.

The purpose of introducing multiple-input continuations was to

lift out and name arbitrary commands, and so they appear as a Se-

quent Core binding. Speciﬁcally, all multiple-input continuations

in Sequent Core are given a label

, as in the continuation binding

j = ˜µ[x, y]. h(+) || x · y · reti

. These labeled continuations serve

as join points: places where the control ﬂow of several diverging

branches of a program joins back up again.

In order to invoke a bound continuation, we can jump to it by

providing the correct number of terms for the inputs, as well as

explicitly specifying the instantiation of any polymorphic type in

System Fω style. For example, the command

let j = ˜µ[a:?, x:a, f:a → Bool ]. hf || x · reti

in jump j Bool True not

will jump to the label

with the inputs

Bool

True

, and

not

which results in

hnot || True · reti

. So when viewing Sequent Core

from the perspective of an abstract machine, its command language

provides three instructions: (1) set a binding with

let

, (2) evaluate

an expression with a cut pair, or (3) perform a direct jump.

Take note that a labeled continuation does not introduce a

binder. As a consequence, the occurrence of

ret

found in

j =

˜µ[x, y]. h(+) || x · y · reti

refers to the nearest surrounding

, unlike

the

ret

found in

f = λx.λy.µret. h(+) || x · y · reti

. Viewing

ret

as a statically bound variable means that labeled continuations

participate in the “tail chasing” discussed previously in Section 2.2.1.

剩余14页未读，继续阅读

weixin_38743076

粉丝: 7
资源: 925

使用sequent calculus作为编译器中间语言

STK-Disk913x-Integrating a 913X OPENstorage Disk - Sequent Envir

Python库 | sequent2-0.0.2.tar.gz

怎么使用nltk进行苏格拉底推论符号化及论证 python

multidict-6.0.2-cp39-cp39-win_amd64.whl

【图像融合】基于matlab小波变换灰色图像融合（含相关性、信噪比）【含Matlab源码 1841期】.md

VOS3000: 高效视频监控系统介绍及其部署指南

【医学图像分割】基于matlab磁共振成像 (MRI) 数值模拟平台【含Matlab源码 826期】.md

pyHook-1.5.1-cp36-cp36m-win_amd64.whl

e4c018e1-bc1a-45ce-a434-93f9285299721728807532179.mp4

llist-0.7.1-cp310-cp310-win_amd64.whl

最新资源