CPS Translations and Applications: The Cube and Beyond

Continuation passing style (CPS) translations of typed -calculi have numerous applications. However, the range of these applications has been confined by the fact that CPS translations are known for non-dependent type systems only, thus excluding well-known systems like the calculus of constructions (CC) and the logical frameworks (LF). This paper presents techniques for CPS translating systems with dependent types, with an emphasis on pure type-theoretical applications.In the first part of the paper we review several lines of work in which the need for CPS translations of dependent type systems has arisen, and discuss the difficulties involved with CPS translating such systems. One way of overcoming these difficulties is to work with so-called domain-free type systems. Thus, instead of Barendregt's -cube we shall consider the domain-free -cube, and instead of traditional pure type systems, we shall consider domain-free pure type systems.We therefore begin the second part by reviewing the domain-free -cube, which includes domain-free versions of CC and LF, and then present CPS translations for all the systems of the domain-free -cube. We also introduce Direct Style (DS) (i.e., inverse CPS) translations for all the systems of the domain-free -cube; such DS translations, which have been used in a number of applications, were previously formulated for untyped and simply-typed languages only.In the third part we review domain-free pure type systems and generalize the CPS translations of the domain-free -cube to a large class of domain-free pure type systems which includes most of the systems that appear in the literature, including those of the domain-free -cube. Many translations that appear in the literature arise as special cases of ours.In the fourth part of the paper we present two approaches to CPS translations of traditional pure type systems. The first, indirect, technique lifts the CPS translation of domain-free pure type systems to the analogous class of traditional pure type systems by using results that relate derivations in domain-free and traditional pure type systems. The second, direct, approach translates derivations, requiring a certain order on derivations to be well-founded. Both techniques yield translations for most of the systems that appear in the literature, including those of Barendregt's -cube.     

Retraction Approach to CPS Transform

We study the continuation passing style (CPS) transform and its generalization, the computational transform, in which the notion of computation is generalized from continuation passing to an arbitrary one. To establish a relation between direct style and continuation passing style interpretation of sequential call-by-value programs, we prove the Retraction Theorem which says that a lambda term can be recovered from its CPS form via a -definable retraction. The Retraction Theorem is proved in the logic of computational lambda calculus for the simply typable terms.     

From Reduction-based to Reduction-free Normalization

We present a systematic construction of a reduction-free normalization function. Starting from a reduction-based normalization function, i.e., the transitive closure of a one-step reduction function, we successively subject it to refocusing (i.e., deforestation of the intermediate reduced terms), simplification (i.e., fusing auxiliary functions), refunctionalization (i.e., Church encoding), and direct-style transformation (i.e., the converse of the CPS transformation). We consider two simple examples and treat them in detail: for the first one, arithmetic expressions, we construct an evaluation function; for the second one, terms in the free monoid, we construct an accumulator-based flatten function. The resulting two functions are traditional reduction-free normalization functions.The construction builds on previous work on refocusing and on a functional correspondence between evaluators and abstract machines. It is also reversible.     

CPS transformation of beta-redexes

The extra compaction of the most compacting CPS transformation in existence, which is due to Sabry and Felleisen, is generally attributed to (1) making continuations occur first in CPS terms and (2) classifying more redexes as administrative. We show that this extra compaction is actually independent of the relative positions of values and continuations and furthermore that it is solely due to a context-sensitive transformation of beta-redexes. We stage the more compact CPS transformation into a first-order uncurrying phase and a context-insensitive CPS transformation. We also define a context-insensitive CPS transformation that provides the extra compaction. This CPS transformation operates in one pass and is dependently typed.     

Compiling lazy functional programs to Java bytecode

The Java Virtual Machine (JVM) was designed as the target for Java compilers, but there is no reason why it cannot be used as the target for other languages. We describe the implementation of a compiler which translates a lazy, weakly‐typed functional program into Java class files. We compare the performance of our compiler to the only other known compiler from a lazy functional language to the JVM. The results are broadly similar, suggesting that to get a significant performance speed‐up using this compilation paradigm will come only from increasing the performance of the JVM, rather than enhancing the compiler itself. Copyright © 1999 John Wiley & Sons, Ltd.     

A New Approach to Parallelization of Serial Nested Loops Using Genetic Algorithms

Loop parallelization is an important issue in the acceleration of the execution of scientific programs. To exploit parallelism in loops a system of equations representing the dependencies between the loop iterations and a system of non-equations indicating the loop boundary conditions has to be solved. This is a NP-Complete problem. Our major contribution in this paper has been to apply genetic algorithm to solve system of equation and non-equation resulted from loop dependency analysis techniques to find two dependent loop iterations. We use distance vector to find the rest of dependencies.     

Secure Information Flow via Linear Continuations

Security-typed languages enforce secrecy or integrity policies by type-checking. This paper investigates continuation-passing style (CPS) as a means of proving that such languages enforce noninterference and as a first step towards understanding their compilation. We present a low-level, secure calculus with higher-order, imperative features and linear continuations.Linear continuations impose a stack discipline on the control flow of programs. This additional structure in the type system lets us establish a strong information-flow security property called noninterference. We prove that our CPS target language enjoys the noninterference property and we show how to translate secure high-level programs to this low-level language. This noninterference proof is the first of its kind for a language with higher-order functions and state.     

基于线性表出的非奇异循环变换局部性优化方法

