On Nominal Syntax and Permutation Fixed Points

TL;DR

This paper introduces a new axiomatisation of alpha-equivalence for nominal terms using fixed-point constraints, improving unification behavior under equational theories like commutativity.

Contribution

It proposes a fixed-point based notion of alpha-equivalence and unification, enhancing finitary properties in the presence of equational theories such as commutativity.

Findings

Alpha-equivalence can be derived from permutation fixed-points.

Unification remains finitary with fixed-point constraints under certain theories.

Provides a sound and complete C-unification algorithm.

Abstract

We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a primitive notion of fixed-point constraint. We show that the standard freshness relation between atoms and terms can be derived from the more primitive notion of permutation fixed-point, and use this result to prove the correctness of the new $\alpha$-equivalence axiomatisation. This gives rise to a new notion of nominal unification, where solutions for unification problems are pairs of a fixed-point context and a substitution. Although it may seem less natural than the standard notion of nominal unifier based on freshness constraints, the notion of unifier based on fixed-point constraints behaves better when equational theories are considered: for example, nominal unification remains finitary in the presence of commutativity, whereas it becomes infinitary when unifiers are expressed using freshness contexts. We provide a definition of $\alpha$-equivalence modulo equational theories that take into account A, C and AC theories. Based on this notion of equivalence, we show that C-unification is finitary and we provide a sound and complete C-unification algorithm, as a first step towards the development of nominal unification modulo AC and other equational theories with permutative properties.

Tables

Table 1. Table 1. Simplification Rules. In ( ⋏ a ​ b ​ s ) 𝑎 𝑏 𝑠 (\curlywedge abs) and ( ≈ α ⋏ a ​ b ​ s ​ 2 ) subscript superscript 𝛼 absent 𝑎 𝑏 𝑠 2 (\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}abs2) , c 1 subscript 𝑐 1 c_{1} and c 2 subscript 𝑐 2 c_{2} are new names.

Table 2. Table 2. Simplification Rules for 𝖢 𝖢 \mathsf{C} -unification problems via 𝖢 𝖢 \mathsf{C} -fixed-point constraints. In rules ( ⋏ C a ​ b ​ s ) subscript 𝐶 𝑎 𝑏 𝑠 (\curlywedge_{C}abs) and ( ≈ α , 𝖢 ⋏ a ​ b ​ s ​ 2 ) subscript superscript 𝛼 𝖢 absent 𝑎 𝑏 𝑠 2 (\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}abs2) , c 1 subscript 𝑐 1 c_{1} and c 2 subscript 𝑐 2 c_{2} are newly generated names.

Equations

$$s,t:=a\mid [a]t\mid (t_1,\dots ,t_n)\mid {\mathsf{f}}^{\mathsf{E}}t\mid \pi \cdot X$$

$$\pi :=Id|(ab)\pi .$$

$$\begin{array}[]{@{\hspace{-1mm}}c@{\hspace{-.2mm}}c@{\hspace{-.2mm}}c}\begin{array}[]{c}(a\ b)\cdot a=b\\ (a\ b)\cdot b=a\\ (a\ b)\cdot c=c\end{array}&\begin{array}[]{c}(a\ b)\cdot(\pi\cdot X)=((a\ b)\circ\pi)\cdot X\\ (a\ b)\cdot\mathsf{f}\ t=\mathsf{f}\ (a\ b)\cdot t\\ (a\ b)\cdot(t_{1},\ldots,t_{n})=((a\ b)\cdot t_{1},\ldots,(a\ b)\cdot t_{n})\end{array}&\begin{array}[]{c}(a\ b)\cdot[a]t=[b](a\ b)\cdot t\\ (a\ b)\cdot[b]t=[a](a\ b)\cdot t\\ (a\ b)\cdot[c]t=[c](a\ b)\cdot t\\ \end{array}\end{array}$$

$$\sigma ::=id|[X\mapsto s]\sigma .$$

$$\begin{array}[]{cc}\begin{array}[]{c}a[X\mapsto s]=a\\ (\mathsf{f}\ t)[X\mapsto s]=\mathsf{f}(t[X\mapsto s])\\ ([a]t)[X\mapsto s]=[a](t[X\mapsto s])\end{array}&\begin{array}[]{c}(t_{1},\ldots,t_{n})[X\mapsto s]=(t_{1}[X\mapsto s],\ldots,t_{n}[X\mapsto s])\\ (\pi\cdot X)[X\mapsto s]=\pi\cdot s\\ (\pi\cdot Y)[X\mapsto s]=\pi\cdot Y\end{array}\end{array}$$

$$\begin{array}[]{c@{\hspace{1.1cm}}c@{\hspace{1.1cm}}c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 17.47658pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=34.95316pt\hbox{\kern 2.70003pt$(\mathbf{\#a})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Delta\vdash a\#b$}}}}\hfil\hskip 31.2982pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\pi^{-1}(a)\#X\in\Delta$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=56.08342pt\hbox{\kern 2.70003pt$(\mathbf{\#var})$}}}\hbox{\kern 2.6pt\hbox{$\displaystyle\Delta\vdash a\#\pi\cdot X$}}}}\hfil\hskip 31.2982pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 3.62502pt\hbox{$\displaystyle\penalty 1\Delta\vdash a\#t$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=41.59071pt\hbox{\kern 2.70003pt$(\mathbf{\#\mathsf{f}})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Delta\vdash a\#\mathsf{f}\ t$}}}}\\[15.49994pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Delta\vdash a\#t_{1}\quad\ldots\quad\Delta\vdash a\#t_{n}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=98.97658pt\hbox{\kern 2.70003pt$(\mathbf{\#tuple})$}}}\hbox{\kern 17.79535pt\hbox{$\displaystyle\Delta\vdash a\#(t_{1},\ldots,t_{n})$}}}}\hfil\hskip 31.2982pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 22.049pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=44.09799pt\hbox{\kern 2.70003pt$(\mathbf{\#[a]})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Delta\vdash a\#[a]t$}}}}\hfil\hskip 31.2982pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 4.43124pt\hbox{$\displaystyle\penalty 1\Delta\vdash a\#t$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=43.20317pt\hbox{\kern 2.70003pt$(\mathbf{\#abs})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Delta\vdash a\#[b]t$}}}}\end{array}$$

$$\text{ds}(\pi ,{\pi }^{\prime })\#X=\{a\#X|a\in \text{ds}(\pi ,{\pi }^{\prime })\}.$$

$$\begin{array}[]{c@{\hspace{1cm}}c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 18.86937pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=37.73874pt\hbox{\kern 2.70003pt$(\mathbf{\mathrel{{\approx}_{\scriptstyle{\alpha}}}a})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Delta\vdash a\mathrel{{\approx}_{\scriptstyle{\alpha}}}a$}}}}\hfil\hskip 28.45274pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 0.0016pt\hbox{$\displaystyle\penalty 1\texttt{ds}(\pi,\pi^{\prime})\#X\subseteq\Delta$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=67.19556pt\hbox{\kern 2.70003pt$(\mathbf{\mathrel{{\approx}_{\scriptstyle{\alpha}}}var})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Delta\vdash\pi\cdot X\mathrel{{\approx}_{\scriptstyle{\alpha}}}\pi^{\prime}\cdot X$}}}}\\[15.49994pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 6.00002pt\hbox{$\displaystyle\penalty 1\Delta\vdash t\mathrel{{\approx}_{\scriptstyle{\alpha}}}t^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=48.11014pt\hbox{\kern 2.70003pt$(\mathbf{\mathrel{{\approx}_{\scriptstyle{\alpha}}}\mathsf{f}})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Delta\vdash\mathsf{f}\ t\mathrel{{\approx}_{\scriptstyle{\alpha}}}\mathsf{f}\ t^{\prime}$}}}}\hfil\hskip 28.45274pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Delta\vdash t_{1}\mathrel{{\approx}_{\scriptstyle{\alpha}}}t_{1}^{\prime}\quad\ldots\quad\Delta\vdash t_{n}\mathrel{{\approx}_{\scriptstyle{\alpha}}}t_{n}^{\prime}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=105.28864pt\hbox{\kern 2.70003pt$(\mathbf{\mathrel{{\approx}_{\scriptstyle{\alpha}}}tuple})$}}}\hbox{\kern 6.23708pt\hbox{$\displaystyle\Delta\vdash(t_{1},\ldots,t_{n})\mathrel{{\approx}_{\scriptstyle{\alpha}}}(t_{1}^{\prime},\ldots,t_{n}^{\prime})$}}}}\\[15.49994pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 9.75731pt\hbox{$\displaystyle\penalty 1\Delta\vdash t\mathrel{{\approx}_{\scriptstyle{\alpha}}}t^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=55.62473pt\hbox{\kern 2.70003pt$(\mathbf{\mathrel{{\approx}_{\scriptstyle{\alpha}}}[a]})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Delta\vdash[a]t\mathrel{{\approx}_{\scriptstyle{\alpha}}}[a]t^{\prime}$}}}}\hfil\hskip 28.45274pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Delta\vdash\ s\mathrel{{\approx}_{\scriptstyle{\alpha}}}(a\ b)\cdot t\quad\Delta\vdash a\#t$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=110.15337pt\hbox{\kern 2.70003pt$(\mathbf{\mathrel{{\approx}_{\scriptstyle{\alpha}}}{\mathsf{a}b}})$}}}\hbox{\kern 27.92035pt\hbox{$\displaystyle\Delta\vdash[a]s\mathrel{{\approx}_{\scriptstyle{\alpha}}}[b]t$}}}}\end{array}$$

$$((\forall a\in A)\pi (a)=a)\Rightarrow \pi \cdot x=x$$

$${\text{supp}}_S(x):=\bigcap \{A\in \mathcal{P}(\mathbb{A})|A\text{mbox}isafinitesupportforx\}.$$

$$a\#X\Leftrightarrow\reflectbox{$\mathsf{N}$}a^{\prime}.(a\ a^{\prime})\cdot X=X.$$

$$\begin{array}[]{cccccccc}\pi^{\rho}:&A&\overset{\rho^{-1}}{\rightarrow}&A&\overset{\pi}{\rightarrow}&A&\overset{\rho}{\rightarrow}&A\\ &a&\mapsto&\rho^{-1}(a)&\mapsto&\pi(\rho^{-1}(a))&\mapsto&\rho(\pi(\rho^{-1}(a)))\end{array}$$

$$\begin{array}[]{l@{\hspace{1cm}}c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 8.91823pt\hbox{$\displaystyle\penalty 1\pi(a)=a$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=51.48132pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge a})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\pi\curlywedge a$}}}}\hfil\hskip 28.45274pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\texttt{supp}(\pi^{{\pi^{\prime}}^{-1}})\setminus\{\overline{c}\}\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=136.64139pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge var})$}}}\hbox{\kern 35.36932pt\hbox{$\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\pi\curlywedge\pi^{\prime}\cdot X$}}}}\\[15.49994pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 2.625pt\hbox{$\displaystyle\penalty 1\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\pi\curlywedge t$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=55.22403pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge\mathsf{f}})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\pi\curlywedge\mathsf{f}\ t$}}}}\hfil\hskip 28.45274pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\pi\curlywedge t_{1}\quad\ldots\quad\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\pi\curlywedge t_{n}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=130.24327pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge tuple})$}}}\hbox{\kern 25.61203pt\hbox{$\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\pi\curlywedge(t_{1},\ldots,t_{n})$}}}}\\[15.49994pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c},c_{1}.\pi\curlywedge(a\ c_{1})\cdot t$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=89.56096pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge abs})$}}}\hbox{\kern 14.91481pt\hbox{$\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\pi\curlywedge[a]t$}}}}\hfil\hskip 28.45274pt&\end{array}$$

$$\begin{array}[]{c@{\hspace{1cm}}c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 30.8897pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=61.77939pt\hbox{\kern 2.70003pt$(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\!a})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\ a\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}a$}}}}\hfil\hskip 28.45274pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\texttt{supp}((\pi^{\prime})^{-1}\circ\pi)\setminus\{\overline{c}\}\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=154.7927pt\hbox{\kern 2.70003pt$(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\!var})$}}}\hbox{\kern 31.77824pt\hbox{$\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\ \pi\cdot X\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\pi^{\prime}\cdot X$}}}}\\[15.49994pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 7.25002pt\hbox{$\displaystyle\penalty 1\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\ t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=74.65079pt\hbox{\kern 2.70003pt$(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\!\mathsf{f}})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\ \mathsf{f}\ t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\mathsf{f}\ t^{\prime}$}}}}\hfil\hskip 28.45274pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.t_{1}\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t_{1}^{\prime}\quad\ldots\quad\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.t_{n}\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t_{n}^{\prime}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=144.36993pt\hbox{\kern 2.70003pt$(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\!tuple})$}}}\hbox{\kern 16.0074pt\hbox{$\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.(t_{1},\ldots,t_{n})\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}(t_{1}^{\prime},\ldots,t_{n}^{\prime})$}}}}\\[15.49994pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 9.75731pt\hbox{$\displaystyle\penalty 1\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\ t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=79.66537pt\hbox{\kern 2.70003pt$(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\![a]})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\ [a]t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}[a]t^{\prime}$}}}}\hfil\hskip 28.45274pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\ s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}(a\ b)\cdot t\qquad\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c},c_{1}.(a\ c_{1})\curlywedge t$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=182.28407pt\hbox{\kern 2.70003pt$(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\!{\mathsf{a}b}})$}}}\hbox{\kern 51.96538pt\hbox{$\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\ [a]s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}[b]t$}}}}\end{array}$$

$$\text{supp}((\rho \circ {\pi }_1{)}^{-1}\circ {\pi }^{\rho }\circ (\rho \circ {\pi }_1))$$

$$=\text{supp}(({\pi }_1^{-1}\circ {\rho }^{-1}))\circ (\rho \circ \pi \circ {\rho }^{-1})\circ (\rho \circ {\pi }_1)$$

$$=\text{supp}({\pi }_1^{-1}\circ \pi \circ {\pi }_1)$$

$$\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c},c_{1}.\ \pi^{\rho}\curlywedge\rho\cdot((a\ c_{1})\cdot t^{\prime}).$$

$$(ac)⋏X$$

$$\displaystyle\Upsilon,\pi\curlywedge X\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\ \pi^{\prime}\curlywedge a$$

$$\displaystyle\Upsilon,\pi\curlywedge X\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\ \pi^{\prime}\curlywedge\pi_{1}\!\cdot\!X$$

$$\iff \text{supp}(({\pi }^{\prime }{)}^{{\pi }_1^{-1}})\setminus \{\overline{c}\}\subseteq \text{supp}(\text{perm}({\rm Y}{|}_X))(byassumption)$$

$$\displaystyle\Leftrightarrow\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\pi^{\prime}\curlywedge\pi_{1}\cdot X\hskip 113.81102pt(by~{}rule~{}(\mathbf{\curlywedge var}))$$

$$\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c},c_{1}.\pi\cdot((a\ c_{1})\cdot t^{\prime})\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}(a\ c_{1})\cdot t^{\prime}$$

$$\begin{array}[]{l@{\hspace{1cm}}c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 10.16823pt\hbox{$\displaystyle\penalty 1\pi(a)=a$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=53.98132pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge a})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\reflectbox{$\mathsf{N}$}\overline{c}.\Upsilon\vdash\pi\curlywedge a$}}}}\hfil\hskip 28.45274pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\texttt{supp}(\pi^{{\pi^{\prime}}^{-1}})\setminus\{\overline{c}\}\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=136.64139pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge var})$}}}\hbox{\kern 34.11932pt\hbox{$\displaystyle\reflectbox{$\mathsf{N}$}\overline{c}.\Upsilon\vdash\pi\curlywedge\pi^{\prime}\cdot X$}}}}\\[15.49994pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 2.625pt\hbox{$\displaystyle\penalty 1\reflectbox{$\mathsf{N}$}\overline{c}.\Upsilon\vdash\pi\curlywedge t$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=57.72403pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge\mathsf{f}})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\reflectbox{$\mathsf{N}$}\overline{c}.\Upsilon\vdash\pi\curlywedge\mathsf{f}\ t$}}}}\hfil\hskip 28.45274pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\reflectbox{$\mathsf{N}$}\overline{c}.\Upsilon\vdash\pi\curlywedge t_{1}\quad\ldots\quad\reflectbox{$\mathsf{N}$}\overline{c}.\Upsilon\vdash\pi\curlywedge t_{n}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=135.24327pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge tuple})$}}}\hbox{\kern 26.86203pt\hbox{$\displaystyle\reflectbox{$\mathsf{N}$}\overline{c}.\Upsilon\vdash\pi\curlywedge(t_{1},\ldots,t_{n})$}}}}\\[15.49994pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\reflectbox{$\mathsf{N}$}\overline{c},c_{1}.\Upsilon\vdash\pi\curlywedge(a\ c_{1})\cdot t$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=92.06096pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge abs})$}}}\hbox{\kern 14.91481pt\hbox{$\displaystyle\reflectbox{$\mathsf{N}$}\overline{c}.\Upsilon\vdash\pi\curlywedge[a]t$}}}}\hfil\hskip 28.45274pt&\end{array}$$

$$\begin{array}[]{l@{\hspace{1cm}}c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 2.29321pt\hbox{$\displaystyle\penalty 1\pi(a)=a$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=38.2313pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge a})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Upsilon\vdash\pi\curlywedge a$}}}}\hfil\hskip 28.45274pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\texttt{supp}(\pi^{{\pi^{\prime}}^{-1}})\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=115.14133pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge var})$}}}\hbox{\kern 31.24431pt\hbox{$\displaystyle\Upsilon\vdash\pi\curlywedge\pi^{\prime}\cdot X$}}}}\\[15.49994pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 2.625pt\hbox{$\displaystyle\penalty 1\Upsilon\vdash\pi\curlywedge t$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=41.974pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge\mathsf{f}})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Upsilon\vdash\pi\curlywedge\mathsf{f}\ t$}}}}\hfil\hskip 28.45274pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Upsilon\vdash\pi\curlywedge t_{1}\quad\ldots\quad\Upsilon\vdash\pi\curlywedge t_{n}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=103.74321pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge tuple})$}}}\hbox{\kern 20.23701pt\hbox{$\displaystyle\Upsilon\vdash\pi\curlywedge(t_{1},\ldots,t_{n})$}}}}\end{array}$$

$$tensy\text{vbox}spread0.0ptplus0.0001fil\text{penalty}1{\rm Y},(c_1{c}_2)⋏\text{Var}(t)⊢\pi ⋏(a{c}_1)\cdot tplus0.0001fil\text{vrule}height=0.25002pt,depth=0.25002pt,width=126.34453pt(⋏\mathbf{abs})where{c}_{1}and{c}_{2}arenewnames{\rm Y}⊢\pi ⋏[a]t$$

$$\begin{array}[]{cc}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 22.01468pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=44.02936pt\hbox{\kern 2.70003pt$(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\!a})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Upsilon\vdash a\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}a$}}}}&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\texttt{supp}((\pi^{\prime})^{-1}\circ\pi)\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=133.29263pt\hbox{\kern 2.70003pt$(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\!var})$}}}\hbox{\kern 29.90323pt\hbox{$\displaystyle\Upsilon\vdash\pi\cdot X\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\pi^{\prime}\cdot X$}}}}\\[15.49994pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 6.00002pt\hbox{$\displaystyle\penalty 1\Upsilon\vdash t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=54.40076pt\hbox{\kern 2.70003pt$(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\!\mathsf{f}})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Upsilon\vdash\mathsf{f}\ t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\mathsf{f}\ t^{\prime}$}}}}&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Upsilon\vdash t_{1}\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t_{1}^{\prime}\quad\ldots\quad\Upsilon\vdash t_{n}\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t_{n}^{\prime}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=117.86987pt\hbox{\kern 2.70003pt$(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\!tuple})$}}}\hbox{\kern 10.63239pt\hbox{$\displaystyle\Upsilon\vdash(t_{1},\ldots,t_{n})\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}(t_{1}^{\prime},\ldots,t_{n}^{\prime})$}}}}\\[15.49994pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 9.75731pt\hbox{$\displaystyle\penalty 1\Upsilon\vdash t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t^{\prime}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=61.91534pt\hbox{\kern 2.70003pt$(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\![a]})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Upsilon\vdash[a]t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}[a]t^{\prime}$}}}}&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Upsilon\vdash s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}(a\ b)\cdot t\quad\Upsilon,(c_{1}\ c_{2})\curlywedge\texttt{Var}(t)\vdash(a\ c_{1})\curlywedge t$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=192.3176pt\hbox{\kern 2.70003pt$(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\!{\mathsf{a}b}})$}}}\hbox{\kern 65.85716pt\hbox{$\displaystyle\Upsilon\vdash[a]s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}[b]t$}}}}\end{array}$$

