Essentially, in a reversible programming language, for each forward computation from state $S$ to state $S'$, there exists a constructive method to go backwards from state $S'$ to state $S$. Besides its theoretical interest, reversible computation is a fundamental concept which is relevant in many different areas like cellular automata, bidirectional program transformation, or quantum computing, to name a few.
In this work, we focus on term rewriting, a computation model that underlies most rule-based programming languages. In general, term rewriting is not reversible, even for injective functions; namely, given a rewrite step $t_1 \rightarrow t_2$, we do not always have a decidable method to get $t_1$ from $t_2$. Here, we introduce a conservative extension of term rewriting that becomes reversible. Furthermore, we also define two transformations, injectivization and inversion, to make a rewrite system reversible using standard term rewriting. We illustrate the usefulness of our transformations in the context of bidirectional program transformation.
Rewriting and narrowing for constructor systems with call-time choice semantics
非融合和非终止的基于构造函数的术语重写系统对于规范和编程的目的是有用的。特别地，现有的函数逻辑语言使用这种重写系统来定义可能不严格的非确定性函数。非确定性采用的语义是调用时间选择，其与非严格性的结合是一个重要的问题，多年前从语义的角度用基于构造器的重写逻辑（CRWL）解决，CRWL是一个众所周知的语义框架，通常被接受为现代函数逻辑语言的合适语义基础。CRWL的一个缺点是它没有一个正确的一步约简的概念，这对于理解和推理计算如何进行是非常有用的。在本文中，我们彻底发展的理论，一阶版本的让重写，一个简单的减少概念，接近经典的长期重写，但扩展了让绑定建设，充分表达结合调用时间的选择与非严格的语义。字母重写可以被看作是术语图重写的一种特殊的文本表示。我们调查的属性，让重写，最显着的等价性相对于一个保守的扩展的CRWL语义处理让绑定，我们通过一些案例研究表明，有两个可互换的正式意见（减少/语义）相同的语言是一个强大的推理工具。在此之后，我们提供了一个概念，让缩小，这是足够的调用时间的选择，证明了健全性和完整性的结果，让缩小让重写。此外，我们将这些let重写和let缩小关系（以及因此CRWL）与普通项重写和缩小（...）逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
Termination of canonical context-sensitive rewriting and productivity of rewrite systems
程序的终止，即，不存在无限的计算，确保了所有初始表达式的范式的存在，从而为函数式程序的规范化语义的定义提供了必要的成分。然而，在惰性函数式语言中，无限的数据结构通常作为计算的结果来交付。例如，所有素数的列表可以作为数值表达式或数据结构的永不结束的流返回。如果允许这样的流，要求终止是无望的。在这种情况下，生产力的概念可以用来提供一个无限数据结构计算的帐户，因为它“捕捉了可计算性的概念，无限列表程序的进展”（B.A. Sijtsma，On the Productivity of Recursive List Definitions，ACM Transactions on程序设计语言and Systems 11（4）：633-649，1989）。然而，在领域的长期重写系统，这可以被看作是（一阶，无类型，无条件）的功能程序，上下文敏感重写（CSR）的终止已被证明相当于重写系统的生产力，通过适当的转换。通过这种方式，可以使用证明CSR终止的工具来证明生产力。在术语重写中，CSR是当仅允许对函数符号的选定参数进行约简时产生的重写限制。在本文中，我们表明，众所周知的CSR的计算能力的结果是有用的，以更好地了解现有的重写系统的生产力和终止CSR之间的联系，并获得更强大的技术来证明重写系统的生产力。
On Complexity Bounds and Confluence of Parallel Term Rewriting
LIP (UMR CNRS/ENS Lyon/UCB Lyon1/Inria)（LIP（法国国家科学研究中心/里昂高等师范学院/里昂第一大学/法国国家信息与自动化研究所联合研究单位））；Birkbeck, University of London（伦敦大学伯贝克学院）；University Grenoble Alpes（格勒诺布尔阿尔卑斯大学）