开发程序的局部性是当今并行编译优化研究的重点之一，而程序变换是开发程序时间局部性和空间局部性的重要手段之一．该文提出了一种新的利用非奇异循环变换来优化程序局部性的局部性优化方法，即基于线性表出的循环变换．该方法利用一组最少的线性无关向量组来线性表出数组访问的下标表达式，并据此构造非奇异变换矩阵来优化数组访问的时间局部性和空间局部性．该方法能充分开发数组访问的时间局部性，能简便地确定是否能对数组访问进行时间局部性或空间局部性优化，并能对给定的嵌套循环同时进行时间局部性和空间局部性优化．实验结果表明了该文所提出的基于线性表出的非奇异循环变换局部性优化方法是有效的．     

Computer-generated Conversation Using Newspaper Headline

In this paper, the authors propose a method that incorporates mechanisms for handling ambiguity in speech and the ability of humans to create associations, and for formulating conversations based on rule base knowledge and common knowledge. Go beyond the level that can be achieved, using only conventional natural language processing and vast repositories of sample patterns. In this paper, the authors propose a method for computer conversation sentences generated using newspaper headlines as an example of how the common knowledge and associative ability are applied.     

Using Maude and Its Strategies for Defining a Framework for Analyzing Eden Semantics

Eden is a parallel extension of the functional language Haskell. On behalf of parallelism Eden overrides Haskell's pure lazy approach, combining a non-strict functional application with eager process creation and eager communication. We desire to investigate alternative semantics for Eden in order to analyze the consequences of some of the decisions adopted during the language design. In this paper we show how to implement in Maude the operational semantics of Eden in such a way that semantic rules can be modified easily. Moreover, other semantic features can be implemented by means of parameterized modules that allow to instantiate in different ways several parameters of the semantics but without modifying the semantic rules.     

Enhancing Text Retrieval by Using Advanced Stylistic Techniques

Text retrieval techniques have long focused on the topic of texts rather than the pragmatic role they play per se. In this article, we address two other aspects in text processing that could enhance text retrieval: (a) the detection of functional style in retrieved texts, and (b) the detection of writer"s attitude towards a given topic in retrieved texts. The former is justified by the fact that current text databases have become highly heterogeneous in terms of document inclusion, while the latter is dictated by the need for advanced and intelligent retrieval tools. Towards this aim, two generalised methodologies are presented in order to achieve the implementation of the findings in both aspects in text processing respectively. Particularly, the first one is fully developed and thus is analysed and evaluated in detail, while for the second one the theoretical framework is given for its subsequent computational implementation. Both approaches are as language independent as possible, empirically driven, and can be used, apart from information retrieval purposes, in various natural language processing applications. These include grammar and style checking, natural language generation, summarisation, style verification in real-world texts, recognition of style shift between adjacent portions of text, and author identification.     

基于时空双稀疏表示的成人ADHD脑网络检测与分析

注意力缺陷多动障碍（Attention deficit hyperactivity disorder,ADHD）主要表现为注意力分散、多动和冲动,是一种常见的精神障碍疾病.作为一种流行的脑功能成像技术,静息态功能核磁共振成像（Resting-state functional magnetic resonance imaging,rsfMRI）常应用于探索ADHD的神经机制.然而,由于rsfMRI数据的高维和少样本特性,采用传统的独立成分分析方法从rsfMRI数据中获得脑网络后,大多用基于体素级的方法进行推断,这难以检测出可靠的、与ADHD相关的脑网络.针对上述问题,本文提出了一种新颖的基于时空双稀疏表示（Dual temporal and spatial sparse representation,DTSSR）的方法和指标,以22名成人ADHD患者为研究对象,从大尺度脑网络级的角度检测出与ADHD相关的脑网络.首先采用DTSSR从ADHD的rsfMRI数据中提取出组脑网络及相应的耦合参数;然后将耦合参数均值池化作为网络的活跃度指标;最后,将活跃度指标与ADHD的量表分进行Spearman相关性分析,检测出与ADHD相关的脑网络.实验结果表明,背侧注意网络、执行控制网络的活跃度与ADHD量表分具有显著相关性.该结果在脑科学角度有合理的解释,且在不同字典尺寸下具有较高稳定性.本文所提方法,为探讨ADHD的潜在神经机制提供了一种新思路.     

Reasoning about programs in continuation-passing style

Plotkin's _v -calculus for call-by-value programs is weaker than the -calculus for the same programs in continuation-passing style (CPS). To identify the call-by-value axioms that correspond to on CPS terms, we define a new CPS transformation and an inverse mapping, both of which are interesting in their own right. Using the new CPS transformation, we determine the precise language of CPS terms closed under -transformations, as well as the call-by-value axioms that correspond to the so-called administrative -reductions on CPS terms. Using the inverse mapping, we map the remaining and equalities on CPS terms to axioms on call-by-value terms. On the pure (constant free) set of -terms, the resulting set of axioms is equivalent to Moggi's computational -calculus. If the call-by-value language includes the control operatorsabort andcall-with-current-continuation, the axioms are equivalent to an extension of Felleisenet al.'s _v -C-calculus and to the equational subtheory of Talcott's logic IOCC.This article is a revised and extended version of the conference paper with the same title [42]. The technical report of the same title contains additional material.The authors were supported in part by NSF grant CCR 89-17022 and by Texas ATP grant 91-003604014.