$$\begin{array}[]{cccl}[\_]_{\curlywedge}:&\mathfrak{F}_{\#}&\longrightarrow&\mathfrak{F}_{\curlywedge}\\ &a\#X&\mapsto&(a\ c_{a})\curlywedge X\mbox{ where }c_{a}\mbox{ is a new name}.\end{array}$$

$$\begin{array}[]{cccl}[\_]_{\#}:&\mathfrak{F}_{\curlywedge}&\longrightarrow&\mathfrak{F}_{\#}\\ &\pi\curlywedge X&\mapsto&\texttt{supp}(\pi)\#X.\end{array}$$

$$(\forall a\in A,\pi (a)=a)\Rightarrow {\rm Y}⊢\pi ⋏t.$$

$$\text{for all X},{\Phi }_2⊢X{\sigma }_1{\sigma }^{\prime }{\stackrel{⋏}{\approx }}_{\alpha }X{\sigma }_2\text{and}{\Phi }_2⊢{\Phi }_1{\sigma }^{\prime }.$$

Full text

Work supported by FAPDF grant 193001369/2016. M. Ayala-Rincón partially funded by CNPq research grant number 307672/2017-4.

1. Introduction

This paper presents a new approach for the definition of nominal languages, based on the use of permutation fixed points. More precisely, we give a new axiomatisation of the $\alpha$-equivalence relation for nominal terms using permutation fixed-points, and revisit nominal unification in this setting.

In nominal syntax [UPG04], atoms are used to represent object-level variables and atom permutations are used to implement renamings, following the nominal-sets approach advocated by Gabbay and Pitts [Gab00, GP02, Pit13]. Atoms can be abstracted over terms; the syntax $[a]s$ represents the abstraction of $a$ in $s$. To rename an abstracted atom $a$ to $b$, a swapping permutation $\pi=(a\,b)$ is applied. Thus, the action of $\pi$ over $[a]s$, written as $(a\,b)\cdot[a]s$, produces the nominal term $[b]s^{\prime}$, where $s^{\prime}$ is the result of swapping $a$ and $b$ in $s$. The $\alpha$-equivalence relation between nominal terms is specified using swappings together with a freshness relation between atoms and terms, written $b\#s$, which roughly corresponds to $b$ not occurring free in $s$.

In this setting, checking $\alpha$-equivalence requires another first-order specialised calculus to check freshness constraints. For instance, checking whether $[a]s\approx_{\alpha}[b]t$ reduces to checking whether $s\approx_{\alpha}(b\,a)\cdot t$ and $a\#t$.

The action of a permutation propagates down the structure of nominal terms, until a variable is reached: permutations suspend over variables. Thus, $\pi\cdot s$ represents the action of a permutation over a nominal term, but is not itself a nominal term unless $s$ is a variable; for instance, $\pi\cdot X$ is a suspension (also called moderated variable), which is a nominal term.

The presence of moderated variables and atom-abstractions makes reasoning about equality of nominal terms more involved than in standard first-order syntax. For example, $\pi\cdot X\approx_{\alpha}^{?}\rho\cdot X$ is only true when $X$ ranges over nominal terms, say $s$, for which all atoms in the difference set of $\pi$ and $\rho$ (i.e., the set $\{a:\pi(a)\neq\rho(a)\}$) are fresh in $s$.

If the domain of a permutation $\pi$ is fresh for $X$ then $\pi\cdot X\mathrel{{\approx}_{\scriptstyle{\alpha}}}Id\cdot X$. Thus a set of freshness constraints (i.e., a freshness context) can be used to specify that a permutation will have no effect on the instances of $X$. This is why in nominal unification [UPG04], the solution for a problem is a pair consisting of a freshness context and a substitution.

The use of freshness contexts is natural when dealing with “syntactic” nominal unification, but in the presence of equational axioms (i.e., equational nominal unification) it is not straightforward. For example, in the case of $\mathsf{C}$-nominal unification (nominal unification modulo commutativity), to specify that a permutation has no effect on the instances of $X$ modulo $\mathsf{C}$, in other words, to specify that the permutation does not affect a given $\mathsf{C}$-equivalence class, we need something more than a freshness constraint (note that $(a\ b)\cdot(a+b)=b+a=_{\mathsf{C}}a+b$, so the permutation $(a\ b)$ fixes the term $a+b$, despite the fact that $a$ and $b$ are not fresh).

In this paper, we propose to axiomatise $\alpha$-equivalence of nominal terms using permutation fixed-point constraints: we write $\pi\curlywedge t$ (read “$\pi$ fixes $t$”) if $t$ is a fixed-point of $\pi$. We show how to derive fixed-point constraints $\pi\curlywedge t$ from primitive constraints of the form $\pi\curlywedge X$, and show the correctness of this approach by proving that the $\alpha$-equivalence relation generated in this way coincides with the one axiomatised via freshness constraints. We then show how fixed-point constraints can be used to specify $\alpha$-equivalence modulo equational theories containing $\mathsf{A}$, $\mathsf{C}$, and $\mathsf{AC}$ operators, and provide an algorithm to solve nominal unification problems modulo $\mathsf{C}$, which outputs a finite set of most general solutions.

Related Work

Equational reasoning has been extensively explored since the early development of modern abstract algebra (see, e.g., the $E$-unification surveys by Siekmann [Sie90] and Baader et al [BS94] and [BSN*+*01]). For $\mathsf{AC}$-equality checking, $\mathsf{AC}$ matching and $\mathsf{AC}$ unification, refined techniques have been applied. For instance, $\mathsf{AC}$-equality check and linear $\mathsf{AC}$-matching problems can be reduced to searching a perfect matching in a bipartite graph [BKN87], whereas $\mathsf{AC}$ unification problems can be reduced to solving a system of Diophantine equations [Sti81, Fag87].

Techniques to deal with $\alpha$-equivalence modulo the equational theories $\mathsf{A}$, $\mathsf{C}$ and $\mathsf{AC}$ were proposed in [AdCSFN17, AdCSMFR19, ARdCSFNS17, ARdCSFNS18], using the standard nominal approach via freshness constraints. Solving nominal $\mathsf{C}$-unification problems requires to deal with fixed-point equations, for which there is no finitary representation of the set of solutions using only freshness constraints and substitutions [ARdCSFNS17, ARdCSFNS18]. A combinatorial algorithm permits to find all the solutions of fixed-point equations [ARdCSFNS18].

Fixed-point constraints arise also in other contexts: Schmidt-Schauß  et al [SKLV17] show how nominal unification problems in a language with recursive let operators give rise to freshness constraints and nominal fixed-point equations. The approach to nominal unification via permutation fixed-points proposed in this paper could also be used to reason about equality in this language.

This paper is a revised and extended version of [AFN18], where nominal terms with fixed-point permutation constraints were first presented. In this paper we prove the correctness of the approach, by showing it is equivalent to the standard presentation via freshness constraints. We also provide proofs of soundness and completeness of the unification algorithm. A generalisation of the notion of $\alpha$-equivalence to take into account equational theories including $\mathsf{A}$, $\mathsf{C}$ and $\mathsf{AC}$ is also provided (only $\mathsf{C}$ was considered in [AFN18]), as well as a $\mathsf{C}$-unification algorithm.

Overview

The paper is organised as follows. Section 2 provides the necessary background material on nominal syntax and semantics. Section 3 introduces fixed-point constraints and $\alpha$-equivalence, and shows that these relations behave as expected. In particular, we show that there is a two-way translation between the freshness-based $\alpha$-equivalence relation and its permutation fixed-point counter-part, which confirms that the fixed-point approach is equivalent to the standard approach via freshness constraints. Section 4 presents a nominal unification algorithm specified by a set of simplification rules, and proves its soundness and completeness. In Section 5 we generalise the approach to take into account equational theories: we define a notion of permutation fixed-point $\alpha$-equivalence modulo $\mathsf{A}$, $\mathsf{C}$ and $\mathsf{AC}$ theories, and develop a $\mathsf{C}$-unification algorithm. Finally, Section 6 concludes and discusses future work.

2. Preliminaries

Let $\mathbb{A}$ be a fixed and countably infinite set of elements $a,b,c,\ldots$, which will be called atoms (atomic names). A permutation on $\mathbb{A}$ is a bijection on $\mathbb{A}$ with finite domain.

Fix a countably infinite set $\mathcal{X}=\{X,Y,Z,\ldots\}$ of variables and a countable set $\mathcal{F}=\{\mathsf{f},\mathsf{g},\ldots\}$ of function symbols.

{defi}

[Nominal grammar] Nominal terms are generated by the following grammar.

[TABLE]

where $a$ is an atom term, $[a]t$ denotes the abstraction of the atom $a$ over the term $t$, $(t_{1},\ldots,t_{n})$ is a tuple, function symbols are equipped with an equational theory $\mathsf{E}$, hence $\mathsf{f}^{\mathsf{E}}\ t$ denotes the application of $\mathsf{f}^{\mathsf{E}}$ to $t$ and $\pi\cdot X$ is a moderated variable or suspension, where $\pi$ is an atom permutation. We write $\mathsf{f}^{\emptyset}$, or simply $\mathsf{f}$, to emphasise that no equational theory is assumed for $\mathsf{f}$, that is, $\mathsf{f}$ is just a function symbol.

We follow the permutative convention [GM08, Convention 2.3] for atoms throughout the paper, i.e., atoms $a,b,c$ range permutatively over $\mathbb{A}$ so that they are always pairwise different, unless stated otherwise.

Atom permutations are represented by finite lists of swappings, which are pairs of different atoms $(a\ b)$; hence, a permutation $\pi$ is generated by the following grammar:

[TABLE]

where $Id$ is the identity permutation, usually omitted from the list of swappings representing a permutation $\pi$. Suspensions of the form $Id\cdot X$ will be represented just by $X$. We write $\pi^{-1}$ for the inverse of $\pi$, and use $\circ$ to denote the composition of permutations. For example, if $\pi=(a\ b)(b\ c)$ then $\pi(c)=a$ and $c=\pi^{-1}(a)$.

The difference set of two permutations $\pi$, $\pi^{\prime}$ is $\texttt{ds}(\pi,\pi^{\prime})=\{a\mid\pi(a)\neq\pi^{\prime}(a)\}$.

We write $\texttt{Var}(t)$ for the set of variables occurring in $t$. Ground terms are terms without variables, that is, $\texttt{Var}(t)=\emptyset$. A ground term may still contain atoms, for example $a$ is a ground term and $X$ is not.

{defi}

[Permutation action] The action of a permutation $\pi$ on a term $t$ is defined by induction on the number of swappings in $\pi$:

$Id\cdot t=t$ and $((a\ b)\pi)\cdot t=(a\ b)\cdot(\pi\cdot t),$ where

[TABLE]

{defi}

[Substitution] Substitutions are generated by the grammar

[TABLE]

Postfix notation is used for substitution application and $\circ$ for composition: $t(\sigma\circ\sigma^{\prime})=(t\sigma)\sigma^{\prime}$. Substitutions act on terms elementwise in the natural way: $t\ id=t,\ t[X\mapsto s]\sigma$ $=$ $(t[X\mapsto s])\sigma$, where

[TABLE]

The following well-known property of substitution and permutation justifies the notation $\pi\cdot s\sigma$ (without brackets), see  [UPG04] for more details.

Lemma 1**.**

Substitution and permutation commute: $\pi\cdot(s\sigma)=(\pi\cdot s)\sigma$.

2.1. Alpha-equivalence via freshness constraints

In the standard nominal approach (see, e.g.,  [Pit03, UPG04, FG07]), the $\alpha$-equivalence relation $s\mathrel{{\approx}_{\scriptstyle{\alpha}}}t$ is defined using a freshness relation between atoms and terms, written $a\#t$ – read “$a$ fresh for $t$” – which, intuitively, corresponds to the idea of an atom not occurring free in a term. These relations are axiomatised using the rules in Figures 1 and 2, respectively.

We call $s\mathrel{{\approx}_{\scriptstyle{\alpha}}}t$ and $a\#t$ $\alpha$-equality and freshness constraints, respectively. Note that to define $\mathrel{{\approx}_{\scriptstyle{\alpha}}}$ we use the difference set of two permutations in rule $(\mathbf{\mathrel{{\approx}_{\scriptstyle{\alpha}}}var})$; we denote by $\texttt{ds}(\pi,\pi^{\prime})\#X$ the following set of freshness constraints:

[TABLE]

The symbols $\Delta$ and $\nabla$ denote freshness contexts, which are sets of freshness constraints of the form $a\#X$. The domain of a freshness context $\Delta$, denoted by $\texttt{dom}(\Delta)$, consists of the atoms occurring in $\Delta$; $\Delta|_{X}$ consists of the restriction of $\Delta$ to the freshness constraints on variable $X$, that is, the set $\{a\#X\ |\ a\#X\in\Delta\}$.

2.2. Nominal sets and support

Let $S$ be a set equipped with an action of the group $\texttt{Perm}(\mathbb{A})$ of finite permutations of $\mathbb{A}$.

{defi}

A set $A\subset\mathbb{A}$ is a support for an element $x\in S$ if for all $\pi\in\texttt{Perm}(\mathbb{A})$, the following holds

[TABLE]

A nominal set is a set equipped with an action of the group $\texttt{Perm}(\mathbb{A})$, that is, a $\texttt{Perm}(\mathbb{A})$-set, all of whose elements have finite support.

As in [Pit13], we denote by $\texttt{ supp}_{S}(x)$ the least finite support of $x$, that is,

[TABLE]

We write $\texttt{supp}(x)$ when $S$ is clear from the context. Clearly, each $a\in\mathbb{A}$ is finitely supported by $\{a\}$, therefore $\texttt{supp}(a)=\{a\}$.

2.3. The “new” quantifier

In Nominal Logic [Pit03], the “new” quantifier

$\mathsf{N}$

is used to quantify over new names. Given two elements $x$, $y$ of a nominal set, write $x\#y$ as an abbreviation of $\texttt{supp}(x)\cap\texttt{supp}(y)=\emptyset$; then \reflectbox{\mathsf{N}}a.P(a,x) (read “for some/any new atom $a$, $P(a,x)$”) abbreviates $\forall a\in\mathbb{A}.a\#x\Rightarrow P(a,x)$ or equivalently $\exists a\in\mathbb{A}.a\#x\wedge P(a,x)$ (see Theorem 3.9 in [Pit13] for more details).

Intuitively, the “new” quantifier is used to indicate that a predicate holds for some (any) new atoms. The formula \reflectbox{\mathsf{N}}a.\phi means “for a fresh name $a$, $\phi$ holds”. Since there is an infinite supply of names and elements of nominal sets have a finite support, it is always possible to pick a fresh name. Moreover, it can be shown that if a property $\phi(a)$ holds for some fresh name $a$ then it holds for all fresh names, so the way in which the fresh atom is chosen is not important.

In proof systems for Nominal Logic, several approaches have been proposed to define rules to introduce and eliminate the

$\mathsf{N}$

quantifier (see, e.g., [Pit03, Che05, CU08]). We follow Cheney’s approach [Che05], where the formula \reflectbox{\mathsf{N}}a.\phi (read “$a$ is a newly quantified atom in $\phi$”) is well formed if $\phi$ is a well-formed formula and $a\in\mathbb{A}$ is semantically fresh. In other words, the introduction of a

$\mathsf{N}$

quantifier for $a$ in a formula $\phi$ requires $a$ to be a new atom, fresh for all the variables in $\phi$ (see [Che05], Figure 5, where the well-formedness rules are given). We implicitly assume that $a$ is a newly generated atom when we introduce

$\mathsf{N}$

in our formulas in the next section. Operationally, proving a formula \reflectbox{\mathsf{N}}a.\phi boils down to picking a fresh atom $c$ and proving that $\phi$ holds when the occurrences of $a$ are replaced by the fresh atom $c$.

3. Fixed-point Constraints

The native notion of equality on nominal terms is $\alpha$-equivalence, written $s\mathrel{{\approx}_{\scriptstyle{\alpha}}}t$. As mentioned in section 2.1, this relation is usually axiomatised using the freshness relation between atoms and terms. The notion of freshness is derived from the notion of support, which in turn is defined using permutation fixed-points (see Definition 2.2). We can define freshness using the quantifier

$\mathsf{N}$

combined with a notion of fixed-point, as shown by Pitts [Pit13] (page 53):

[TABLE]

In this paper, instead of defining $\alpha$-equivalence using freshness, we define it using the more primitive notion of fixed-point under the action of permutations. We will denote this relation $\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$, and show that it coincides with $\mathrel{{\approx}_{\scriptstyle{\alpha}}}$ on ground terms, i.e., the relation defined using permutation fixed points corresponds to the relation defined using freshness. For non-ground terms, there is also a correspondence, but under different kinds of assumptions (fixed-point constraints vs. freshness constraints).

3.1. Fixed-points of permutations and term equality

We start by defining a binary relation that describes which elements of a nominal set $S$ are fixed-points of a permutation $\pi\in\texttt{Perm}(\mathbb{A})$:

{defi}

[Fixed-point relation]

Let $S$ be a nominal set. The fixed-point relation $\curlywedge\subseteq\texttt{Perm}(\mathbb{A})\!\times\!S$ is defined as: $\pi\curlywedge x\Leftrightarrow\pi\cdot x=x.$ Read “$\pi\curlywedge x$” as “$\pi$ fixes $x$”.

It is easy to see that if $\texttt{dom}(\pi)\cap\texttt{supp}(x)=\emptyset$ then $\pi\curlywedge x$ holds (this follows directly from the definition of support, see Definition 2.2). However, the other direction does not hold in general. For example, consider expressions built using atoms and a binary commutative operator $+$; the permutation $\pi=(a\ b)$ fixes the equivalence class of the expression $a+b$ despite the fact that its support coincides with $\texttt{dom}(\pi)$.

Permutation fixed-points will play an important role in the definition of $\alpha$-equality of nominal terms. Below we define fixed-point constraints and equality constraints using predicates $\curlywedge$ and $\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$ and then give deduction rules to derive fixed-point and equality judgements.

Intuitively, for $s$ and $t$ ground nominal terms

• •

$s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t$ will mean that $s$ and $t$ are $\alpha$-equivalent, i.e., equivalent modulo renaming of abstracted atoms.

• •

$\pi\curlywedge t$ will mean that the permutation $\pi$ fixes the nominal term $t$, that is, $\pi\cdot t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t$. This means that $\pi$ has “no effect” on $t$ except for the renaming of bound names, for instance, $(a\ b)\curlywedge[a]a$ but not $(a\ b)\curlywedge\mathsf{f}\ a$.

In the case of non-ground terms, a fixed-point or $\alpha$-equality constraint has to be evaluated in a context, which provides information about permutations that fix the variables.

{defi}

[Fixed-point and equality constraints] A fixed-point constraint is a pair $\pi\curlywedge t$ of a permutation $\pi$ and a term $t$. An $\alpha$-equivalence constraint is a pair of the form $s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t$.

We call a fixed-point constraint of the form $\pi\curlywedge X$ a primitive fixed-point constraint and a finite set of such constraints is called a fixed-point context. $\Upsilon,\Psi,\ldots$ range over fixed-point contexts.

We write $\pi\curlywedge\texttt{Var}(t)$ as an abbreviation for the set of constraints $\{\pi\curlywedge X\mid X\in\texttt{Var}(t)\}$.

We now introduce some notation:

The set $\texttt{Var}(\Upsilon)$ of variables is defined as expected: it contains all the variables mentioned in the fixed-point context $\Upsilon$.

The set of permutations of a fixed-point context $\Upsilon$ with respect to the variable $X\in\texttt{Var}(\Upsilon)$, denoted by $\texttt{perm}(\Upsilon|_{X})$, is defined as $\texttt{perm}(\Upsilon|_{X}):=\{\pi\ |\ \pi\curlywedge X\in\Upsilon\}$.

For a substitution $\sigma$ and a fixed-point context $\Upsilon$ we define $\Upsilon\sigma:=\{\pi\curlywedge X\sigma\,|\,\pi\curlywedge X\in\Upsilon\}$.

To axiomatise the relation $\curlywedge$, we rely on the notion of conjugation of permutations. Conjugacy plays an important role in group theory [Hun80]. Recall that in a group $G$, the element $b$ is a conjugate of $a$ if there exists an element $g$ such that $gag^{-1}=b$. It can be easily shown that conjugacy is an equivalence relation: if $b$ is a conjugate of $a$ then $a$ is a conjugate of $b$. The conjugacy class of $a$ consists of the elements of the form $gag^{-1}$, for $g\in G$. In the case of permutation groups, the conjugate of $\pi$ with respect to $\rho$, denoted as $\pi^{\rho}$, is the result of the composition: $\rho\circ\pi\circ\rho^{-1}$.

[TABLE]

The notion of support of a permutation or nominal term will be necessary for the next results. Considering permutations as elements of a nominal set, it follows from Definition 2.2 that $\texttt{supp}(\pi)=\texttt{dom}(\pi)$; similarly, in the case of a ground term $t$, the support coincides with its set of free names, i.e., $\texttt{supp}(t)={\tt fn}(t)$. In the case a term $t$ is not ground, it should be considered in a context, say $\Upsilon$, which gives information about its variables. We define it after introducing fixed-point and $\alpha$-equality judgements.

{defi}

[Judgements] A fixed-point judgement is a tuple \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\curlywedge t of a fixed-point context and a fixed-point constraint where the atoms $\overline{c}$ are newly quantified. Here $\overline{c}=c_{1},\ldots,c_{n}$, and $n=0$ stands for empty quantification; in that case we may omit the

$\mathsf{N}$

quantifier and write simply $\Upsilon\vdash\pi\curlywedge t$.

An $\alpha$-equivalence judgement is a tuple \Psi\vdash\reflectbox{\mathsf{N}}\overline{c}.\ s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t of a fixed-point context and an equality constraint where the atoms $\overline{c}$ are newly quantified.

The derivable fixed-point and $\alpha$-equivalence judgements are defined by the rules in Figures 3 and 4. We give an example before explaining the rules in more detail.

{exa}

The term $[a]\mathsf{f}a$ is a fixed-point for the permutation $(a\ b)$, since $(a\ b)\cdot[a]\mathsf{f}a=[b]\mathsf{f}b$, which is $\alpha$-equivalent to $[a]\mathsf{f}a$. As expected, we can derive $\vdash(a\ b)\curlywedge[a]\mathsf{f}a$. For this we use the rule $(\mathbf{\curlywedge abs})$, which requires to prove \vdash\reflectbox{\mathsf{N}}c_{1}.(a\ b)\curlywedge(a\ c_{1})\cdot\mathsf{f}a. Since $(a\ c_{1})\cdot\mathsf{f}a=\mathsf{f}c_{1}$, we need to prove \vdash\reflectbox{\mathsf{N}}c_{1}.(a\ b)\curlywedge c_{1}, which holds by $(\mathbf{\curlywedge a})$. However, $\mathsf{f}a$ is not a fixed-point for $(a\ b)$: we cannot derive $\vdash(a\ b)\curlywedge\mathsf{f}a$. This is to be expected, since $\mathsf{f}a$ and $\mathsf{f}b$ are not $\alpha$-equivalent; we cannot derive $\vdash(a\ b)\cdot\mathsf{f}a\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\ \mathsf{f}a$.

The premise of rules $(\mathbf{\curlywedge abs})$ and $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\!{\mathsf{a}b}})$ introduces a newly quantified atom $c_{1}$. Recall that the introduction of a

