检索结果-内蒙古大学图书馆

Generic recursive lens combinators and their calculation laws

THEORETICAL COMPUTER SCIENCE 2022年 913卷 113-137页

作者： Xie, Ruifeng Hu, Zhenjiang Peking Univ MoE Key Lab High Confidence Software Technol Beijing Peoples R China Peking Univ Sch Comp Sci Beijing Peoples R China

Bidirectional transformation is a generic method for synchronizing two related data structures, with applications in databases, software model transformation, graph transformation, etc. Since the data to synchronize often have complicated and disparate structures, bidirectional transformations are hard to develop, correctly comprehend, reason about, or maintain. programming language researchers have invested much efforts to invent new frameworks and paradigms, to aid the development of complex bidirectional transformations. However, these frameworks are not always applicable due to certain subtleties in the problem specification;some bidirectional programs become too complicated and unstructured to verify their correctness, not to mention their poor efficiency. In this paper, we propose a collection of generic recursion patterns for bidirectional transformations, and develop corresponding calculation laws. With these generic recursion patterns, we can develop structured bidirectional transformations, which are easy to understand and maintain. With these calculation laws, we can effectively optimize bidirectional programs, while preserving its very semantics. We demonstrate, through calculation of bidirectional transformations on trees, the expressiveness of the combinators and the effectiveness of the calculation laws. (c) 2022 Elsevier B.V. All rights reserved.

关键词： Bidirectional transformations Program calculation programming language theory

来源：评论

学校读者我要写书评

暂无评论

Divide-and-conquer checkpointing for arbitrary programs with no user annotation

引用

OPTIMIZATION METHODS & SOFTWARE 2018年第4-6期33卷 1288-1330页

作者： Siskind, Jeffrey Mark Pearlmutter, Barak A. Purdue Univ Sch Elect & Comp Engn W Lafayette IN 47907 USA Maynooth Univ Dept Comp Sci Maynooth Kildare Ireland

Classical reverse-mode automatic differentiation (AD) imposes only a small constant-factor overhead in operation count over the original computation, but has storage requirements that grow, in the worst case, in proportion to the time consumed by the original computation. This storage blowup can be ameliorated by checkpointing, a process that reorders application of classical reverse-mode AD over an execution interval to tradeoff space vs. time. Application of checkpointing in a divide-and-conquer fashion to strategically chosen nested execution intervals can break classical reverse-mode AD into stages which can reduce the worst-case growth in storage from linear to sublinear. Doing this has been fully automated only for computations of particularly simple form, with checkpoints spanning execution intervals resulting from a limited set of program constructs. Here we show how the technique can be automated for arbitrary computations. The essential innovation is to apply the technique at the level of the language implementation itself, thus allowing checkpoints to span any execution interval.

关键词： Reverse-mode automatic differentiation binomial checkpointing treeverse programming language theory compiler theory lambda calculus

来源：评论

学校读者我要写书评

暂无评论

THE STRUCTURE AND SEMANTICS OF ACTOR languageS

引用

SCHOOL/WORKSHOP ON RESEARCH AND EDUCATION IN CONCURRENT SYSTEMS ORIENTED languageS

作者： AGHA, G Department of Computer Science University of Illinois at Urbana-Champaign 1304 W. Springfield Avenue Urbana 61801 IL United States

ISBN: (纸本)354053931X

The actor model is developed as a foundation for concurrent object-oriented programming. The model provides for non-interference of state changes with multiple threads, inherent concurrency, reconfigurability, encapsulation of namespace, and weak fairness. The paper provides a survey of work in actor languages and can be divided into two areas: namely, formal aspects of the actor model and the structure of actor languages. We provide an abstract view of actor computations in terms of event diagrams and the laws of concurrent computing. The event diagrams can be given a semantics in terms of power domains. We then define the necessary constructs in a minimal actor language. This provides the building blocks for constructing a rich variety of concurrent computing structures. The second part of the paper shows how these higher level structures are built in terms of the actor primitives. In particular, this discussion illustrates how delayed evaluation, streams, continuations, higher-order functions, and other structures, can be built in terms of actor languages. We also note some experiences gained from the implementation of actor systems and argue for the potential advantages discovered by this work. Finally, we discuss some recent research on computational reflection. This work provides the ability to model control, and the ability to treat inheritance as a programmer defined method rather than a predefined linguistic object. The resulting flexibility is very much in the actor tradition of languages. © Springer-Verlag Berlin Heidelberg 1991.

关键词： CONCURRENCY MULTIPROCESSOR ARCHITECTURES OBJECT-ORIENTED programming programming language theory CONCURRENT programming STRUCTURES DISTRIBUTED SYSTEMS ACTORS

来源：评论

学校读者我要写书评

暂无评论

Distributive laws in programming structures

Distributive laws in programming structures

引用

作者： Rypacek, Ondrej University of Nottingham

学位级别：博士

