On equal \(\mu \)-terms
type: Item
instance of: scholarly article
title: On equal \(\mu \)-terms
zbMATH Open document ID: 1227.68041
author: Jörg Endrullis
author: Clemens Grabmayer
author: Jan Willem Klop
author: Vincent van Oostrom
published in: Theoretical Computer Science
publication date: 2011-07-07T00:00:00Z
review text: From the text: ``The paper studies a particular orthogonal higher-order rewrite system that we will call \(R_\mu\), containing terms built from some constants, variables, a binary function symbol \texttt{F}, and a higher-order symbol \(\mu\) allowing to construct terms such as \(\mu x. {\mathtt F}(x,{\mathtt c})\), where \texttt{c} is a constant. Everything in this paper generalizes to a more general first-order signature \(\Sigma\), but for our purposes, with recursive types as main application, the specific signature as mentioned will be assumed. There is a single rewrite rule, the \(\mu\)-rule, which reads \(\mu x.M \rightarrow M, x:=\mu x.M\) (in meta-notation using the schematic variable \(M\) and meta-substitution). The rewrite system \(R_\mu\) embodies the recursion principle in a most concentrated form, replacing the fixed point combinators \(Y\) as employed in \(\lambda\)-calculus. In fact, we can consider \(R_\mu\) to be a sub-calculus of \(\lambda\)-calculus, via the translation replacing \(\mu\) by \(Y\circ\mu\) for some fixed point combinator \(Y\); the \(\mu\)-rule then becomes a derived rule. [...] This translation preserves unsolvability; meaningless terms are carried over to unsolvables in the \(\lambda\)-calculus. Just as we can view \(\lambda\)-calculus from the finitary or the infinitary perspective, the latter leading to semantical notions such as Böhm trees, its subsystem \(R_\mu\) can also be viewed finitary or infinitary. The infinitary perspective of \(R_\mu\) is in fact rather well known, as it pertains to tree unwinding semantics of e.g. recursive types [\textit{H. P. Barendregt}, \textit{W. J. M. Dekkers} and \textit{R. Statman}, Lambda Calculus with Types. Perspectives in Logic. Cambridge: Cambridge University Press (2011; Zbl 1347.03001)]. The ensuing equality is called `strong equality' in [Barendregt et al., loc. cit.], holding when \(\mu\)-terms \(M,N\) have the same possibly infinite tree unwinding. There are many proof systems for …
reviewed by: Saeed Salehi
Mathematics Subject Classification ID: 68Q42
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 5918234
zbMATH Keywords: weak \(\mu\)-equality
zbMATH Keywords: strong \(\mu\)-equality
zbMATH Keywords: \(\alpha\)-equivalence
zbMATH Keywords: renaming
zbMATH Keywords: tree automata
MaRDI profile type: Publication
full work available at URL: j.tcs.2011.04.011
OpenAlex ID: W55323366
cites work: Rudiments of \(\mu\)-calculus
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Q3024900
cites work: Q4447227
cites work: Theoretical Computer Science
cites work: Q3839071
cites work: A duality in proof systems for recursive type equality and for bisimulation equivalence on cyclic term graphs
cites work: A duality between proof systems for cyclic term graphs
cites work: Automated Deduction – CADE-19
cites work: Rational rewriting
cites work: Q4355684
cites work: Context rewriting
cites work: Q4259973
cites work: Q4954449
cites work: Iterative Lexicographic Path Orders
cites work: Q3918095
cites work: Q4799892
DOI: 10.1016/J.TCS.2011.04.011
description: scientific article; zbMATH DE number 5918234