$\mathsf{N}$

quantifier requires the use of a new atom by well formedness (see Section 2.3). Therefore, in rules $(\mathbf{\curlywedge abs})$ and $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\!{\mathsf{a}b}})$ we can assume that the atom $c_{1}$ does not occur in the conclusion.

In rule $(\mathbf{\curlywedge var})$, the condition $\texttt{supp}(\pi^{{\pi^{\prime}}^{-1}})\setminus\{\overline{c}\}\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$ means that the permutation $\pi^{{\pi^{\prime}}^{-1}}$ can only affect atoms in $\texttt{perm}(\Upsilon|_{X})$ and new atoms, hence it fixes $X$. Rules $(\mathbf{\curlywedge{\mathsf{f}}})$ and $(\mathbf{\curlywedge\texttt{tuple}})$ are straightforward. Rule $(\mathbf{\curlywedge abs})$ is the most interesting one. The intuition behind this rule is the following: $[a]t$ is a fixed-point of $\pi$ if $\pi\cdot[a]t$ is $\alpha$-equivalent to $[a]t$, that is, $[\pi(a)]\pi\cdot t$ is $\alpha$-equivalent to $[a]t$; the latter means that the only free atom in $t$ that could be affected by $\pi$ is $a$, hence, if we replace occurrences of $a$ in $t$ with another, new atom $c$, $\pi$ should have no effect. Note that if a judgement \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge t is derivable, then so is \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c},\overline{c^{\prime}}.\pi\curlywedge t for a new set of atoms $\overline{c^{\prime}}$ (there is an infinite supply of new atoms).

The $\alpha$-equivalence relation is defined using fixed-point judgements (see rule $(\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}{\mathsf{ab}})$). Rules $(\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}{\mathsf{a}})$, $(\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}{\mathsf{f}})$, $(\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}{\mathsf{[a]}})$ and $(\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}{\mathsf{tuple}})$ are defined as expected, whereas the intuition behind rule $(\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}{\mathsf{var}})$ is similar to the corresponding rule in Figure 3. The most interesting rule is $(\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}{\mathsf{ab}})$. Intuitively, it states that for two abstractions $[a]s$ and $[b]t$ to be equivalent, we must obtain equivalent terms if we rename in one of them, in our case $t$, the abstracted atom $b$ to $a$, so that they both use the same atom. Moreover, the atom $a$ should not occur free in $t$, which is checked by stating that $(a\ c_{1})$ fixes $t$ for some newly generated atom $c_{1}$.

{exa}

Notice that $(b\,e)\curlywedge X\vdash(a\,b)\curlywedge[a](\mathsf{f}a,(c\,d)\cdot X)$. This is derived as follows: by rule $(\mathbf{\curlywedge{\mathsf{a}bs}})$ we have to show (b\,e)\curlywedge X\vdash\reflectbox{\mathsf{N}}g.(a\,b)\curlywedge(\mathsf{f}g,(a\,g)(c\,d)\cdot X); by rule $(\mathbf{\curlywedge{\mathsf{t}uple}})$ this requires (b\,e)\curlywedge X\vdash\reflectbox{\mathsf{N}}g.(a\,b)\curlywedge\mathsf{f}g and (b\,e)\curlywedge X\vdash\reflectbox{\mathsf{N}}g.(a\,b)\curlywedge(a\,g)(c\,d)\cdot X; the former holds by application of rules $(\mathbf{\curlywedge\mathsf{f}})$ and $(\mathbf{\curlywedge{\mathsf{a}}})$ since $(a\,b)\cdot g=g$, and the latter by rule $(\mathbf{\curlywedge{\mathsf{v}ar}})$, since $\texttt{supp}((a\ b)^{(c\ d)(a\ g)})\setminus\{g\}=\{g,b\}\setminus\{g\}=\{b\}$ and $\texttt{supp}((b\ e))=\{b,e\}$.

However, it is not possible to derive $(a\,e)\curlywedge X\vdash(a\,b)\curlywedge[a](\mathsf{f}a,(c\,d)\cdot X)$ since in this case $b$ is not in the support of the permutations that fix $X$ (only $(a\ e)$ fixes $X$ according to our context).

We prove below that $\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$ is indeed an equivalence relation, for which we need to study the properties of the relations $\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$ and $\curlywedge$, starting with inversion and equivariance.

Lemma 2** (Inversion).**

The inference rules for $\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$ are invertible.

Proof 3.1**.**

Straightforward since there is only one rule for each syntactic class of terms. Note that in the case of rule $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\!{\mathsf{a}b}})$, the permutative convention ensures that $a$ and $b$ are different atoms.

Equivariance is an important notion in nominal logic: equivariant subsets of nominal sets are closed under permutation (see Definition 1.8 in [Pit13]). Below we show that the fixed-point and $\alpha$-equivalence relations are equivariant.

Lemma 3** (Equivariance).**

1. (1)

\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge\ t* iff \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi^{\rho}\curlywedge\rho\cdot t, for any permutation $\rho$.* 2. (2)

\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t* iff \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\cdot s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\pi\cdot t, for any permutation $\pi$.*

Proof 3.2**.**

For both parts the “if” statement is trivial, by taking the identity permutation, $\mathit{Id}$. We prove the “only if” statements.

1. (1)

The proof is by rule induction using the rules in Figure 3. We consider cases depending on the last rule applied in the derivation.

1. (a)

The rule applied is $(\mathbf{\curlywedge a})$.

In this case, $t=a$. Notice that, $\Upsilon\vdash\pi^{\prime}\curlywedge a$ if, and only if, $\pi^{\prime}(a)=a$. We want to show that \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi^{\rho}\curlywedge\rho(a), for any permutation $\rho$. Notice that $\pi^{\rho}(\rho(a))=(\rho\circ\pi\circ\rho^{-1})(\rho(a))=(\rho\circ\pi)(a)=\rho(\pi(a))=\rho(a)$, and the result follows. 2. (b)

The rule applied is $(\mathbf{\curlywedge var})$.

In this case one has $t=\pi_{1}\cdot X$ and \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge\pi_{1}\cdot X. We need to prove that \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi^{\rho}\curlywedge\rho\cdot(\pi_{1}\cdot X), which requires $\texttt{supp}((\rho\circ\pi_{1})^{-1}\circ\pi^{\rho}\circ(\rho\circ\pi_{1}))\setminus\{\overline{c}\}\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$.

Note that, since \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge\pi_{1}\cdot X, it follows that $\texttt{supp}(\pi_{1}^{-1}\circ\pi\circ\pi_{1})\setminus\{\overline{c}\}\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$. By definition of $\pi^{\rho}$, it follows that

[TABLE]

Therefore, the result follows. 3. (c)

The rule applied is $(\mathbf{\curlywedge abs})$.

In this case, $t=[a]t^{\prime}$ and \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge[a]t^{\prime}, therefore, there exists a proof $\Pi$ :

tensy

\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 48.99814pt\hbox{\displaystyle\penalty 1\Pi}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=105.49629pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c},c_{1}.\ \pi\curlywedge(a\ c_{1})\cdot t^{\prime}}}}}\hskip 5.0pt plus 1.0fil\penalty 2

* $(\mathbf{\curlywedge abs})$*

\displaystyle\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\curlywedge[a]t^{\prime}

**

By induction hypothesis, for an arbitrary permutation $\rho$, there exists a derivation $\Pi^{\prime}$ for :

[TABLE]

Since $\rho\cdot((a\ c_{1})\cdot t^{\prime})=(\rho(a)\ \rho(c_{1}))\cdot(\rho\cdot t^{\prime})=(\rho(a)\ c_{1})\cdot(\rho\cdot t^{\prime})$ because $c_{1}$ is a new name, we have

tensy

\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 63.73485pt\hbox{\displaystyle\penalty 1\Pi^{\prime}}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=136.5097pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c},c_{1}.\ \pi^{\rho}\curlywedge(\rho(a)\ c_{1})\cdot(\rho\cdot t^{\prime})}}}}\hskip 5.0pt plus 1.0fil\penalty 2

* *

\displaystyle\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi^{\rho}\curlywedge[\rho(a)]\rho\cdot t^{\prime}

**

and the result follows. 4. (d)

The rule applied is $(\mathbf{\curlywedge\mathsf{f}})$ or $(\mathbf{\curlywedge tuple})$.

These cases follow directly by induction hypothesis. 2. (2)

The proof is by rule induction using the rules in Figure 4.

1. (a)

The rule applied is $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}a})$.

In this case, $s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t$ is an instance of $a\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}a$. It is straightforward to check that \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\cdot a\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\pi\cdot a, via an application of the rule $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}a})$. 2. (b)

The rule applied is $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}var})$.

In this case, \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi_{1}\cdot X\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\pi_{2}\cdot X and $\texttt{supp}(\pi_{2}^{-1}\circ\pi_{1})\setminus\{\overline{c}\}\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$.

Notice that $\texttt{supp}((\pi\circ\pi_{2})^{-1}\circ\pi\circ\pi_{1})=\texttt{supp}(\pi_{2}^{-1}\circ\pi_{1})$. Therefore, by rule $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}var})$, \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\cdot(\pi_{1}\cdot X)\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\pi\cdot(\pi_{2}\cdot X). 3. (c)

The cases corresponding to rule $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}f})$ and rule $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}[a]})$ follow directly by induction hypothesis. 4. (d)

The rule applied is $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}ab})$.

In this case, there exist derivations $\Pi_{1}$ and $\Pi_{2}$ such that

tensy

\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 42.54616pt\hbox{\displaystyle\penalty 1\Pi_{1}}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=95.39233pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\ t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}{\alpha}(a\ b)\cdot s}}}}\hskip 5.0pt plus 1.0fil\penalty 2\qquad\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 40.90514pt\hbox{\displaystyle\penalty 1\Pi{2}}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=92.11029pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c},c_{1}.\ (a\ c_{1})\curlywedge s}}}}\hskip 5.0pt plus 1.0fil\penalty 2

* $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}ab})$*

\displaystyle\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ [a]t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}[b]s

**

By induction hypothesis, and part (1) of this lemma:

1. (i)

there exists a proof $\Pi_{1}^{\prime}$ of \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\cdot t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\pi\cdot((a\ b)\cdot s). 2. (ii)

there exists a proof $\Pi_{2}^{\prime}$ of \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c},c_{1}.\ (a\ c_{1})^{\pi}\curlywedge\pi\cdot s.

It is easy to show that $\pi\cdot((a\ b)\cdot s)=(\pi(a)\ \pi(b))\cdot(\pi\cdot s)$, and since $c_{1}$ is new, $\pi(c_{1})=c_{1}$, therefore, the result follows.

tensy

\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 68.94662pt\hbox{\displaystyle\penalty 1\Pi_{1}^{\prime}}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=148.19327pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\ \pi\cdot t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}{\alpha}(\pi(a)\ \pi(b))\cdot\pi\cdot s}}}}\hskip 5.0pt plus 1.0fil\penalty 2\qquad\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 54.10536pt\hbox{\displaystyle\penalty 1\Pi{2}^{\prime}}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=118.51074pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c},c_{1}.\ (\pi(a)\ c_{1})\curlywedge\pi\cdot s}}}}\hskip 5.0pt plus 1.0fil\penalty 2

* $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}ab})$*

\displaystyle\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ [\pi(a)]\pi\cdot t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}[\pi(b)]\pi\cdot s

**

{exa}

Notice that $(a\ c)\curlywedge X\vdash(a\ b)\curlywedge(b\ c)\cdot X$, for $(a\ c)\curlywedge X\vdash(a\ c)\curlywedge X$ and $(a\ b)^{(b\ c)}=(a\ c)$. Using the Equivariance Lemma, with $\rho=(b\ c)$, we deduce:

[TABLE]

Proposition 3.3** (Strengthening for $\curlywedge$).**

If \Upsilon,\pi\curlywedge X\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi^{\prime}\curlywedge s and $\texttt{supp}(\pi)\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$ or $X\notin\texttt{Var}(s)$ then \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi^{\prime}\curlywedge s.

Proof 3.4**.**

By induction on the structure of $s$.

• •

$s=a$**

In this case, \Upsilon,\pi\curlywedge X\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi^{\prime}\curlywedge a. By rule $(\mathbf{\curlywedge a})$,

[TABLE]

• •

$s=\pi_{1}\cdot X$* (the case $s=\pi_{1}\cdot Y$ is trivial).*

In this case, \Upsilon,\pi\curlywedge X\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi^{\prime}\curlywedge\pi_{1}\cdot X.

[TABLE]

• •

$s=[a]s^{\prime}$**

In this case, \Upsilon,\pi\curlywedge X\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi^{\prime}\curlywedge[a]s^{\prime}, $\texttt{supp}(\pi)\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$ or $X\notin\texttt{Var}(s^{\prime})$. Then there exists a derivation

tensy

\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 64.20155pt\hbox{\displaystyle\penalty 1\mathcal{D}}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=136.042pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Upsilon,\pi\curlywedge X\vdash\reflectbox{$\mathsf{N}$}\overline{c},c_{1}.\ \pi^{\prime}\curlywedge(a\ c_{1})\cdot s^{\prime}}}}}\hskip 5.0pt plus 1.0fil\penalty 2

* $(\mathbf{\curlywedge abs})$*

\displaystyle\Upsilon,\pi\curlywedge X\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi^{\prime}\curlywedge[a]s^{\prime}

**

By induction hypothesis, there exists a derivation $\mathcal{D}^{\prime}$ such that

tensy

\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 48.3558pt\hbox{\displaystyle\penalty 1\mathcal{D^{\prime}}}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=105.8905pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c},c_{1}.\ \pi^{\prime}\curlywedge(a\ c_{1})\cdot s^{\prime}}}}}\hskip 5.0pt plus 1.0fil\penalty 2

* $(\mathbf{\curlywedge abs})$*

$\displaystyle\Upsilon\vdash\pi^{\prime}\curlywedge[a]s^{\prime}$

**

• •

$s=\mathsf{f}s^{\prime}$* or $s=(s_{1},\ldots s_{n})$*

These cases follow easily by induction hypothesis.

Proposition 3.5** (Strengthening for $\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$).**

If \Upsilon,\pi\curlywedge X\vdash\reflectbox{\mathsf{N}}\overline{c}.\ s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t and $\texttt{supp}(\pi)\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$ or $X\not\in\texttt{Var}(s,t)$, then \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t.

Proof 3.6**.**

The proof is similar to that of Proposition 3.3 and omitted.

The following auxiliary lemma permits to deduce a fixed-point constraint for a permutation $\pi$ and term $t$ from constraints involving $t$. Intuitively, it states that we can deduce that $\pi$ fixes $t$ if the support of $\pi$ is contained in permutations that fix $t$.

Lemma 4**.**

Let $I$ be a set of indices. If \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c_{i}}.\pi_{i}\curlywedge t for all $i\in I$, and $\pi$ is a permutation such that $\texttt{supp}(\pi)\setminus\{\overline{c}\}\subseteq\bigcup_{i\in I}\texttt{supp}(\pi_{i})\setminus\bigcup_{i\in I}\overline{c_{i}}$ then \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge t.

Proof 3.7**.**

By induction on $t$.

• •

If $t=a$ then by assumption $\pi_{i}(a)=a$ for all $i\in I$ since \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c_{i}}.\pi_{i}\curlywedge a (rule $(\mathbf{\curlywedge a})$). Then, $\pi(a)=a$ by the assumption on the support of $\pi$. The result follows by rule $(\mathbf{\curlywedge a})$.

• •

If $t=\pi^{\prime}\cdot X$ then $\texttt{supp}(\pi_{i}^{{\pi^{\prime}}^{-1}})\setminus\{\overline{c_{i}}\}\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$ because \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c_{i}}.\pi_{i}\curlywedge t for all $i\in I$ (rule $(\mathbf{\curlywedge var})$).