Distributive laws in Computer Science are rules governing the transformation of one programming structure into another. In programming, they are programs satisfying certain formal conditions. Their importance has been to date documented in several isolated cases by diverse formal approaches. These applications have always meant leaps in understanding the nature of the subject. However, distributive laws have not yet been given the attention they deserve. One of the reasons for this omission is certainly the lack of a formal notion of distributive laws in their full generality. This hinders the discovery and formal description of occurrences of distributive laws, which is the precursor of any formal manipulation. In this thesis, an approach to formalisation of distributive laws is presented based on the functorial approach to formal Category theory pioneered by Lawvere and others, notably Gray. The proposed formalism discloses a rather simple nature of distributive laws of the kind found in programming structures based on lax 2-naturality and Gray's tensor product of 2-categories. It generalises the existing more specific notions of distributive laws. General notions of products, coproducts and composition of distributive laws are studied and conditions for their construction given. Finally, the proposed formalism is put to work in establishing a semantical equivalence between a large class of functional and object-based programs.

关键词： functional programming distributive laws category theory 2-categories mathematics of programming programming language theory theory of computation

来源：评论

学校读者我要写书评

暂无评论

ML Polymorphism of Linear Lambda Calculus with First-class Continuations 19

ML Polymorphism of Linear Lambda Calculus with First-class C...

引用

8th International Conference on Software and Computer Applications (ICSCA)

作者： Nishizaki, Shin-ya Tokyo Inst Technol 2-12-1 Ookayama Meguro Tokyo 1528552 Japan

ISBN: (纸本)9781450365734

The Curry-Howard isomorphism shows that an intuitionistic deductive system is similar to a formal computational system;propositions correspond to types, proofs to lambda-terms, and a proof normalization procedure to an evaluation strategy. Furthermore, the duality between computation values and continuations is discovered under the Curry-Howard isomorphism. In the traditional lambda calculus, duplication and erasing of values are allowed but those of continuations prohibited. On the other hand, in the lambda calculus with first-class continuations, both values and continuations are permitted to be duplicated and erased. In our previous paper, we proposed a linear lambda calculus with first-class continuations, in which we cannot duplicate and erase values but can do continuations. In this paper, we propose an ML polymorphic type system for the linear lambda calculus with first-class continuations and design a type inference algorithm of the type system.

关键词： programming language theory functional programming language lambda calculus linear logic continuations Curry-Howard isomorphism ML type system

来源：评论

学校读者我要写书评

暂无评论

EXPERIMENTAL PRE-PROCESSOR FOR ACTION-BASED COMPUTING

EXPERIMENTAL PRE-PROCESSOR FOR ACTION-BASED COMPUTING

引用

作者： ANNA SOKOLINSKAYA Tampere University of Technology

学位级别：硕士

The conventional programming paradigms were developed for the sequential model of computation. Concurrent computing is implemented through processes. Communication between processes is implemented manually, which leads to a number of problems. In response to this, the action-oriented paradigm was developed, as well as the tentative action language. This language features actions as the main entities of execution con- taining all the functionality of the program. Actions are not executed sequentially; in- stead the next action to be executed is selected non-deterministically by the scheduler, which is a part of the operating system. Implementing the action-oriented approach thoroughly requires the development of spe- cial hardware as well as the specially designed operating system. As this is not yet pos- sible, a simulation environment has been developed in order to test and explore the ac- tion-oriented paradigm. This environment requires the solutions to be written in C pro- gramming language, following the specific format understandable for the environment. This structure does not correspond to the structure of an action program, and the key entities of the action-oriented paradigm are hidden behind cumbersome C functions. This thesis presents a possible implementation of the simulation environment that pro- vides opportunities to explore and test the action paradigm in a more convenient and coherent way. The suggested environment is based on the existing framework. A partic- ular action language based on XML and C has been designed as a part of this thesis. As the implementation of the proposed environment is process-oriented on the low level, this language allows the user to write the functionality of the solutions in C language while maintaining the outline of an action program. XML syntax is used for the pro- posed action language in order to emphasize the hierarchical structure of an action pro- gram and utilize existing software tools to check, inspect and

关键词： concurrent computing action paradigm programming language theory

来源：评论

学校读者我要写书评

暂无评论

Linear Lambda Calculus with Non-linear First-class Continuations

Linear Lambda Calculus with Non-linear First-class Continuat...

引用

2017年第六届软件与计算机应用国际会议

作者： Shin-ya NISHIZAKI Tokyo Institute of Technology

The Curry-Howard isomorphism is the correspondence between propositions and types, proofs and lambda-terms, and proof normalization and evaluation. In Curry-Howard isomorphism, we find a duality between values and continuations in pure functional languages with respect to logical negation. My previous paper and other researchers' studies reveal that we can obtain a first-class continuation mechanism by providing duplicability and removability of continuations, which is equivalent to the rightcontraction and weakening rules in Gentzen's deductive system, the sequent calculus. In the lambda calculus, it is allowed to duplicate and remove values, but the continuations are impossible to duplicate and remove. In our previous paper, we showed that we can obtain the lambda calculus with first-class continuations providing duplicability and removability of both values and continuations. In this paper, we will study a calculus in which we only have duplicability and removability of continuations. We formalize this calculus in the framework of linear logic, which is a logical system sensitive to duplicability and removability, proposed by Jean-Yves Girard.

关键词： programming language theory functional programming language lambda calculus linear logic continuations

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：