Since $\texttt{supp}(\pi)\setminus\{\overline{c}\}\subseteq\bigcup_{i\in I}\texttt{supp}(\pi_{i})\setminus\bigcup_{i\in I}\overline{c_{i}}$, also $\texttt{supp}(\pi^{{\pi^{\prime}}^{-1}})\setminus\{\overline{c}\}\subseteq\bigcup_{i\in I}\texttt{supp}(\pi_{i}^{{\pi^{\prime}}^{-1}})\setminus\bigcup_{i\in I}\overline{c_{i}}$. The result follows by rule $(\mathbf{\curlywedge var})$.

• •

The other cases follow directly by induction.

The following correctness property states that $\curlywedge$ is indeed the fixed-point relation.

Theorem 5** (Correctness).**

Let $\Upsilon$, $\pi$ and $t$ be a fixed-point context, a permutation and a nominal term, respectively. \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\curlywedge t     iff     \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\cdot t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t.

Proof 3.8**.**

In both directions the proof is by induction on the structure of the term $t$, distinguishing cases according to the last rule applied in the derivation.

($\Rightarrow$) The interesting cases correspond to variables and abstractions; the other cases follow directly by the induction hypothesis.

1. (1)

The last rule is $(\mathbf{\curlywedge var})$.

In this case, $t=\pi^{\prime}\cdot X$ and $\texttt{supp}((\pi^{\prime})^{-1}\circ\pi\circ\pi^{\prime})\setminus\{\overline{c}\}\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$, and therefore \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\cdot(\pi^{\prime}\cdot X)\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\pi^{\prime}\cdot X, via rule $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}var})$. 2. (2)

The last rule is $(\mathbf{\curlywedge abs})$. In this case, $t=[a]t^{\prime}$ and by assumption there is a derivation of the form:

tensy

\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 48.99814pt\hbox{\displaystyle\penalty 1\Pi}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=105.49629pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c},c_{1}.\ \pi\curlywedge(a\ c_{1})\cdot t^{\prime}}}}}\hskip 5.0pt plus 1.0fil\penalty 2

* *

\displaystyle\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge[a]t^{\prime}

**

We need to prove that \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ [\pi(a)]\pi\cdot t^{\prime}\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}[a]t^{\prime}, that is, \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\cdot t^{\prime}\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}(\pi(a)\ a)\cdot t^{\prime} and also \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c},c_{1}.(\pi(a)\ c_{1})\curlywedge t^{\prime}.

By IH, there exists a proof $\Pi^{\prime}$ for \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c},c_{1}.\pi\cdot((a\ c_{1}).t^{\prime})\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}(a\ c_{1})\cdot t^{\prime}. The following equivalence holds, since $c_{1}$ is newly quantified:

[TABLE]

Also, \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c},c_{1}.(\pi\cdot t^{\prime})\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}(\pi(a)\ c_{1})\cdot((a\ c_{1})\cdot t^{\prime}) by Equivariance. Note that $(\pi(a)\ c_{1})\cdot((a\ c_{1})\cdot t^{\prime})=(\pi(a)\ a)\cdot t^{\prime}$, hence \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\cdot t^{\prime}\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}(\pi(a)\ a)\cdot t^{\prime} as required.

Since \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c},c_{1}.\ \pi\curlywedge(a\ c_{1})\cdot t^{\prime}, we also have \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c},c_{1}.\ \pi^{(a\ c_{1})}\curlywedge t^{\prime} by equivariance and we deduce \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c},c_{1}.(\pi(a)\ c_{1})\curlywedge t^{\prime} as required.

($\Leftarrow$) Similarly, we proceed by induction on the derivation of \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\cdot t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t. We show the interesting cases, the others follow directly by induction.

1. (1)

The rule is $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}var})$.

In this case $t=\pi_{1}\cdot X$ and there exists a proof of \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\cdot(\pi_{1}\cdot X)\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\pi_{1}\cdot X. Therefore, $\texttt{supp}(\pi_{1}^{-1}\circ\pi\circ\pi_{1})\setminus\{\overline{c}\}\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$, and one can conclude that \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\curlywedge\pi_{1}\cdot X, via application of rule $(\mathbf{\curlywedge var})$. 2. (2)

The rule is $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}ab})$.

In this case, $t=[a]t^{\prime}$ and since \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ [\pi(a)]\pi\cdot t^{\prime}\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}[a]t^{\prime}, we know (Inversion):

\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\cdot t^{\prime}\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}(\pi(a)\ a)\cdot t^{\prime}* and \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c},c_{1}.(\pi(a)\ c_{1})\curlywedge t^{\prime}.*

By Equivariance \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.((\pi(a)\ a)\circ\pi)\cdot t^{\prime}\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t^{\prime} and by induction \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.((\pi(a)\ a)\circ\pi)\curlywedge t^{\prime}.

*From \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c},c_{1}.(\pi(a)\ c_{1})\curlywedge t^{\prime} and \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.((\pi(a)\ a)\circ\pi)\curlywedge t^{\prime} we deduce \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c},c_{1}.\pi^{(a\ c_{1})}\curlywedge t^{\prime} by Lemma 4, since $\texttt{supp}(\pi^{(a\ c_{1})})\setminus\{\overline{c},c_{1}\}\subseteq(\texttt{supp}((\pi(a)\ a)\circ\pi)\setminus\{\overline{c}\})\cup(\texttt{supp}((\pi(a)\ c_{1}))\setminus\{c_{1}\})$. By Equivariance, \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c},c_{1}.\pi\curlywedge(a\ c_{1})\cdot t^{\prime}, and therefore \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\curlywedge[a]t^{\prime} by $(\mathbf{\curlywedge ab})$, as required. *

Recall that $\Upsilon\sigma$ denotes the set of fixed-point constraints obtained by applying the substitution $\sigma$ to the constraints in $\Upsilon$ (see Section 3.1). Below we abbreviate $\Upsilon\vdash\pi_{1}\curlywedge t_{1}$, …, $\Upsilon\vdash\pi_{n}\curlywedge t_{n}$ as $\Upsilon\vdash\pi_{1}\curlywedge t_{1},\ldots,\pi_{n}\curlywedge t_{n}$. Thus, $\Upsilon\vdash\Upsilon^{\prime}\sigma$ means that each of the constraints in $\Upsilon^{\prime}\sigma$ is derivable from $\Upsilon$.

Proposition 3.9** (Preservation under Substitution).**

Suppose that $\Upsilon\vdash\Upsilon^{\prime}\sigma$. Then,

1. (1)

\Upsilon^{\prime}\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\curlywedge s\Longrightarrow\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\curlywedge s\sigma. 2. (2)

\Upsilon^{\prime}\vdash\reflectbox{\mathsf{N}}\overline{c}.\ s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t\Longrightarrow\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ s\sigma\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t\sigma.

Proof 3.10**.**

By induction on the rules in Figures 3 and  4.

1. (1)

We distinguish cases depending on the last rule applied in the derivation of \Upsilon^{\prime}\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge s.

1. (a)

The rule is $(\mathbf{\curlywedge a})$.

In this case, $s=a$ and

tensy

$\displaystyle\penalty 1\pi(a)=a$

* $(\mathbf{\curlywedge a})$*

\displaystyle\Upsilon^{\prime}\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge a

**

The result follows trivially, since $a\sigma=a$ for any substitution $\sigma$. 2. (b)

The rule is $(\mathbf{\curlywedge f})$

In this case, $s=\mathsf{f}s^{\prime}$ and there exists a proof $\Pi^{\prime}$ of

tensy

\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 23.6548pt\hbox{\displaystyle\penalty 1\Pi^{\prime}}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=56.34961pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Upsilon^{\prime}\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\pi\curlywedge s^{\prime}}}}}\hskip 5.0pt plus 1.0fil\penalty 2

* $(\mathbf{\curlywedge f})$*

\displaystyle\Upsilon^{\prime}\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge\mathsf{f}s^{\prime}

**

By induction hypothesis, there exists a proof $\Pi^{{}^{\prime\prime}}$ such that

tensy

\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 27.02074pt\hbox{\displaystyle\penalty 1\Pi^{{}^{\prime\prime}}}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=63.30147pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c}.\pi\curlywedge s^{\prime}\sigma}}}}\hskip 5.0pt plus 1.0fil\penalty 2

* $(\mathbf{\curlywedge f})$*

\displaystyle\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge(\mathsf{f}s^{\prime})\sigma

** 3. (c)

The rule is $(\mathbf{\curlywedge abs})$

In this case $s=[a]s^{\prime}$ and there exists a proof $\Pi^{\prime}$ of the form

tensy

\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 45.64748pt\hbox{\displaystyle\penalty 1\Pi^{\prime}}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=100.33496pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Upsilon^{\prime}\vdash\reflectbox{$\mathsf{N}$}\overline{c},c_{1}.\pi\curlywedge(a\ c_{1})\cdot s^{\prime}}}}}\hskip 5.0pt plus 1.0fil\penalty 2

* $(\mathbf{\curlywedge abs})$*

\displaystyle\Upsilon^{\prime}\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge[a]s^{\prime}

**

By induction hypothesis, there exists a proof $\Pi^{{}^{\prime\prime}}$ of the form

tensy

$\displaystyle\penalty 1\Pi$

* *

\displaystyle\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c},c_{1}.\pi\curlywedge((a\ c_{1})\cdot s^{\prime})\sigma

**

Since $((a\ c_{1})\cdot s^{\prime})\sigma=(a\ c_{1})\cdot(s^{\prime}\sigma)$ and $[a](s^{\prime}\sigma)=([a]s^{\prime})\sigma$, it follows that

tensy

\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 53.7823pt\hbox{\displaystyle\penalty 1\Pi}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=115.06462pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}\overline{c},c_{1}.\pi\curlywedge(a\ c_{1})\cdot(s^{\prime}\sigma)}}}}\hskip 5.0pt plus 1.0fil\penalty 2

* $(\mathbf{\curlywedge abs})$*

\displaystyle\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge[a](s^{\prime}\sigma)

** 4. (d)

The rule is $(\mathbf{\curlywedge tuple})$

This case is analogous to the case for $(\mathbf{\curlywedge f})$, and follows directly by IH. 5. (e)

The rule is $(\mathbf{\curlywedge var})$

In this case, $s=\rho\cdot X$ and \Upsilon^{\prime}\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge\rho\cdot X holds, that is, $\texttt{supp}(\pi^{\rho^{-1}})\setminus\{\overline{c}\}\subseteq\texttt{supp}(\texttt{perm}(\Upsilon^{\prime}|_{X}))$.

From $\Upsilon\vdash\Upsilon^{\prime}\sigma$, it follows that, $\Upsilon\vdash\pi_{1}\curlywedge X\sigma$, for all $\pi_{1}\curlywedge X\in\Upsilon^{\prime}$.

Therefore, \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi^{\rho^{-1}}\curlywedge X\sigma by Lemma 4, and the result follows by Equivariance. 2. (2)

We proceed by analysing the last rule used in the derivation of \Upsilon^{\prime}\vdash\reflectbox{\mathsf{N}}\overline{c}.\ s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t.

1. (a)

The last rule is $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}a})$.

This case is trivial. 2. (b)

The last rule is $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}var})$.

In this case we have \Upsilon^{\prime}\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\cdot X\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\pi^{\prime}\cdot X and therefore $\texttt{supp}((\pi^{\prime})^{-1}\circ\pi)\setminus\{\overline{c}\}\subseteq\texttt{supp}(\texttt{perm}(\Upsilon^{\prime}|_{X}))$.

From $\Upsilon\vdash\Upsilon^{\prime}\sigma$, it follows that $\Upsilon\vdash\pi_{1}\curlywedge X\sigma$, for all $\pi_{1}\curlywedge X\in\Upsilon^{\prime}$.

Therefore, \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.(\pi^{\prime})^{-1}\circ\pi\curlywedge X\sigma by Lemma 4, and the result follows by Theorem 5 and Equivariance. 3. (c)

The last rule is $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}f})$ or $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}[a]})$. These cases follow directly by induction. 4. (d)

The last rule is $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}ab})$.

In this case, we know \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ [a]s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}[b]t and therefore (by Inversion) \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}(a\ b)\cdot t and \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c},c_{1}.(a\ c_{1})\curlywedge t.

By induction hypothesis, \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ s\sigma\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}(a\ b)\cdot t\sigma, and by part (1) of this proposition, \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c},c_{1}.(a\ c_{1})\curlywedge t\sigma. The result then follows using rule $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}ab})$.

Corollary 3.11** (Weakening).**

Assume $\Upsilon^{\prime}\subseteq\Upsilon$.

1. (1)

\Upsilon^{\prime}\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\curlywedge s\Longrightarrow\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ \pi\curlywedge s. 2. (2)

\Upsilon^{\prime}\vdash\reflectbox{\mathsf{N}}\overline{c}.\ s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t\Longrightarrow\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t.

3.2. Alternative approaches to new name generation

In the previous section we used the “new” quantifier to deal with new names in constraints: judgements involve newly quantified constraints, and in rules $(\mathbf{\curlywedge ab})$ and $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}ab})$, when new fresh names are needed, a newly quantified atom is used.

An alternative approach consists of quantifying judgements instead of constraints. More precisely, we can define judgements of the form \reflectbox{\mathsf{N}}\overline{c}.(\Upsilon\vdash\pi\curlywedge t) and \reflectbox{\mathsf{N}}\overline{c}.(\Upsilon\vdash s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t). Rules to derive this kind of judgements can be easily obtained by adapting the rules in Figures 3 and 4. We show the rules for fixed-point judgements in Figure 5. For the sake of readabilty, we omit brackets around judgements in the rules and assume the quantifiers have maximal scope.

Yet another approach consists of using a name generator whenever new names are required (see [CU08, CM17]), as done in [AFN18]. In this case, the new quantifier is not needed, and new names are generated dynamically by using an external generator, under the assumption that the generator outputs a new (unused name) whenever needed. For comparison, we recall in Figure 6 the rules given in [AFN18] to derive fixed-point judgements $\Upsilon\vdash\pi\curlywedge t$. Note that in rule $(\mathbf{\curlywedge abs})$ the fixed-point context $\Upsilon$ is augmented with constraints $(c_{1}\ c_{2})\curlywedge\texttt{Var}(t)$. These constraints serve to store the information about the fact that the generated atoms are ”new”. The trick is to generate two atoms, even though only one new atom is needed ($c_{1}$, to replace $a$), in order to be able to express the fact that $c_{1}$ is new. This solution is inspired by the link between freshness, the new quantifier and fixed-point equations, a\#X\Leftrightarrow\reflectbox{\mathsf{N}}a^{\prime}.(a\ a^{\prime})\cdot X=X, mentioned at the beginning of Section 3.

The rules to derive $\alpha$-equivalence judgements following this approach are recalled in Figure 7.

The latter approach has the advantage of having a simpler syntax for judgements (without quantification) but relies on an external name generator, which can be seen as adding a form of state. In other words, in the latter approach rules produce side-effects. Although not as elegant as the approaches using

$\mathsf{N}$

, this approach is convenient from an implementation point of view. In the next sections we use this technique to translate primitive freshness constraints to primitive fixed-point constraints, and to specify a unification algorithm.

3.3. From freshness to fixed-point constraints and back again

In this section we show that the $\alpha$-equivalence relation defined in terms of freshness constraints, denoted as $\mathrel{{\approx}_{\scriptstyle{\alpha}}}$, is equivalent to $\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$, given that a transformation $[\_]^{\curlywedge}$ from primitive freshness to primitive fixed-point constraints and a transformation $[\_]^{\#}$ from primitive fixed-point to primitive freshness constraints can be defined.

Below we denote by $\mathfrak{F}_{\#}$ the family of freshness contexts, and by $\mathfrak{F}_{\curlywedge}$ the family of fixed-point contexts. The mapping $[\_]_{\curlywedge}$ associates each primitive freshness constraint with a fixed-point constraint; it extends to freshness contexts in the natural way.

[TABLE]

We denote by $[\Delta]_{\curlywedge}$ the image of $\Delta$ under $[\_]_{\curlywedge}$.

The mapping $[\_]_{\#}$ associates each primitive fixed-point constraint with a freshness constraint; it extends to fixed-point contexts in the natural way.

[TABLE]

We denote by $[\Upsilon]_{\#}$ the image of $\Upsilon$ under $[\_]_{\#}$.

Below we abbreviate the set of constraints $\{a_{1}\#t,\ldots a_{n}\#t\mid a_{1},\ldots,a_{n}\in A\}$ as $\overline{A\#t}$.

Using the above-specified translation of primitive constraints, we translate freshness judgements into fixed-point judgements with newly quantified constraints:

$\Delta\vdash a\#t$ is translated as [\Delta]_{\curlywedge}\vdash\reflectbox{\mathsf{N}}c.(a\ c)\curlywedge t

and vice-versa:

\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge t is translated as $[\Upsilon]_{\#}\vdash\overline{\texttt{supp}(\pi)\setminus\{\overline{c}\}\#t}$.

Theorem 6**.**

1. (1)

\Delta\vdash a\#t\Leftrightarrow[\Delta]_{\curlywedge}\vdash\reflectbox{\mathsf{N}}c.(a\ c)\curlywedge t. 2. (2)

\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge t\Leftrightarrow[\Upsilon]_{\#}\vdash\overline{\texttt{supp}(\pi)\setminus\{\overline{c}\}\#t}.

Proof 3.12**.**

Part (1):

$(\Rightarrow)$* By induction on the derivation of $\Delta\vdash a\#t$ (see the rules in Figure 1). We distinguish cases based on the last rule used in the derivation.*

• •

If the rule is $(\mathbf{\#a})$ then $t$ is an atom $b$ (it cannot be $a$), and the result follows by rule $(\mathbf{\curlywedge a})$.

• •

If the rule is $(\mathbf{\#var})$ then $t=\pi\cdot X$ and since $\Delta\vdash a\#\pi\cdot X$ we know $\pi^{-1}(a)\#X\in\Delta$ by Inversion. Hence, $(\pi^{-1}(a)\ c_{\pi^{-1}(a)})\curlywedge X\in[\Delta]_{\curlywedge}$, and therefore $\texttt{supp}((a\ c)^{\pi^{-1}})\setminus\{c\}\subseteq\texttt{supp}(\texttt{perm}([\Delta]_{\curlywedge}|_{X}))$ (recall that $\pi^{-1}(c)=c$ since $c$ is a new atom). The result then follows by rule $(\mathbf{\curlywedge var})$.

• •

The cases for $(\mathbf{\#tuple})$ and $(\mathbf{\#f})$ follow directly by induction.

• •

If the rule is $(\mathbf{\#[a]})$ then $t=[a]s$ and we need to prove [\Delta]_{\curlywedge}\vdash\reflectbox{\mathsf{N}}c.(a\ c)\curlywedge[a]s. By rule $(\mathbf{\curlywedge abs})$, it suffices to show [\Delta]_{\curlywedge}\vdash\reflectbox{\mathsf{N}}c,c_{1}.(a\ c)\curlywedge(a\ c_{1})\cdot s. By Equivariance, this is equivalent to [\Delta]_{\curlywedge}\vdash\reflectbox{\mathsf{N}}c,c_{1}.(a\ c)^{(a\ c_{1})}\curlywedge s, or equivalently [\Delta]_{\curlywedge}\vdash\reflectbox{\mathsf{N}}c,c_{1}.(c_{1}\ c)\curlywedge s, which holds trivially since $c$ and $c_{1}$ are new atoms ($(c_{1}\ c)\cdot s=s$)

• •

If the rule is $(\mathbf{\#abs})$ then $t=[b]s$. By assumption, $\Delta\vdash a\#[b]s$, hence $\Delta\vdash a\#s$. By induction hypothesis, [\Delta]_{\curlywedge}\vdash\reflectbox{\mathsf{N}}c.(a\ c)\curlywedge s, and by Equivariance, [\Delta]_{\curlywedge}\vdash\reflectbox{\mathsf{N}}c,c_{1}.(a\ c)\curlywedge(b\ c_{1})\cdot s. The result follows by rule $(\mathbf{\curlywedge abs})$.

$(\Leftarrow)$* By induction on the derivation of [\Delta]_{\curlywedge}\vdash\reflectbox{\mathsf{N}}c.(a\ c)\curlywedge t. We distinguish cases based on the last rule used in the derivation.*

• •

If the rule is $(\mathbf{\curlywedge a})$ then $t$ is an atom $b$ (it cannot be $a$), and the result follows by rule $(\mathbf{\#a})$.

• •

If the rule is $(\mathbf{\curlywedge var})$ then $t=\pi\cdot X$ and since [\Delta]_{\curlywedge}\vdash\reflectbox{\mathsf{N}}c.(a\ c)\curlywedge\pi\cdot X we know $\texttt{supp}((a\ c)^{\pi^{-1}})\setminus\{c\}\subseteq\texttt{supp}(\texttt{perm}([\Delta]_{\curlywedge}|_{X}))$ by Inversion. Hence, $\pi^{-1}(a)\in\texttt{supp}(\texttt{perm}([\Delta]_{\curlywedge}|_{X}))$, and therefore $\pi^{-1}(a)\#X\in\Delta$ by definition of the mapping $[\cdot]_{\curlywedge}$. The result then follows by rule $(\mathbf{\#var})$.

• •

The cases for $(\mathbf{\curlywedge tuple})$ and $(\mathbf{\curlywedge f})$ follow directly by induction.

• •

*If the rule is $(\mathbf{\curlywedge abs})$ then there are two cases, $t=[a]s$ and $t=[b]s$. *

If $t=[a]s$ the result follows directly by rule $(\mathbf{\#[a]})$.

If $t=[b]s$ then by assumption and Inversion, [\Delta]_{\curlywedge}\vdash\reflectbox{\mathsf{N}}cc_{1}.(a\ c)\curlywedge(b\ c_{1})\cdot s. By Equivariance, [\Delta]_{\curlywedge}\vdash\reflectbox{\mathsf{N}}cc_{1}.(a\ c)\curlywedge s. By induction hypothesis we deduce $\Delta\vdash a\#s$, and the result follows by rule $(\mathbf{\#abs})$.

Part (2):

$(\Rightarrow)$* By induction on the derivation of \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge t. Again we distinguish cases based on the last rule used in the derivation. The only interesting cases are rule $(\mathbf{\curlywedge var})$ and $(\mathbf{\curlywedge abs})$.*

• •

If the last rule applied is $(\mathbf{\curlywedge var})$ then $t=\pi^{\prime}\cdot X$. By Inversion, $\texttt{supp}(\pi^{{\pi^{\prime}}^{-1}})\setminus\{\overline{c}\}\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$. Therefore, for any $a\in\texttt{supp}(\pi)\setminus\{\overline{c}\}$, $\pi^{\prime-1}(a)\in\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$. By definition of the mapping $[\cdot]_{\#}$, $\pi^{\prime-1}(a)\#X\in[\Upsilon]_{\#}$, and the result follows by rule $(\mathbf{\#var})$.

• •

If the last rule applied is $(\mathbf{\curlywedge abs})$ then $t=[a]s$. In this case, we know \Upsilon\vdash\reflectbox{\mathsf{N}}c.c_{1}.\pi\curlywedge(a\ c_{1})\cdot s. By induction, $[\Upsilon]_{\#}\vdash\texttt{supp}(\pi)\setminus\{c,c_{1}\}\#(a\ c_{1})\cdot s$, hence $[\Upsilon]_{\#}\vdash\texttt{supp}(\pi)\setminus\{a\}\#s$, and the result follows by rules $(\mathbf{\#[a]})$ and $(\mathbf{\#abs})$.

$(\Leftarrow)$* By induction on $t$.*

• •

If $t$ is an atom $a$ then $a\not\in\texttt{supp}(\pi)\setminus\{\overline{c}\}$ (by Inversion, rule $(\mathbf{\#a})$). The result follows by rule $(\mathbf{\curlywedge a})$.

• •

If $t=\pi^{\prime}\cdot X$, then the rule applied in the derivation is rule $(\mathbf{\#var})$. By Inversion, for any atom $a$ in $\texttt{supp}(\pi)\setminus\{\overline{c}\}$, $\texttt{supp}(\pi^{\pi^{\prime-1}})\subseteq\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$ and the result follows by rule $(\mathbf{\curlywedge var})$.

• •

If $t=[a]s$ then for any atom $b\in\texttt{supp}(\pi)\setminus\{\overline{c}\}$ ($b$* different from $a$ by the permutative convention), we know $[\Upsilon]_{\#}\vdash b\#s$, since by assumption $[\Upsilon]_{\#}\vdash b\#[a]s$ and the last rule applied in the derivation must have been rule $(\mathbf{\#abs})$. In particular, for any atom $b\in\texttt{supp}(\pi)\setminus\{\overline{c},a,c_{1}\}$, $[\Upsilon]_{\#}\vdash b\#s$. Then, by induction hypothesis, \Upsilon\vdash\reflectbox{\mathsf{N}}c.c_{1}.\pi^{(a\ c_{1})}\curlywedge s and the result follows by Equivariance and rule $(\mathbf{\curlywedge abs})$.*

• •

The other cases follow directly by induction.

Theorem 7**.**

$\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$* coincides with $\mathrel{{\approx}_{\scriptstyle{\alpha}}}$ on ground terms, that is, $\vdash s\mathrel{{\approx}_{\scriptstyle{\alpha}}}t\iff\vdash s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t$. More generally,*

1. (1)

$\Delta\vdash s\mathrel{{\approx}_{\scriptstyle{\alpha}}}t\Rightarrow[\Delta]_{\curlywedge}\vdash s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t$. 2. (2)

\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t\Rightarrow[\Upsilon]_{\#},\Delta\vdash s\mathrel{{\approx}_{\scriptstyle{\alpha}}}t, where $\Delta\vdash\overline{c}\#\texttt{Var}(s,t)$.

Proof 3.13**.**

1. (1)

The first part is proved by induction on the derivation of $\Delta\vdash s\mathrel{{\approx}_{\scriptstyle{\alpha}}}t$, distinguishing cases according to the last rule applied (see Figure 2). The interesting cases correspond to $(\mathbf{\mathrel{{\approx}_{\scriptstyle{\alpha}}}var})$ and $(\mathbf{\mathrel{{\approx}_{\scriptstyle{\alpha}}}ab})$.

• •

If the last rule applied is $(\mathbf{\mathrel{{\approx}_{\scriptstyle{\alpha}}}var})$:

tensy

$\displaystyle\penalty 1\texttt{ds}(\pi,\pi_{1})\#X\subseteq\Delta$

* $(\mathbf{\mathrel{{\approx}_{\scriptstyle{\alpha}}}var})$*

$\displaystyle\Delta\vdash\pi\cdot X\mathrel{{\approx}_{\scriptstyle{\alpha}}}\pi_{1}\cdot X$

**

We want to show that $[\Delta]_{\curlywedge}\vdash\pi\cdot X\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\pi_{1}\cdot X$. To use rule $(\mathbf{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}var})$, we need to show that $\texttt{supp}(\pi_{1}^{-1}\circ\pi)\subseteq\texttt{supp}(\texttt{perm}(([\Delta]\curlywedge)|_{X}))$. Let $b\in\texttt{supp}(\pi_{1}^{-1}\circ\pi)$ and suppose $b\notin\texttt{ds}(\pi,\pi_{1})$. Then $\pi(b)=\pi_{1}(b)$ and $\pi_{1}^{-1}(\pi(b))=b$, contradiction. Therefore, $b\in\texttt{ds}(\pi,\pi_{1})$ and $(b\ c_{b})\curlywedge X\in[\Delta]_{\curlywedge}$ (for $c_{b}$ a new name), and the result follows.

• •

If the last rule applied is $(\mathbf{\mathrel{{\approx}_{\scriptstyle{\alpha}}}ab})$ the result follows directly by induction and Theorem 6. 2. (2)

The second part is proved by induction on the derivation of $\Upsilon\vdash s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t$, distinguishing cases according to the last rule applied. Again the interesting cases correspond to variables and abstractions. The proof follows the lines of the previous part and is omitted.

As a corollary, since $\mathrel{{\approx}_{\scriptstyle{\alpha}}}$ is an equivalence relation [UPG04], we deduce that $\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$ is also an equivalence relation.

Theorem 8**.**

$\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$* is an equivalence relation.*

Lemma 9** ($\curlywedge$ preservation under $\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$).**

If $\Upsilon\vdash s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t$ and \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge s then \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge t.

Proof 3.14**.**

Direct consequence of Theorem 5, Equivariance and Transitivity.

Having proved that $\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$ is an equivalence relation, and that $\curlywedge$ is correctly defined with respect to $\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$, we can use $\curlywedge$ to define the support of a non-ground term. We denote the support of a term in context $\Upsilon\vdash t$ as $\texttt{supp}_{\Upsilon}(t)$. As indicated in Definition 2.2, the set of atoms in the support of an element of a nominal set can be characterised by using permutation fixed points. In the particular case of terms, the previous results justify the definition of $\texttt{supp}_{\Upsilon}(t)$ using fixed-point judgements as follows.

{defi}

Let $\Upsilon\vdash t$ be a term in context. The support of $t$ with respect to $\Upsilon$, $\texttt{supp}_{\Upsilon}(t)$, is the smallest set $A$ of atoms such that for any permutation $\pi$,

[TABLE]

As expected, $\alpha$-equivalent terms have the same support.

Lemma 10**.**

1. (1)

If $\Upsilon\vdash s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t$ then $\texttt{supp}_{\Upsilon}(s)=\texttt{supp}_{\Upsilon}(t)$. 2. (2)

\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge t* if and only if $\texttt{supp}(\pi)\setminus{\{\overline{c}\}}\cap\texttt{supp}_{\Upsilon}(t)=\emptyset$.*

Proof 3.15**.**

Direct consequence of Definition 3.3 and Lemma 9.

4. Nominal Unification via fixed-point constraints

In this section we address the problem of unifying nominal terms. Solutions for unification problems will be represented using fixed-point constraints and substitutions. After defining unification problems, we present a simplification algorithm that computes the most general unifier for a unification problem, provided the problem has a solution (otherwise the algorithm stops indicating that there is no solution). To specify the nominal unification algorithm, in this section we follow the approach to dealing with new atoms that relies on a name generator.

{defi}

A unification problem Pr consists of a finite set of equality and fixed-point constraints of the form $s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}^{?}t$ and $\pi\curlywedge^{?}t$, respectively.

Below we call $\pi\curlywedge^{?}X$ a primitive constraint.

{defi}

[Solution]

A solution for a problem Pr is a pair of the form $\langle\Phi,\sigma\rangle$ where the following conditions are satisfied:

1. (1)

$\Phi\vdash\pi\curlywedge t\sigma$, if $\pi\curlywedge^{?}t\in\texttt{Pr}$; 2. (2)

$\Phi\vdash s\sigma\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t\sigma$, if $s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}^{?}t\in\texttt{Pr}$. 3. (3)

$X\sigma\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}X\sigma\sigma$ for all $X\in\texttt{Var}(\texttt{Pr})$ (the substitution is idempotent).

The solution set for a problem Pr is denoted by $\mathcal{U}(\texttt{Pr})$.

Solutions in $\mathcal{U}(\texttt{Pr})$ can be compared using the following ordering.

{defi}

Let $\Phi_{1},\Phi_{2}$ be fixed-point contexts, and $\sigma_{1},\sigma_{2}$ substitutions. Then $\langle\Phi_{1},\sigma_{1}\rangle\leq\langle\Phi_{2},\sigma_{2}\rangle$ if there exists some $\sigma^{\prime}$ such that

[TABLE]

{defi}

A principal (or most general) solution to a problem Pr is a least element of $\mathcal{U}(\texttt{Pr})$.

We design a unification algorithm via the simplification rules presented in Table 1. These rules act on unification problems Pr by transforming constraints into simpler ones, or instantiating variables in the case of rules $(\mathrel{{\approx}_{\scriptstyle{\alpha}}}inst1)$ and $(\mathrel{{\approx}_{\scriptstyle{\alpha}}}inst1)$. We call the latter instantiating rules. We abbreviate $(t_{1},\ldots,t_{n})$ as $(\widetilde{t})_{1..n}$, and for a set $S$, $\overline{\pi\curlywedge S}=\{\pi\curlywedge X\ |\ X\in S\}$.

We write $\texttt{Pr}\Longrightarrow\texttt{Pr}^{\prime}$ when $\texttt{Pr}^{\prime}$ is obtained from Pr by applying a simplification rule from Table 1, and we write $\stackrel{{\scriptstyle*}}{{\Longrightarrow}}$ for the reflexive and transitive closure of $\Longrightarrow$.

Lemma 11** (Termination).**

There is no infinite chain of reductions $\Longrightarrow$ starting from a problem Pr.

Proof 4.1**.**

Termination of the simplification rules follows directly from the fact that the following measure of the size of Pr is strictly decreasing:

$[\texttt{Pr}]=(n_{1},M)$* where $n_{1}$ is the number of different variables used in Pr, and $M$ is the multiset of sizes of equality constraints and non-primitive fixed-point constraints occurring in Pr. To compare $[\texttt{Pr}]$ and $[\texttt{Pr}^{\prime}]$ we use the lexicographic combination of the usual order on natural numbers, $>$, and its multiset extension. We denote the order by $>_{lex}$. Thus, $[\texttt{Pr}]>_{lex}[\texttt{Pr}^{\prime}]$ if $\texttt{Pr}^{\prime}$ has less variables than Pr, or if it has the same number of variables but smaller equality constraints and non-primitive fixed-point constraints.*

Each simplification step $\texttt{Pr}\Longrightarrow\texttt{Pr}^{\prime}$ either eliminates one variable (when an instantiation rule is used) and therefore decreases the first component of the interpretation, or leaves the first component unchanged but replaces a constraint with smaller ones and/or primitive ones (when a non-instantiating rule is used). Therefore, $\texttt{Pr}\Longrightarrow\texttt{Pr}^{\prime}$ implies $[\texttt{Pr}]>_{lex}[\texttt{Pr}^{\prime}]$. Hence, it is not possible to have an infinite descending chain.

If $\texttt{Pr}\Longrightarrow^{*}\texttt{Pr}^{\prime}$ and $\texttt{Pr}^{\prime}$ is irreducible, we say that $\texttt{Pr}^{\prime}$ is a normal form. We will show next that if instantiation rules are not used, each problem Pr has a unique normal form. Indeed unicity of normal forms for non-instantiating rules is a consequence of the following property.

Lemma 12** (Confluence).**

The relation $\Longrightarrow$ defined by the rules in Table 1 without $(\mathrel{{\approx}_{\scriptstyle{\alpha}}}inst1)$ and $(\mathrel{{\approx}_{\scriptstyle{\alpha}}}inst2)$ is confluent.

Proof 4.2**.**

Confluence follows from the fact that the rules have no critical pairs (there are only trivial overlaps) and are terminating (by Newman’s lemma).

If instantiating rules are used, normal forms are not necessarily unique. For example, the problem $(a\ b)\curlywedge^{?}X,X\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}^{?}Y$ has two normal forms:

[TABLE]

[TABLE]

However reductions do always terminate with some normal form, and all the normal forms of a problem are equivalent in a natural and useful sense (see Definition 4.2 and Theorem 14). We will use the notation $\langle\mathcal{\texttt{Pr}}\rangle_{\texttt{nf}}$ to refer to any normal form of Pr.

We say that an equality constraint $s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}^{?}t$ is reduced when one of the following holds:

1. (1)

$s=a$ and $t=b$ are distinct atoms; 2. (2)

$s$ and $t$ are headed with different function symbols, that is, $s=\mathsf{f}\ s^{\prime}$ and $t=\mathsf{g}\ t^{\prime}$; 3. (3)

$s$ and $t$ have different term constructors, that is, $s=[a]s^{\prime}$ and $t=\mathsf{f}\ t^{\prime}$, for some term former $\mathsf{f}$, or $s=\pi\cdot X$ and $t=a$, etc.

A fixed-point constraint $\pi\curlywedge^{?}s$ is reduced when it is of the form $\pi\curlywedge^{?}a$ and $\pi(a)\neq a$, or $\pi\curlywedge^{?}X$; the former is inconsistent whereas the latter is consistent.

{exa}

For $\texttt{Pr}=[a]\mathsf{f}(X,a)\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}^{?}[b]\mathsf{f}((b\ c)\cdot W,(a\ c)\cdot Y)$, we obtain the following derivation chain using the rules in Table 1:

[TABLE]

{defi}

[Characterisation of normal forms]

Let Pr be a problem such that $\langle\mathcal{\texttt{Pr}}\rangle_{\texttt{nf}}={\texttt{Pr}^{\prime}}$. We say that $\texttt{Pr}^{\prime}$ is reduced when it consists of reduced constraints, and successful when $\texttt{Pr}^{\prime}=\emptyset$ or contains only consistent reduced fixed-point constraints; otherwise, $\langle\mathcal{\texttt{Pr}}\rangle_{\texttt{nf}}$* fails*.

The simplification rules (Table 1) specify a unification algorithm: we apply the simplification rules in a problem Pr until we reach a normal form $\langle\mathcal{\texttt{Pr}}\rangle_{\texttt{nf}}$. {defi}[Computed Solutions]

If $\langle\mathcal{\texttt{Pr}}\rangle_{\texttt{nf}}$ fails or contains reduced equational constraints, we say that Pr is unsolvable; otherwise, $\langle\mathcal{\texttt{Pr}}\rangle_{\texttt{nf}}$ is solvable and its solution, denoted $\langle\texttt{Pr}\rangle_{\mathtt{\it{sol}}}$, consists of the composition $\sigma$ of substitutions applied through the simplification steps and the fixed-point context $\Phi=\{\pi\curlywedge X\ |\pi\curlywedge^{?}X\in\langle\mathcal{\texttt{Pr}}\rangle_{\texttt{nf}}\}$.

{exa}

[Continuing example 4] Notice that $\langle\Psi,\sigma\rangle$, where $\Psi=\{(a\ c_{1})\curlywedge W,(c_{1}\ c_{2})\curlywedge W\}$ and $\sigma=\{Y\mapsto b,X\mapsto(a\ b)\circ(b\ c)\cdot W\}$, is a solution for Pr.

We will now show that every solvable unification problem has a principal solution, computed by the unification algorithm, such that any other solution can be obtained as an instance of the principal one.

We start by proving that the non-instantiating rules preserve the set of solutions.

Lemma 13** (Correctness of Non-Instantiating rules).**

Let Pr be a unification problem such that $\texttt{Pr}\Longrightarrow^{*}\texttt{Pr}^{\prime}$ without using instantiating rules $(\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}inst1)$ and $(\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}inst2)$ then

1. (1)

$\mathcal{U}(\texttt{Pr})=\mathcal{U}(\texttt{Pr}^{\prime})$, and 2. (2)

if $\texttt{Pr}^{\prime}$ contains equational or inconsistent reduced fixed-point constraints then $\mathcal{U}(\texttt{Pr})=\emptyset$.

Proof 4.3**.**

The proof is by induction on the length of the derivation $\texttt{Pr}\overset{n}{\Longrightarrow}\texttt{Pr}^{\prime}$.

Base Case.* $n=0$. Then $\texttt{Pr}=\texttt{Pr}^{\prime}$ and the result is trivial.*

Induction Step.* Suppose, $n>0$ and consider the reduction chain*

[TABLE]

The proof follows by case analysis on the last rule applied in $\texttt{Pr}_{n-1}$.

1. (1)

The rule is $(\curlywedge at)$.

In this case, $\texttt{Pr}_{n-1}=\texttt{Pr}_{n-1}^{\prime}\uplus\{\pi\curlywedge^{?}a\}\Longrightarrow\texttt{Pr}_{n-1}^{\prime}=\texttt{Pr}_{n}$, and $\pi(a)=a$.

Let $\langle\Psi,\sigma\rangle\in\mathcal{U}(\texttt{Pr}_{n-1})$, then

1. (a)

$\ \Psi\vdash\pi^{\prime}\curlywedge t\sigma$, for all $\pi^{\prime}\curlywedge^{?}t\in\texttt{Pr}^{\prime}_{n-1}$ 2. (b)

$\ \Psi\vdash t\sigma\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}s\sigma$, for all $t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}^{?}s\in\texttt{Pr}_{n-1}^{\prime}$; 3. (c)

$X\sigma=X\sigma\sigma$, for all $X\in\texttt{Var}(\texttt{Pr}_{n-1}^{\prime})$.

Therefore, $\langle\Psi,\sigma\rangle\in\mathcal{U}(\texttt{Pr}_{n})$ and $\mathcal{U}(\texttt{Pr}_{n-1})\subseteq\mathcal{U}(\texttt{Pr}_{n})$. The other inclusion is trivial. 2. (2)

The rule is $(\curlywedge var)$.

In this case, $\texttt{Pr}_{n-1}=\texttt{Pr}_{n-1}^{\prime}\uplus\{\pi\curlywedge^{?}\pi^{\prime}\cdot X\}\Longrightarrow\texttt{Pr}_{n-1}^{\prime}\cup\{\pi^{(\pi^{\prime})^{-1}}\curlywedge^{?}X\}=\texttt{Pr}_{n}$, and $\pi^{\prime}\neq Id$.

Let $\langle\Psi,\sigma\rangle\in\mathcal{U}(\texttt{Pr}_{n-1})$, then

1. (a)

$\ \Psi\vdash\pi^{\prime}\curlywedge t\sigma$, for all $\pi^{\prime}\curlywedge^{?}t\in\texttt{Pr}^{\prime}_{n-1}$, and $\Psi\vdash\pi\curlywedge\pi^{\prime}\cdot X\sigma$. 2. (b)

$\ \Psi\vdash t\sigma\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}s\sigma$, for all $t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}^{?}s\in\texttt{Pr}_{n-1}^{\prime}$; 3. (c)

$X\sigma=X\sigma\sigma$, for all $X\in\texttt{Var}(\texttt{Pr}_{n-1}^{\prime})$.

Notice that

[TABLE]

Therefore, $\langle\Psi,\sigma\rangle\in\mathcal{U}(\texttt{Pr}_{n})$ and $\mathcal{U}(\texttt{Pr}_{n-1})\subseteq\mathcal{U}(\texttt{Pr}_{n})$. The other inclusion is similar. 3. (3)

The rule is $\curlywedge abs$. Then

[TABLE]

where $c_{1}$ and $c_{2}$ are new names not occurring anywhere in the problem.

Let $\langle\Psi,\sigma\rangle\in\mathcal{U}(\texttt{Pr}_{n-1}$) be a solution for $\texttt{Pr}_{n-1}$:

1. (a)

$\ \Psi\vdash\pi^{\prime}\curlywedge t\sigma$, for all $\pi^{\prime}\curlywedge^{?}t\in\texttt{Pr}^{\prime}$, and $\Psi\vdash\pi\curlywedge([a]s)\sigma$. 2. (b)

$\ \Psi\vdash t\sigma\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}s\sigma$, for all $t\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}^{?}s\in\texttt{Pr}^{\prime}$.

Since $\Psi\vdash\pi\curlywedge([a]s)\sigma$ and $([a]s)\sigma=[a]s\sigma$, it follows that $\Psi\vdash\pi\curlywedge[a](s\sigma)$. From inversion and rule $(\mathbf{\curlywedge abs})$ (see Figure 6), this implies that there exists a proof for $\Psi,\overline{(c_{1}\ c_{2})\curlywedge\texttt{Var}(s\sigma)}\vdash\pi\curlywedge(a\ c_{1}).s\sigma$.

Notice that we can always choose $c_{1}$ and $c_{2}$ such that $\texttt{supp}((c_{1}\ c_{2}))\cap\texttt{supp}(s\sigma)=\emptyset$, from Lemma 10, it follows that $\Psi\vdash(c_{1}\ c_{2})\curlywedge s\sigma$. Since $\Psi,\overline{(c_{1}\ c_{2})\curlywedge\texttt{Var}(s\sigma)}\vdash\pi\curlywedge(a\ c_{1}).s\sigma$, it follows that $\Psi\vdash\pi\curlywedge(a\ c_{1}).s\sigma$, by Proposition 3.9. The other inclusion is similar.

The cases corresponding to the other non-instantiating simplification rules are similar to the above and omitted.

We now show that the result of the algorithm is a principal solution.

Theorem 14**.**

Let Pr be a unification problem, and suppose $\langle\texttt{Pr}\rangle_{\mathtt{\it{sol}}}=\langle\Phi,\sigma\rangle$. Then:

1. (1)

$\langle\Phi,\sigma\rangle\in\mathcal{U}(\texttt{Pr})$, and 2. (2)

$\langle\Phi,\sigma\rangle\leq\langle\Phi^{\prime},\sigma^{\prime}\rangle$* for all other $\langle\Phi^{\prime},\sigma^{\prime}\rangle\in\mathcal{U}(\texttt{Pr})$. That is, the solution is also a least or principal solution.*

Proof 4.4**.**

We work by induction on the length of the reduction $\texttt{Pr}\Longrightarrow^{*}\langle\texttt{Pr}\rangle_{\mathtt{\it{sol}}}$.

• •

Suppose Pr is in normal form. Then the result is trivial since:

1. (1)

$\sigma=\mathit{Id}$, $\Phi\vdash\texttt{Pr}\mathit{Id}$ and $\mathit{Id}$ is idempotent; 2. (2)

For any other $\langle\Phi^{\prime},\sigma^{\prime}\rangle\in\mathcal{U}(\texttt{Pr})$, $\sigma^{\prime}$ is such that $\Phi^{\prime}\vdash\Phi\sigma$ and $\Phi^{\prime}\vdash X\mathit{Id}\sigma\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}X\sigma$ for all $X$.

• •

Suppose $\texttt{Pr}\Longrightarrow\texttt{Pr}^{\prime}$ by some non-instantiating simplification. Then using Lemma 13, we know that $\mathcal{U}(\texttt{Pr})=\mathcal{U}(\texttt{Pr}^{\prime})$. Both parts of the result follow by induction.

• •

Suppose $\texttt{Pr}\Longrightarrow^{\theta}\texttt{Pr}^{\prime}\theta$ by an instantiating rule. Assume $\texttt{Pr}=\texttt{Pr}^{\prime}\cup\{\pi\cdot X\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t\}$ where $\theta=[X\mapsto\pi^{-1}\cdot t]$ and $X\not\in\texttt{Var}(t)$ (the case for the other instantiating rule is similar). Suppose $\langle\texttt{Pr}^{\prime}\theta\rangle_{\mathtt{\it{sol}}}=\langle\Phi,\sigma\rangle$, so that by construction $\langle\texttt{Pr}\rangle_{\mathtt{\it{sol}}}=\langle\Phi,\theta\circ\sigma\rangle$.

1. (1)

It is easy to see that $\theta\circ\sigma$ is idempotent and by the first part of the inductive hypothesis $\Phi\vdash\texttt{Pr}^{\prime}\theta\sigma$, that is, $\langle\Phi,\theta\circ\sigma\rangle\in\mathcal{U}(\texttt{Pr})$. 2. (2)

Suppose $\langle\Phi^{\prime},\sigma^{\prime}\rangle\in\mathcal{U}(\texttt{Pr})$. Then $\Phi^{\prime}\vdash X\sigma^{\prime}\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}\pi^{-1}\cdot t\sigma^{\prime}$ by Equivariance. Hence, $\langle\Phi^{\prime},\theta\circ\sigma^{\prime\prime}\rangle\in\mathcal{U}(\texttt{Pr})$ where $\sigma^{\prime\prime}$ acts just like $\sigma^{\prime}$ only it maps $X$ to $X$, $\theta=[X\mapsto\pi^{-1}\cdot t]$, and $\sigma^{\prime}=\theta\circ\sigma^{\prime\prime}$. Note that $\langle\Phi^{\prime},\sigma^{\prime\prime}\rangle\in\mathcal{U}(\texttt{Pr}^{\prime}\theta)$ and by inductive hypothesis $\langle\Phi,\sigma\rangle\leq\langle\Phi^{\prime},\sigma^{\prime\prime}\rangle$. It follows that $\langle\Phi,\theta\circ\sigma\rangle\leq\langle\Phi^{\prime},\theta\circ\sigma^{\prime\prime}\rangle$.

Matching and unification are closely related notions. While unification is the basis of logic programming languages, matching is at the heart of rewriting and functional programming. A matching algorithm can be easily derived from a unification algorithm. First we recall the definition of matching.

{defi}

A matching problem is a particular kind of unification problem Pr in which the variables in right-hand sides of equality constraints are disjoint from the variables in left-hand sides. A solution $\langle\Phi,\sigma\rangle$ for a matching problem Pr satisfies $\Phi\vdash s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}t\sigma$ and $\Phi\vdash\pi\curlywedge t\sigma$, for each $s\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}^{?}t,\pi\curlywedge^{?}t\in\texttt{Pr}$ (i.e., in a matching problem, only the variables in right-hand sides of terms can be instantiated.

A nominal matching algorithm can be obtained from the unification algorithm specified in Table 1 by restricting the instantiation rules, so that only variables which were in left-hand sides of equality constraints in the initial problem can be instantiated.

{obs}

Theorem 5 guarantees the equivalence between $\mathrel{{\approx}_{\scriptstyle{\alpha}}}$ and $\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$, therefore, we can associate the unification algorithm proposed, with the standard nominal unification algorithm proposed in [UPG04]. The problem Pr introduced in Example 4, is equivalent to the nominal unification problem $\mathcal{P}=\{[a]\mathsf{f}(X,a)\mathrel{{\approx}_{\scriptstyle{\alpha}}}^{?}[b]\mathsf{f}((b\ c)\cdot W,(a\ c)\cdot Y\}$, and using the standard simplification rules [UPG04]:

[TABLE]

The pair $\langle\mathcal{P}\rangle_{\tt sol}=\langle\{a\#W\},\delta\rangle$, where $\delta=\{Y\mapsto b,X\mapsto(a\ b)\circ(b\ c)\cdot W\}$ is a solution for $\mathcal{P}$. Using the translation $[\_]_{\curlywedge}$, we obtain $[\langle\mathcal{P}\rangle_{\tt sol}]_{\curlywedge}=\langle\{[a\#W]_{\curlywedge}\},\delta\rangle=\langle(a\ c_{a})\curlywedge W,\delta\rangle$, where $c_{a}$ is a new name, which is equivalent to $\langle(a\ c_{a})\curlywedge W,(c_{a}\ c_{1})\curlywedge W,\delta\rangle$, for $c_{a}$ and $c_{1}$ not occurring anywhere in $\mathcal{P}$. Therefore, $[\langle\mathcal{P}_{\tt sol}\rangle]_{\curlywedge}$ is a solution for $\texttt{Pr}=\{[a]\mathsf{f}(X,a)\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}^{?}[b]\mathsf{f}((b\ c)\cdot W,(a\ c)\cdot Y\}$. Similarly, from the solution $\langle\Psi,\sigma\rangle$ proposed in Example 4.2, we obtain $\langle[\Psi]_{\#},\sigma\rangle=\langle a\#W,c_{1}\#W,c_{2}\#W,\sigma\rangle$, which is a solution for $\mathcal{P}$.

In the theorem below $\texttt{Pr}_{\curlywedge}$ denotes a unification problem w.r.t. $\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$ and $\curlywedge$, and $\mathcal{P}_{\#}$ denotes a unification problem w.r.t. $\mathrel{{\approx}_{\scriptstyle{\alpha}}}$ and $\#$.

Theorem 15**.**

Let $\texttt{Pr}_{\curlywedge}$ and $\mathcal{P}_{\#}$ be unification problems such that $[\texttt{Pr}_{\curlywedge}]^{\#}=\mathcal{P}_{\#}$ and $\langle\Psi,\sigma\rangle\in\mathcal{U}(\texttt{Pr}_{\curlywedge})$ and $\langle\Delta,\delta\rangle\in\mathcal{U}(\mathcal{P}_{\#})$ be solutions for $\texttt{Pr}_{\curlywedge}$ and $\mathcal{P}_{\#}$, respectively. Then

1. (1)

$\langle[\Psi]_{\#},\sigma\rangle\in\mathcal{U}(\mathcal{P}_{\#})$. 2. (2)

$\langle[\Delta]_{\curlywedge},\delta\rangle\in\mathcal{U}(\texttt{Pr}_{\curlywedge})$.

Proof 4.5**.**

Consequence of Theorems 6 and 7 and the fact that substitution preserves $\#$, $\mathrel{{\approx}_{\scriptstyle{\alpha}}}$, $\curlywedge$ and $\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$ judgements (see Proposition 3.9).

It is easy to see that the algorithm in Table 1 is exponential (as the one given in [UPG04]): even if we restrict the problems to first-order unification problems (without atoms), the simplification of the following problem requires a number of steps which is exponential with respect to the size of the problem.

[TABLE]

Comparing this algorithm with the one based on freshness constraints, one notices that there is a correspondence between the simplification rules in both approaches (the term syntax is the same in both cases). Moreover, the simplification rules for fixed-point constraints work exactly like the simplification rules for freshness constraints (fixed-point rules have linear complexity, same as the simplification rules for freshness constraints in the freshness-based approach). The techniques designed to improve the efficiency of the freshness-based nominal unification algorithm (see, e.g., [Cal10, LV10]) can equally apply to the fixed-point based algorithm. To avoid the exponential complexity, terms should be represented via graphs, and permutations should be applied in a lazy way (see [Cal10, LV10] for details). We leave the development of efficient implementations to future work and in the rest of the paper we focus on unification modulo equational theories.

5. Nominal alpha-equivalence modulo equational theories

In this section an extension of $\alpha$-equality to take into account equational theories will be proposed. It is well-known that first-order unification modulo an arbitrary equational theory $\mathsf{E}$ is undecidable, therefore, it is expected that nominal unification modulo $\mathsf{E}$ (nominal $\mathsf{E}$-unification, for short) inherits this undecidability property. In this work, we propose an approach to deal with particular classes of equational theories, such as, associativity ($\mathsf{A}$), commutativity ($\mathsf{C}$) and associativity-commutativity ($\mathsf{AC}$), using fixed-point constraints.

In the case in which $\mathsf{E}$ = $\mathsf{A}$, $\mathsf{C}$, $\mathsf{AC}$, or a combination of these theories, an algorithm to check $\mathsf{E}$-$\alpha$-equality via freshness constraints was proposed in [AdCSFN17, AdCSMFR19], where correctness results were formally verified using the Coq proof assistant, and an implementation in Ocaml was given. Unification was considered only for $\mathsf{C}$ theories, for which it was shown that in general there is no finitary representation of the set of solutions if solutions are represented by freshness contexts and substitutions.

We argue that the approach of fixed-point constraints is convenient when dealing with unification problems in equational theories that involve some notion of permutation of elements (such as commutativity), as it was shown in the previous version of this paper [AFN18].

5.1. Alpha-equivalence modulo $\mathsf{E}$ via permutation fixed points

In this section the relations $\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$ and $\curlywedge$ will be extended to $\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}$ and $\curlywedge_{\mathsf{E}}$, where $\mathsf{E}$ is some equational theory. Inference rules will be parameterised by $\mathsf{E}$ so they can be reused when other theories are exploited.

In this work we have dedicated rules for $\mathsf{A}$, $\mathsf{C}$ and $\mathsf{AC}$, and their application depends on whether the signature $\Sigma$ has function symbols satisfying these theories. Whenever we want to restrict the results to a particular theory, we will explicitly indicate the $\mathsf{E}$.

Similarly to the case of pure/syntactic $\alpha$-equality we define notions of $\mathsf{E}$-fixed-point and $\mathsf{E}$-$\alpha$-equality constraints, as well as $\mathsf{E}$-fixed-point contexts and $\mathsf{E}$-judgments as expected.

{defi}

[$\mathsf{E}$-constraints and $\mathsf{E}$-fixed-point contexts]

• •

An $\mathsf{E}$-fixed-point constraint is a pair of the form $\pi\curlywedge_{\mathsf{E}}t$, of a permutation $\pi$ and a term $t$. An $\mathsf{E}$-$\alpha$-equality constraint (for short, $\mathsf{E}$-equality constraint or just equality constraint) is a pair of the form $s\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}t$, for nominal terms $s$ and $t$.

• •

We call a fixed-point constraint of the form $\pi\curlywedge_{\mathsf{E}}X$ a primitive $\mathsf{E}$-fixed-point constraint and a finite set of such constraints is called an $\mathsf{E}$-fixed-point context. $\Upsilon,\Psi,\ldots$ range over contexts.

Intuitively, $s\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}t$ will mean that $s$ and $t$ are $\alpha$-equivalent modulo the equational theory $\mathsf{E}$, and $\pi\curlywedge_{\mathsf{E}}t$ will mean that the permutation $\pi$ has no effect on the equivalence class of the term $t$ modulo $\mathsf{E}$. For instance, $(a\ c)\curlywedge_{\mathsf{C}}+(a,c)$, assuming + is commutative, but not $(a\ c)\curlywedge_{\mathsf{C}}\mathsf{f}(a,c)$, if $\mathsf{f}$ is not a commutative symbol.

Below we assume that commutative symbols are always applied to pairs (although the grammar of nominal terms permits application of function symbols to tuples, we assume a syntactic check is carried out in the case of $\mathsf{C}$-symbols).

{defi}

An $\mathsf{E}$-fixed-point judgement is a tuple \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge_{\mathsf{E}}t of a fixed-point context and a fixed-point constraint, possibly with some newly quantified atoms, whereas an $\mathsf{E}$-$\alpha$-equality judgement is a tuple \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.s\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}t of a fixed-point context and an $\mathsf{E}$-equality constraint, also with some newly quantified atoms $\overline{c}$.

$\mathsf{E}$-judgements are derived using the rules in Figures 8 and 9.

Notice that unlike the syntactical case, where the deduction rules for $\curlywedge$ do not use $\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}$, here the rules for $\curlywedge_{\mathsf{E}}$ and $\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}$ are mutually recursive when the theory $\mathsf{E}$ involves function symbols with commutative and associative-commutativity properties (see rules $(\mathbf{\curlywedge_{\mathsf{E}}\mathsf{f}^{\mathsf{C}}})$ and $(\mathbf{\curlywedge_{\mathsf{E}}\mathsf{f}^{\mathsf{AC}}})$. We assume that the terms are flattened w.r.t. associative and associative-commutative function symbols.

Despite the fact that the rules are mutually recursive, the relations are well-defined since the recursion is well-founded. To see this, one can use a measure that interprets each equality judgement by the pair consisting of the maximum of the sizes of terms in the equality constraint and the symbol $\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}$, and each fixed-point judgement by the pair consisting of the size of the term in the fixed-point constraint and the fixed-point symbol. For example, \Upsilon\vdash\reflectbox{\mathsf{N}}c.s\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}t is interpreted by $\langle max(|s|,|t|),\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}\rangle$ and \Upsilon\vdash\reflectbox{\mathsf{N}}c.(a\ b)\curlywedge_{\mathsf{E}}t by $\langle|t|,\curlywedge_{\mathsf{E}}\rangle$. We compare these pairs lexicographically, using the ordering on natural numbers to compare the sizes of terms, and the ordering $\curlywedge_{\mathsf{E}}>\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}$ for the second component of pairs. We can then check that in all the rules in Figures 8 and 9 the premises are strictly smaller than the conclusion according to this ordering, therefore the rules provide an inductive definition of the set of derivable judgements.

Rules $(\mathbf{\curlywedge_{\mathsf{E}}a}),(\mathbf{\curlywedge_{\mathsf{E}}var}),(\mathbf{\curlywedge_{\mathsf{E}}abs})$ and $(\mathbf{\curlywedge_{\mathsf{E}}tuple})$ behave exactly as the corresponding rules in Figure 3 (where $\mathsf{E}=\emptyset$), i.e., the theory $\mathsf{E}$ has no effect on the fixed-point constraint.

Rule $(\mathbf{\curlywedge_{\mathsf{E}}\mathsf{f}})$ is used for associative and uninterpreted function symbols. In the case of commutative or associative-commutative function symbols the rules $(\mathbf{\curlywedge_{\mathsf{E}}f^{\mathsf{C}}})$ and $(\mathbf{\curlywedge_{\mathsf{E}}f^{\mathsf{AC}}})$ are used. The goal is to ensure the analogous of Theorem 5 for the relations $\curlywedge_{\mathsf{E}}$ and $\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}$ that we wish to obtain: \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge_{\mathsf{E}}t iff $\Upsilon\vdash\overline{c}.\pi\cdot t\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}t$ (Theorem 16). This is illustrated in the example below.

{exa}

Let $+$ be a commutative function symbol and suppose that we want to decide whether $\emptyset\vdash(a\ b)\curlywedge_{\mathsf{C}}((a+b)+c)$, which corresponds to $\emptyset\vdash(a\ b)\cdot((a+b)+c)\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}(a+b)+c$ since $(a\ b)\cdot((a+b)+c)=(b+a)+c\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}(a+b)+c$. In general, $\Upsilon\vdash\pi\curlywedge_{\mathsf{C}}t_{0}+t_{1}$ means that the permutation $\pi$ fixes $t_{0}+t_{1}$ modulo $\mathsf{C}$ (given the information in $\Upsilon$), that is, $\Upsilon\vdash\pi\cdot(t_{0}+t_{1})\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}t_{0}+t_{1}$. By definition, the permutation $\pi$ distributes homomorphically over the operator $+$, therefore, we have $\Upsilon\vdash\pi\cdot t_{0}+\pi\cdot t_{1}\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}t_{0}+t_{1}\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}t_{1}+t_{0}$. Thus, two cases can be distinguished: $\Upsilon\vdash\pi\cdot t_{i}\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}t_{i}$ or $\Upsilon\vdash\pi\cdot t_{i}\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}t_{(i+1)mod\ 2}$, for $i=0,1$ (see rule $(\mathbf{\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}f^{\mathsf{C}}})$ in Figure 9).

Similarly, $\alpha$-equality rules (see Figure 4) have their equational counterpart in Figure 9: rules for atoms, tuples and abstractions are not affected by the theory $\mathsf{E}$, whereas rules involving function symbols $\mathsf{f}^{\mathsf{E}}$ have to be analysed separately.

• •

Associative symbols: rule $(\mathbf{\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}\mathsf{f}^{\mathsf{A}}})$ assumes that terms are flattened with respect to nested occurrences of $\mathsf{f}^{\mathsf{A}}$.

• •

Commutative symbols: rule $(\mathbf{\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}\mathsf{f}^{\mathsf{C}}})$ is used.

• •

Associative-commutative symbols: terms are assumed to be flattened with respect to the $\mathsf{f}^{\mathsf{AC}}$ function symbol, and rule $(\mathbf{\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}\mathsf{f}^{\mathsf{AC}}})$ is used.

{exa}

Consider the signature $\Sigma_{\mathsf{A}}=\{\mathsf{f}^{\mathsf{A}}\}\cup\Sigma^{\emptyset}$, where $\Sigma^{\emptyset}$ is a set of uninterpreted function symbols. Rules $(\mathbf{\curlywedge_{\mathsf{E}}\mathsf{f}^{\mathsf{AC}}})$, $(\mathbf{\curlywedge_{\mathsf{E}}\mathsf{f}^{\mathsf{C}}}),(\mathbf{\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}\mathsf{f}^{\mathsf{C}}})$ and $(\mathbf{\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}\mathsf{f}^{\mathsf{AC}}})$ will not be used in judgements involving $\Sigma_{\mathsf{A}}$-terms, therefore, we can replace $\mathsf{E}$ for $\mathsf{A}$ and obtain rules for $\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{A}}}}$ and $\curlywedge_{\mathsf{A}}$. For instance, consider $\mathsf{f}^{\mathsf{A}}([a]a,\mathsf{f}^{\mathsf{A}}(b,X))$, which is represented in flattened form as $\mathsf{f}^{\mathsf{A}}([a]a,b,X)$.

tensy

\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1\small\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 36.07254pt\hbox{\displaystyle\penalty 1}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=72.14508pt\hbox{\kern 2.70003pt(\mathbf{\curlywedge_{\mathsf{A}}a})}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Upsilon\vdash\reflectbox{$\mathsf{N}$}c_{1}.(a\ d)\curlywedge_{\mathsf{A}}c_{1}}}}}\hskip 4.5pt plus 1.0fil\penalty 2}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=125.06578pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge_{\mathsf{A}}abs})$}}}\hbox{\kern 29.74284pt\hbox{$\displaystyle\Upsilon\vdash(a\ d)\curlywedge_{\mathsf{A}}[a]a$}}}}\hskip 4.5pt plus 1.0fil\penalty 2\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 27.46397pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=54.92795pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge_{\mathsf{A}}a})$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\Upsilon\vdash(a\ d)\curlywedge_{\mathsf{A}}b$}}}}\hskip 4.5pt plus 1.0fil\penalty 2\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\{a,d\}\!\subseteq\!\texttt{supp}(\texttt{perm}(\Upsilon|_{X}))$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=101.33784pt\hbox{\kern 2.70003pt$(\mathbf{\curlywedge_{\mathsf{A}}a})\;\;\hbox to0.0pt{\mbox{\bf?}\hss}$}}}\hbox{\kern 21.05495pt\hbox{$\displaystyle\Upsilon\vdash(a\ d)\curlywedge_{\mathsf{A}}X$}}}}\hskip 4.5pt plus 1.0fil\penalty 2}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=449.14369pt\hbox{\kern 3.00003pt(\mathbf{\curlywedge_{\mathsf{A}}\mathsf{tuple}})}}}\hbox{\kern 173.12471pt\hbox{\displaystyle\Upsilon\vdash(a\ d)\curlywedge_{\mathsf{A}}([a]a,b,X)}}}}\hskip 5.0pt plus 1.0fil\penalty 2

$(\mathbf{\curlywedge_{\mathsf{A}}\mathsf{f}^{\mathsf{A}}})$

$\displaystyle\Upsilon\vdash(a\ d)\curlywedge_{\mathsf{A}}\mathsf{f}^{\mathsf{A}}([a]a,b,X)$

The conclusion of this derivation depends on the support of the permutations in $\Upsilon$, this is illustrated with the question mark ‘?’ in the rightmost leaf in the derivation. For example, if, on one hand, $\Upsilon=\emptyset$, then this derivation fails and we cannot conclude that $(a\ d)$ fixes $\mathsf{f}^{\mathsf{A}}([a]a,b,X)$; if, on the other hand, $\Upsilon=\{(a\ b)\curlywedge X,(d\ e)\curlywedge X\}\cup\Upsilon^{\prime}$, then we could conclude the opposite.

{exa}

Consider the signature $\Sigma_{\{\mathsf{C,AC}\}}=\{\mathsf{\oplus}^{\mathsf{C}},\mathsf{or}^{\mathsf{AC}}\}\cup\{\forall^{\emptyset},\mathsf{g}^{\emptyset}\}\cup\Sigma^{\emptyset}$, where $\forall$ and $\mathsf{g}$ are unary uninterpreted function symbols. To improve readability, we will omit the superscripts of the function symbols in the rest of this example. Since we only have commutative and associative-commutative symbols, we will replace $\mathsf{E}$ in the rules by $\{\mathsf{C,AC}\}$, therefore, obtaining rules for $\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{\{C,AC\}}}}}$ and $\curlywedge_{\mathsf{\{C,AC\}}}$. By applying the rules one can verify that

• •

$\emptyset\not\vdash(a\ b)(b\ c)\curlywedge_{\mathsf{\{C,AC\}}}(\mathsf{g}(a)\oplus\mathsf{g}(b))\oplus\mathsf{g}(c)$, this is due to the fact that $\oplus$ is commutative but not associative, and the permutation $(a\ b)(b\ c)$ swaps the atom $a$ which is an argument of the inner $\oplus$ with the atom $c$ which is an argument of the outer $\oplus$;

• •

$\emptyset\vdash(a\ b)(b\ c)\curlywedge_{\mathsf{\{C,AC\}}}\mathsf{or}(\mathsf{or}(\mathsf{g}(a),\mathsf{g}(b)),\mathsf{g}(c))$;

• •

$\emptyset\vdash(a\ b)\curlywedge_{\mathsf{\{C,AC\}}}\forall[a]\mathsf{or}(\mathsf{or}((a\oplus b),(b\oplus c)),(a\oplus c))$;

• •

$(a\ b)\curlywedge_{\mathsf{\{C,AC\}}}X\vdash\forall[a]\mathsf{or}(\mathsf{or}((a\oplus X),g(c)),g(a))\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{\{C,AC\}}}}}\forall[b]\mathsf{or}(\mathsf{or}(g(c),((a\ b)\cdot X\oplus b)),g(b))$.

The theorem below extends Theorem 5, relating fixed-point constraints to fixed-point equalities, for the case in which equational theories $\mathsf{A},\mathsf{C}$ and $\mathsf{AC}$ are involved.

Theorem 16**.**

Let $\Upsilon,\pi$ and $t$ be an $\mathsf{E}$-fixed-point context, a permutation and a nominal term, respectively. \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge_{\mathsf{E}}t iff \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\cdot t\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}t.

Proof 5.1**.**

The proof is by induction on the derivation, similar to the proof of Theorem 5, except for the use of rules dealing with function symbols modulo $\mathsf{E}$. The rule for associative symbols is the same as for syntactic symbols; we consider the cases of commutative and associative-commutative symbols.

• •

Suppose that \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge_{\mathsf{E}}\mathsf{f}^{\mathsf{C}}(t_{0},t_{1}), therefore, rule $(\mathbf{\curlywedge_{\mathsf{E}}\mathsf{f}^{\mathsf{C}}})$ was applied, and one gets \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\cdot(\mathsf{f}^{\mathsf{C}}(t_{0},t_{1}))\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}\mathsf{f}^{\mathsf{C}}(t_{0},t_{1}), and the result follows trivially. The other direction is also trivial.

• •

Suppose that \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge_{\mathsf{E}}\mathsf{f}^{\mathsf{AC}}(t_{0},\ldots,t_{n}), therefore, rule $(\mathbf{\curlywedge_{\mathsf{E}}\mathsf{f}^{\mathsf{AC}}})$ was applied, and one gets \Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\cdot(\mathsf{f}^{\mathsf{AC}}(t_{0},\ldots,t_{n}))\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}\mathsf{f}^{\mathsf{AC}}(t_{0},\ldots,t_{n}), and the result follows trivially. The other direction is also trivial.

5.2. From freshness to $\mathsf{E}$-fixed-point constraints and back again

In [ARdCSFNS18] relations $\approx_{\{\alpha,\mathsf{A}\}}$, $\approx_{\{\alpha,\mathsf{C}\}}$, $\approx_{\{\alpha,\mathsf{AC}\}}$ and their combination $\approx_{\{\mathsf{A},\mathsf{C},\mathsf{AC}\}}$ were defined as extensions of $\mathrel{{\approx}_{\scriptstyle{\alpha}}}$ using the standard approach via freshness constraints (see the rules in Figures 1 and 2) but using specific rules for associative, commutative and associative-commutative symbols. We recall those rules in Figure 10.

Using a generalisation of the functions $[\_]_{\curlywedge}$ and $[\_]_{\#}$ defined in Section 3.3, we can obtain results that extend Theorem 6 and Theorem 7 to the equational case. The functions $[\_]_{\curlywedge}^{\mathsf{E}}$ and $[\_]_{\#}^{\mathsf{E}}$ defined below are the natural extension of the previous translation functions.

The mapping $[\_]_{\curlywedge}^{\mathsf{E}}$ associates each primitive freshness constraint in $\Delta$ with a primitive fixed-point constraint:

[TABLE]

This mapping extends directly to contexts. We denote by $[\Delta]_{\curlywedge}^{\mathsf{E}}$ the image of $\Delta$ under $[\_]_{\curlywedge}^{\mathsf{E}}$.

The mapping $[\_]_{\#}^{\mathsf{E}}$ associates each primitive fixed-point constraint in $\Upsilon$ with a primitive freshness context:

[TABLE]

We denote by $[\Upsilon]_{\#}^{\mathsf{E}}$ the union of the freshness contexts obtained by translating each constraint in $\Upsilon$ using $[\_]_{\#}^{\mathsf{E}}$.

Theorem 17**.**

1. (1)

\Delta\vdash a\#t\Leftrightarrow[\Delta]^{\mathsf{E}}\vdash\reflectbox{\mathsf{N}}c.(a\ c)\curlywedge_{\mathsf{E}}t. 2. (2)

\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\pi\curlywedge_{\mathsf{E}}t\Leftrightarrow[\Upsilon]_{\#}^{\mathsf{E}}\vdash\overline{\texttt{supp}(\pi)\setminus\{\overline{c}\}\#t}.

Proof 5.2**.**

The proof follows the same lines of the proof of Theorem 6. We discuss only the proof of part (1). The proof is by induction on rules of Figure 1 used in the derivation of $\Delta\vdash a\#t$. We show only the cases corresponding to function symbols.

$(\Longrightarrow)$**

• •

Rule $(\mathbf{\#f})$

In this case $t=\mathsf{f}^{\mathsf{E}}t^{\prime}$, for some theory $\mathsf{E}$. The analysis is based on the specific theory:

1. (1)

$\mathsf{f}^{\mathsf{E}}=\mathsf{f}^{\mathsf{A}}$**

This case is analogous to the case in which $\mathsf{E}=\emptyset$. 2. (2)

$\mathsf{f}^{\mathsf{E}}=\mathsf{f}^{\mathsf{C}}$**

There is a proof $\Pi$ of the form

tensy

\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 25.58179pt\hbox{\displaystyle\penalty 1\Pi}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=58.66359pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\Delta\vdash a#(t_{1},t_{2})}}}}\hskip 5.0pt plus 1.0fil\penalty 2

* $(\mathbf{\#f})$*

$\displaystyle\Delta\vdash a\#\mathsf{f}^{\mathsf{C}}(t_{1},t_{2})$

**

By induction hypothesis, there exists a proof $\Pi^{\prime}$ of [\Delta]^{\mathsf{E}}_{\curlywedge}\vdash\reflectbox{\mathsf{N}}c_{a}.(a\ c_{a})\curlywedge_{\mathsf{E}}(t_{1},t_{2}). Therefore, there is a proof of the form

tensy

\displaystyle\penalty 1\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 39.07158pt\hbox{\displaystyle\penalty 1\Pi_{1}^{{}^{\prime}}}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=88.44318pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle[\Delta]^{\mathsf{E}}{\curlywedge}\vdash\reflectbox{$\mathsf{N}$}c{a}.(a\ c_{a})\curlywedge_{\mathsf{E}}t_{1}}}}}\hskip 5.0pt plus 1.0fil\penalty 2\quad\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 39.07158pt\hbox{\displaystyle\penalty 1\Pi_{2}^{{}^{\prime}}}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=88.44318pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle[\Delta]^{\mathsf{E}}{\curlywedge}\vdash\reflectbox{$\mathsf{N}$}c{a}.(a\ c_{a})\curlywedge_{\mathsf{E}}t_{2}}}}}\hskip 5.0pt plus 1.0fil\penalty 2

* $(\mathbf{\curlywedge_{\mathsf{E}}tuple})$*

\displaystyle[\Delta]^{\mathsf{E}}_{\curlywedge}\vdash\reflectbox{\mathsf{N}}c_{a}.(a\ c_{a})\curlywedge_{\mathsf{E}}(t_{1},t_{2})

**

From [\Delta]^{\mathsf{E}}_{\curlywedge}\vdash\reflectbox{\mathsf{N}}c_{a}.(a\ c_{a})\curlywedge_{\mathsf{E}}t_{i} one can derive that [\Delta]^{\mathsf{E}}_{\curlywedge}\vdash\reflectbox{\mathsf{N}}c_{a}.(a\ c_{a})\cdot t_{i}\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}t_{i}, by Theorem 16, for ($i=1,2$). By applying rule $(\mathbf{\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}\mathsf{f}^{\mathsf{C}}})$, it follows that

[TABLE]

and the result follows from Theorem 16. 3. (3)

$\mathsf{f}^{\mathsf{E}}=\mathsf{f}^{\mathsf{A}}$**

The proof is analogous to the case above.

($\Longleftarrow$) The interesting case is again for rule $(\mathbf{\curlywedge_{\mathsf{E}}\mathsf{f}^{\mathsf{C}}})$.

Suppose that [\Delta]_{\curlywedge}^{\mathsf{E}}\vdash\reflectbox{\mathsf{N}}c.(a\ c)\curlywedge_{\mathsf{E}}t_{1}\oplus t_{2}. We want to prove that $\Delta\vdash a\#t_{1}\oplus t_{2}$. From rule $(\mathbf{\curlywedge_{\mathsf{E}}\mathsf{f}^{\mathsf{C}}})$ we can conclude that

• •

either there exist proofs of [\Delta]_{\curlywedge}^{\mathsf{E}}\vdash\reflectbox{\mathsf{N}}c.(a\ c)\cdot t_{1}\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}t_{1} and [\Delta]_{\curlywedge}^{\mathsf{E}}\vdash\reflectbox{\mathsf{N}}c.(a\ c)\cdot t_{2}\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}t_{2}, and by Theorem 16 it follows that there exist proofs of [\Delta]_{\curlywedge}^{\mathsf{E}}\vdash\reflectbox{\mathsf{N}}c.(a\ c)\curlywedge_{\mathsf{E}}t_{1} and [\Delta]_{\curlywedge}^{\mathsf{E}}\vdash\reflectbox{\mathsf{N}}c.(a\ c)\curlywedge_{\mathsf{E}}t_{2}, and the result follows by induction hypothesis.

• •

or there exist proofs of [\Delta]_{\curlywedge}^{\mathsf{E}}\vdash\reflectbox{\mathsf{N}}c.(a\ c)\cdot t_{1}\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}t_{2} and [\Delta]_{\curlywedge}^{\mathsf{E}}\vdash\reflectbox{\mathsf{N}}c.(a\ c)\cdot t_{2}\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}t_{1}.

Since these equalities hold for any new name $c$ (not occurring in $t_{1}$ or $t_{2}$), then $a$ cannot be in the support of $t_{1}$ and $t_{2}$ and therefore $a$ is fresh in $t_{1}$ and $t_{2}$.

We can now relate $\alpha$-equivalence modulo $\mathsf{E}$ via freshness constrains ($\approx_{\{\alpha,\mathsf{E}\}}$) with its version via fixed-point constraints ($\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}$).

Theorem 18**.**

1. (1)

\Upsilon\vdash\reflectbox{\mathsf{N}}\overline{c}.\ s\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}t\Rightarrow[\Upsilon]_{\#}^{\mathsf{E}}\cup\Delta\vdash s\approx_{\{\alpha,\mathsf{E}\}}t, where $\Delta\vdash\overline{c}\#\texttt{Var}(s,t)$. 2. (2)

$\Delta\vdash s\approx_{\{\alpha,\mathsf{E}\}}t\Rightarrow[\Delta]^{\mathsf{E}}_{\curlywedge}\vdash s\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}t$.

Proof 5.3**.**

The proof is very similar to the proof of Theorem 7, except for the case of rules involving function symbols $\mathsf{f}^{\mathsf{E}}$, with $\mathsf{E}\neq\emptyset$, where the reasoning is similar to the one in the proof of Theorem 17.

5.3. Solving nominal $\mathsf{C}$-unification problems via fixed-point constraints

In this section we propose an approach to nominal unification modulo commutativity via the notion of fixed-point constraints.

For example, assuming $+$ is commutative, i.e., $X+Y=Y+X$, a problem of the form

[TABLE]

can be solved by unifying $(a\ b)\cdot X$ with $Y$ and $a$ with $X$, or $(a\ b)\cdot X$ with $X$ and $a$ with $Y$.

In [ARdCSFNS18], a simplification algorithm for solving nominal $\mathsf{C}$-unification was proposed. This algorithm was based on the standard nominal unification algorithm [UPG04] where $\alpha$-equivalence is defined w.r.t. the notion of freshness. Upon the input of a unification problem Pr, the algorithm outputs a finite family of triples of the form $\langle\nabla,\sigma,P\rangle$, where $\nabla$ is a freshness context, $\sigma$ a substitution and $P$ is a set of fixed-point equations, which are solved using a separate procedure.

In [ARdCSFNS17] it is proved that even a simple unification problem such as $(a\ b)\cdot X\mathrel{{\approx}_{\scriptstyle{\alpha}}}X$ (i.e., a problem consisting of just one fixed-point equation) could produce an infinite and independent set of solutions, whenever the signature contains commutative function symbols. For example, if $f$ is commutative, the following substitutions solve this equation: $\{X\mapsto a+b,X\mapsto f(a+b),X\mapsto[e](a+b,b+a),\ldots\}$. Therefore, it is not possible to obtain a finite and complete set of solutions for every solvable unification problem if solutions are expressed using freshness constraints and substitutions. However, we remark that the problem $+((a\ b)\cdot X,a)\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\alpha}^{?}(Y,X)$ mentioned above has in fact a finite number of most general solutions (indeed, two) if we solve it using fixed-point constraints. The most general unifiers are $\{X\mapsto a,Y\mapsto b\}$ and $\{Y\mapsto a,(a\ b)\curlywedge X\}$. This observation led us to use fixed-point constraints instead of freshness constraints to express solutions.

Similarly to Section 4, below we define the notion of nominal $\mathsf{C}$-unification in terms of $\mathsf{C}$-fixed-point constraints, and provide a nominal $\mathsf{C}$-unification unification algorithm specified by means of simplification rules.

In this section, as in Section 4, we assume a generator of new names exists, and remove the new quantifier from the syntax of unification problems.

{defi}

A $\mathsf{C}$-unification problem Pr is a pair $\langle\Phi,P\rangle$ where $P$ is a finite set of $\mathsf{C}$-equality constraints $s\stackrel{{\scriptstyle\curlywedge?}}{{\approx}}_{\mathsf{C}}t$ and $\Phi$ is a finite set of $\mathsf{C}$-fixed-point constraints $\pi\curlywedge_{\mathsf{C}}^{?}t$. To ease the notation, we will denote $s\stackrel{{\scriptstyle\curlywedge?}}{{\approx}}_{\mathsf{C}}t$ by $s\approx^{?}t$.

{defi}

[Solutions of $\mathsf{C}$-unification problems] A solution for a $\mathsf{C}$-unification problem $\texttt{Pr}=\langle\Phi,P\rangle$ is a pair $\langle\Upsilon,\sigma\rangle$, where the following conditions are satisfied

1. (1)

$\Upsilon\vdash\pi\curlywedge_{\mathsf{C}}t\sigma$, if $\pi\curlywedge_{\mathsf{C}}^{?}t\in\Phi$; 2. (2)

$\Upsilon\vdash s\sigma\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}t\sigma$, if $s\approx^{?}t\in P$. 3. (3)

$\Upsilon\vdash X\sigma\sigma\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}X\sigma$.

The set of solutions for a $\mathsf{C}$-unification problem Pr is denoted as $\mathcal{U}_{\mathsf{C}}(\texttt{Pr})$.

{defi}

[Most general solution and complete set of solutions]

• •

For $\langle\Upsilon,\sigma\rangle$ and $\langle\Psi,\delta\rangle$ in $\mathcal{U}_{\mathsf{C}}(\texttt{Pr})$, we say that $\langle\Upsilon,\sigma\rangle$ is * more general than* $\langle\Psi,\delta\rangle$, denoted $\langle\Upsilon,\sigma\rangle\preceq\langle\Psi,\delta\rangle$, if there exists a substitution $\rho$ satisfying $\Psi\vdash\sigma\rho\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}\delta$ and $\Psi\vdash\Upsilon\rho$.

• •

A subset $\mathcal{C}$ of $\mathcal{U}_{\mathsf{C}}(\texttt{Pr})$ is a complete set of solutions of Pr if for all $\langle\Psi,\sigma\rangle\in\mathcal{U}_{\mathsf{C}}(\texttt{Pr})$, there exits a $\langle\Upsilon,\delta\rangle\in\mathcal{C}$ such that $\langle\Upsilon,\delta\rangle\preceq\langle\Psi,\sigma\rangle$. We denote a complete set of solutions of the $\mathsf{C}$-unification problem Pr as $\mathcal{C}(\texttt{Pr})$.

Table 2 presents the simplification rules for $\mathsf{C}$-unification problems. They are derived from the deduction rules for judgements, as done for the syntactic case. The main difference is that now there are two rules for the simplification of fixed-point constraints involving commutative symbols (rules $(\mathbf{\curlywedge_{\mathsf{C}}\mathsf{f}^{\mathsf{C}}1})$ and $(\mathbf{\curlywedge_{\mathsf{C}}\mathsf{f}^{\mathsf{C}}2})$) and two rules to deal with equality of terms rooted by a commutative symbol (rules $(\mathbf{\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}\mathsf{f}^{\mathsf{C}}1})$ and $(\mathbf{\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}\mathsf{f}^{\mathsf{C}}2})$).

We write $\texttt{Pr}\Longrightarrow_{\mathsf{C}}\texttt{Pr}^{\prime}$ when $\texttt{Pr}^{\prime}$ is obtained from Pr by applying a simplification rule from Table 2 and we write $\stackrel{{\scriptstyle*}}{{\Longrightarrow}}_{\mathsf{C}}$ for the reflexive and transitive closure of $\Longrightarrow_{\mathsf{C}}$. We omit the subindex when it is clear from the context.

Lemma 19** (Termination of simplification for $\mathsf{C}$-unification problems).**

There is no infinite chain of reductions $\Longrightarrow_{\mathsf{C}}$ starting from a $\mathsf{C}$-unification problem Pr.

Proof 5.4**.**

Termination of the simplification rules follows directly from the fact that the following measure of the size of Pr is strictly decreasing: $[\texttt{Pr}]=(n_{1},M)$ where $n_{1}$ is the number of different variables used in Pr, and $M$ is the multiset of heights of equality constraints and non-primitive fixed-point constraints occurring in Pr.

Each simplification step either eliminates one variable (when an instantiation rule is used) and therefore decreases the first component of the interpretation, or leaves the first component unchanged but replaces a constraint with primitive ones and/or constraints where terms have smaller height.

The simplification rules (Table 2) specify a $\mathsf{C}$-unification algorithm: we apply the simplification rules in a problem Pr until we reach normal forms. In the case of a term rooted by a commutative symbol, two rules can be applied, so a tree of derivations is built. The termination property (Lemma 19) guarantees the tree is finite.

For the leaves in the tree (i.e., normal forms), the notions of consistency, failure, correctness can be defined as in Section 4 (see Definition 4.2). So, if a normal form contains equality constraints, or inconsistent fixed-point constraints of the form $\pi\curlywedge_{\mathsf{C}}^{?}a$ such that $\pi(a)\neq a$ then this normal form is a failure. Only leaves containing consistent fixed-point constraints produce solutions.

We now prove that the $\mathsf{C}$-unification algorithm is sound and complete. The proof is done in two stages, first we show that the non-instantiating rules preserve solutions if we consider all the branches of the derivation tree (here it is important to consider all the branches: due to the non-deterministic application of rules involving commutative operators, if we consider just one branch we may loose solutions). Then we show that the set of solutions computed from all the successful leaves is a complete set of solutions for the initial problem.

Lemma 20** (Correctness of non-instantiating rules).**

Let Pr be a $\mathsf{C}$-unification problem and $n$ a natural number. Assume $\texttt{Pr}\overset{{n}}{\Longrightarrow_{\mathsf{C}}}\texttt{Pr}^{\prime}_{i}$ $(i\in I)$ are all the reduction sequences of length smaller than or equal to $n$ starting from Pr that do not use instantiating rules $(\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}inst1)$ and $(\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}inst2)$. Then

1. (1)

$\mathcal{U}_{\mathsf{C}}(\texttt{Pr})=\bigcup_{i\in I}\mathcal{U}_{\mathsf{C}}(\texttt{Pr}^{\prime}_{i})$, and 2. (2)

if $\texttt{Pr}^{\prime}_{i}$ contains inconsistent reduced fixed-point constraints then $\mathcal{U}_{\mathsf{C}}(\texttt{Pr}^{\prime}_{i})=\emptyset$.

Proof 5.5**.**

For part (1), as for the proof of Lemma 13, we proceed by induction on $n$, but here we need to consider all the branches of length smaller than or equal to $n$ in the derivation tree to ensure completeness.

The interesting cases are for the rules involving $\mathsf{C}$ function symbols, all the other cases are very similar to the proof of Lemma 13.

• •

Suppose that the last step of a simplification chain has the form

[TABLE]

In this case, the rule used is either $(\curlywedge_{\mathsf{C}}\mathsf{f}^{\mathsf{C}}1)$ or $(\curlywedge_{\mathsf{C}}\mathsf{f}^{\mathsf{C}}2)$.

Assume $i=0$ and $(\curlywedge_{\mathsf{C}}\mathsf{f}^{\mathsf{C}}1)$ was used (the case $i=1$ is identical).

There is another reduction sequence of the same length using $(\curlywedge_{\mathsf{C}}\mathsf{f}^{\mathsf{C}}2)$ and ending on $\texttt{Pr}_{n}^{1}$ (the same problem with $i=1$).

Let $\langle\Psi,\sigma\rangle\in\mathcal{U}(\texttt{Pr}_{n-1}$) be a solution for $\texttt{Pr}_{n-1}$:

1. (1)

$\Psi\vdash\pi^{\prime}\curlywedge_{\mathsf{C}}t\sigma$, for all $\pi^{\prime}\curlywedge^{?}t\in\texttt{Pr}^{\prime}$ and $\Psi\vdash\pi\curlywedge_{\mathsf{C}}\mathsf{f}^{\mathsf{C}}(s_{0},s_{1})\sigma$. 2. (2)

$\Psi\vdash t\sigma\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}s\sigma$, for all $t\approx^{?}s\in\texttt{Pr}^{\prime}$.

Since $\Psi\vdash\pi\curlywedge_{\mathsf{C}}\mathsf{f}^{\mathsf{C}}(s_{0},s_{1})\sigma$ and $\mathsf{f}^{\mathsf{C}}(s_{0},s_{1})\sigma=\mathsf{f}^{\mathsf{C}}(s_{0}\sigma,s_{1}\sigma)$, it follows that $\Psi\vdash\pi\curlywedge_{\mathsf{C}}\mathsf{f}^{\mathsf{C}}(s_{0}\sigma,s_{1}\sigma)$. From $(\mathbf{\curlywedge_{\mathsf{E}}\mathsf{f}^{\mathsf{C}}})$, one has that either there exist a proof for $\Psi\vdash\pi\cdot s_{0}\sigma\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}s_{i}\sigma$ and $\Psi\vdash\pi\cdot s_{1}\sigma\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}s_{(i+1)mod\ 2}\sigma$, for $i=0$ or for $i=1$. Therefore, $\langle\Psi,\sigma\rangle\in\mathcal{U}(\texttt{Pr}_{n}^{0})$ or $\langle\Psi,\sigma\rangle\in\mathcal{U}(\texttt{Pr}_{n}^{1})$ and the result follows.

The other direction is similar: if $\langle\Psi,\sigma\rangle\in\mathcal{U}(\texttt{Pr}_{n}^{i})$, then $\langle\Psi,\sigma\rangle\in\mathcal{U}(\texttt{Pr}_{n-1})$.

• •

Suppose the last step of the simplification chain has the form

[TABLE]

where $\texttt{Pr}_{n}^{i}=\texttt{Pr}^{\prime}\cup\{s_{0}\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}t_{i},s_{1}\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}t_{(i+1)mod\ 2}\}$.

As above, it follows that there two branches of this form, for $i=0$ and $i=1$.

Let $\langle\Psi,\sigma\rangle\in\mathcal{U}(\texttt{Pr}_{n-1}$) be a solution for $\texttt{Pr}_{n-1}$. In particular, $\Psi\vdash\mathsf{f}^{\mathsf{C}}(s_{0}\sigma,s_{1}\sigma)\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}\mathsf{f}^{\mathsf{C}}(t_{0}\sigma,t_{1}\sigma)$. By applying rule $(\mathbf{\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{E}}}}\mathsf{f}^{\mathsf{C}}})$, one has that there exist proofs of $\Psi\vdash s_{0}\sigma\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}t_{i}\sigma$ and $\Psi\vdash s_{1}\sigma\mathrel{\stackrel{{\scriptstyle\curlywedge}}{{\approx}}_{\scriptstyle{\alpha,\mathsf{C}}}}t_{(i+1)mod\ 2}\sigma$, for $i=0$ or $i=1$. Therefore, $\langle\Psi,\sigma\rangle\in\mathcal{U}(\texttt{Pr}_{n}^{i})$ for $i=0$ or $i=1$, and the result follows.

Similarly, if $\langle\Psi,\sigma\rangle\in\mathcal{U}(\texttt{Pr}_{n}^{i})$, then $\langle\Psi,\sigma\rangle\in\mathcal{U}(\texttt{Pr}_{n-1})$.

The second part of the lemma follows directly from the fact that inconsistent constraints are not derivable, therefore have no solutions.

As in Section 4, when Pr is a successful leaf, $\langle\texttt{Pr}\rangle_{\mathtt{\it{sol}}}$ consists of the composition $\sigma$ of all substitutions applied through the simplification steps and the fixed point context obtained.

Theorem 21** (Soundness and Completeness).**

Let $\texttt{Pr}=\langle\Upsilon,P\rangle$ be a $\mathsf{C}$-unification problem and let $\{\texttt{Pr}^{\prime}_{i}\mid\texttt{Pr}\overset{*}{\Longrightarrow_{\mathsf{C}}}\texttt{Pr}^{\prime}_{i}~{}and~{}\texttt{Pr}^{\prime}_{i}\mbox{ successful normal form}\}$ be the set of all the successful normal forms of Pr (i.e., leaves in the derivation tree without equality constraints or inconsistent fixed-point constraints).

1. (1)

If $\langle\Phi,\sigma\rangle\in\bigcup\langle\texttt{Pr}^{\prime}_{i}\rangle_{\mathtt{\it{sol}}}$ then $\langle\Phi,\sigma\rangle\in\mathcal{U}(\texttt{Pr})$, and 2. (2)

If $\langle\Phi,\sigma\rangle\in\mathcal{U}(\texttt{Pr})$, there exists $\langle\Phi^{\prime},\sigma^{\prime}\rangle$ such that $\langle\Phi^{\prime},\sigma^{\prime}\rangle\in\bigcup\langle\texttt{Pr}^{\prime}_{i}\rangle_{\mathtt{\it{sol}}}$ and $\langle\Phi^{\prime},\sigma^{\prime}\rangle\preceq\langle\Phi,\sigma\rangle$, that is, the set $\bigcup\langle\texttt{Pr}^{\prime}_{i}\rangle_{\mathtt{\it{sol}}}$ is a complete set of solutions.

Proof 5.6**.**

The proof is by induction on the length of a derivation $\texttt{Pr}{\Longrightarrow}^{*}\texttt{Pr}^{\prime}_{i},$ distinguishing cases according to the first rule used. By Lemma 20, it is sufficient to check generality of solutions after each application of instantiation rules. If the first step uses a non-instantiating rule, then the previous lemma, together with the induction hypothesis, ensures that the set of solutions of Pr is exactly the set of solutions of its children. If the first step is instantiating, we proceed as in the proof of Theorem 14.

{obs}

Using the approach to nominal $\alpha$-equivalence via freshness, a nominal $\mathsf{C}$-unification algorithm was presented in [ARdCSFNS18, ARdCSFNS17], which outputs solutions represented as triples $\langle\nabla,\sigma,P\rangle$ consisting of a freshness context $\nabla$, a substitution $\sigma$ and a set $P$ of fixed-point equations of the form $\pi\cdot X\approx_{\{\alpha,\mathsf{C}\}}^{?}X$.

As with standard nominal unification, one can use the functions $[\_]_{\#}$ and $[\_]_{\curlywedge}$ to translate solutions $\langle\nabla,\sigma,P\rangle$ of nominal $\mathsf{C}$-unification problems with freshness constraints as solutions $\langle[\nabla]_{\curlywedge}\cup\{P_{\curlywedge_{\mathsf{C}}}\},\sigma\rangle$ of nominal $\mathsf{C}$-unification problems via $\mathsf{C}$-fixed-point constraints, where $P_{\curlywedge_{\mathsf{C}}}=\{\pi\curlywedge_{\mathsf{C}}X\ |\ \pi\cdot X\approx_{\{\alpha,\mathsf{C}\}}^{?}X\in P\}$.

A set of simplification rules generalising the $\mathsf{C}$-unification algorithm to take into account $\mathsf{A}$ and $\mathsf{AC}$ symbols was proposed in Ribeiro’s thesis [dCS19] following the freshness constraint approach. The main difficulty is in the rules to deal with the $\mathsf{AC}$ symbols and with treatment of fixed-point equations of the form $\pi\cdot X\approx^{?}_{\{\alpha,\mathsf{AC}\}}X$. Analytical proofs of soundness and completeness of such rules were given, and a formalisation in Coq was developed for the $\mathsf{C}$-unification algorithm presented in [ARdCSFNS18]. In future work we will consider and relate $\mathsf{AC}$-nominal unification with freshness and fixed-point constraints.

Regarding the complexity of the $\mathsf{C}$-unification algorithm based on fixed-point constraints, we observe that in the syntactic case (i.e., without $\alpha$-equivalence rules), the $\mathsf{C}$-unification problem is NP-complete so it is expected that the algorithm will be exponential (Chapter 10 on Equational Unification in [BN98] surveys in detail the cases of $\mathsf{C}$ and $\mathsf{AC}$ unification). Comparing the nominal unification modulo $\mathsf{C}$ based on freshness and on fixed-point constraints, we can again notice that there is a one-to-one correspondence in the simplification rules, and thus the algorithms have the same behaviour during the simplification phase. The main difference is that using the freshness approach, a second algorithm is needed to solve fixed-point equations (generating an infinite number of solutions in general), which is avoided with the fixed-point approach.

6. Conclusions and Future Work

The notion of fixed-point constraint allowed us to obtain a finite representation of solutions for nominal $\mathsf{C}$-unification problems. This brings a novel alternative to standard nominal unification approaches in which just the algebra of atom permutations and the logic of freshness constraints are used to implement equational reasoning (e.g., [AK16, Cal13, CF08, Che10, FGM04]), and in particular to their extensions modulo commutativity, for which only infinite representations were possible in the standard approach. We have shown that with the new proposed approach the development of an algorithm to solve nominal equational problems modulo $\mathsf{C}$ is simpler, avoiding, thanks to the use of fixed-point constraints, the development of procedures for the generation of infinite independent sets of solutions.

In future work we plan to extend this approach to matching and unification modulo different equational theories as well as to the treatment of equational problems in nominal rewriting modulo. Future study will also address handling the case of Mal’cev permutative theories, which include $n$-ary functions with permutative arguments [Com93], as well as the more general and complex case of permutative equational theories [Sch89]. Finally, exploring the relation between Higher-Order Pattern unification in the style of Levy and Villaret [LV08] and nominal unification with fixed-point constrains would be also of great interest.