Théo Ladune

Gordon Clare

Pierrick Philippe

Félix Henry

Artificial Intelligence based Video Codec (AIVC) for CLIC 2022

This paper presents the AIVC submission to the CLIC 2022 video track. AIVC is a fully-learned video codec based on conditional autoencoders. The flexibility of the AIVC models is leveraged to implement rate allocation and frame structure competition to select the optimal coding configuration per-sequence. This competition yields compelling compression performance, offering a rate reduction of -26 % compared with the absence of competition.

Introduction

Over the last few years, deep neural networks (DNN) have been proposed to replace the handcrafted operations performed by conventional video coding algorithms (e.g. HEVC [START_REF] Sullivan | Overview of the high efficiency video coding (hevc) standard[END_REF] and VVC [START_REF] Bross | Developments in international video coding standardization after avc, with an overview of versatile video coding (VVC)[END_REF]). Thanks to their expressiveness and their ability to be globally optimized, DNN-based coding schemes have been showing fast-paced performance improvement. For instance, the learned image coder proposed by Cheng et al. [START_REF] Cheng | Learned image compression with discretized gaussian mixture likelihoods and attention modules[END_REF] is competitive with the image coding configuration of VVC.

Yet, the introduction of an additional temporal dimension makes video coding substantially more difficult than image coding. Even though numerous previous works address learned video coding [START_REF] Guo | Learning cross-scale prediction for efficient neural video compression[END_REF][START_REF] Agustsson | Scale-space flow for end-to-end optimized video compression[END_REF][START_REF] Alexandre | Deep video compression for interframe coding[END_REF][START_REF] Hu | Improving deep video compression by resolution-adaptive flow coding[END_REF][START_REF] Hu | FVC: A new framework towards deep video compression in feature space[END_REF][START_REF] Ladune | AIVC: Artificial intelligence based video codec[END_REF], conventional algorithms remain the best performing approaches. This assessment is supported by the CLIC 2021 video track results, which was won by a perceptually optimized VVC submission [START_REF] Philippe | Coding standards as anchors for the CVPR CLIC video track[END_REF].

The processing of a video frame by a conventional and a learned video codec share many similarities. Both approaches compute a prediction of the frame to be coded, based on previously transmitted frames. Then only the unpredicted part is sent. While conventional and learned codecs rely on the same basic principles, a significant difference arises when one takes a closer look. For each step of the processing, conventional approaches feature a large number of coding modes (i.e. different operations available), enabling the selection of the most suited operation for the signal to compress. This selection is performed at a pixel level, allowing for fine-grain content adaptation. On the contrary, learned approaches tend to perform the same processing on all input data, which limits content adaptation.

The goal of the CLIC 2022 video track is to compress several 10-second video sequences into an allocated bits budget, while obtaining the best reconstruction quality. These videos exhibit a great variety of spatial and temporal complexity. As such, it is possible to save bits for simple signals (which require fewer bits to be properly reconstructed) and invest these bits into more complex content. While this competition is easily achieved for conventional codecs, it is more challenging for learned ones.

In this paper, we propose to use AIVC [START_REF] Ladune | AIVC: Artificial intelligence based video codec[END_REF], an opensource learned video codec, and to adapt it for the CLIC 2022 video track. In order to cope with the wide variety of the video sequences, we carry out large-scale competition among the different possibilities offered by AIVC: multiple quality levels and flexible frame structures (intra-frame period, GOP size). Moreover, a simple filtering is added as a preprocessing option to target the low bitrate track. In short, this paper illustrates how to obtain the best results from a fully learned video codec in a practical context.

The AIVC codec

This section describes AIVC, an end-to-end learned video codec. More technical details are provided in [START_REF] Ladune | AIVC: Artificial intelligence based video codec[END_REF], open-source models and several illustrations are available at https://orange-opensource.github.io/AIVC/.

Architecture overview

AIVC performs the coding of one video frame x t , while exploiting information from up to two already transmitted (i.e. available at the decoder) reference frames xp and xf . AIVC architecture is presented in Fig. 1. It is based on two conditional autoencoders: MNet and CNet. Unlike the usual analysis-synthesis autoencoder, a conditional autoencoder [START_REF] Ladune | Conditional coding for flexible learned video compression[END_REF] features a decoder-side conditioning transform. This conditioning transform aims to compute relevant information from decoder-side quantities, which reduces the amount of bits sent from the encoder to the decoder. MNet stands for motion network and is responsible for estimating and conveying motion information. This information is then used by a motion compensation algorithm to obtain a temporal prediction xt . Motion information is composed of two pixel-wise motion maps v p and v f (one for each reference frame) as well as a bi-directional prediction weighting β. Furthermore, MNet also computes and conveys a coding mode selection α, which arbitrates between two possible coding modes.

The first coding mode is called Skip mode. It is a direct copy of the temporal prediction, with no transmission associated. Consequently, Skip mode is particularly dedicated to the stationary areas, well predicted enough to be directly copied. The second coding mode relies on CNet to transmit the areas of x t not present in the prediction xt i.e. the areas for which the prediction is not accurate enough. In the end, both coding mode contributions are summed up to obtain the decoded frame xt .

The analysis and synthesis architecture proposed in [START_REF] Cheng | Learned image compression with discretized gaussian mixture likelihoods and attention modules[END_REF] is used for MNet and CNet. The conditioning transform replicates the analysis architecture. These transforms are based on convolutional layers with attention modules and residual blocks. Moreover, AIVC relies on hyperpriors to perform the entropy coding. The AIVC encoder has around 17 million parameters. The AIVC decoder has 34 million parameters which requires 136 MBytes of storage.

Training

The purpose of the training stage is to prepare the model to compress frames with zero, one or two reference frames available. To this end, a training example consists of the successive coding of 3 frames (see Fig. 2). This coding configuration features an I-frame (no reference), a P-frame (one reference) and B-frame (two references). The model parameters are learned through a stochastic gradient descent which aims to minimize the following loss function over the 3 frames:

L λ = 2 t=0 D (x t , xt ) + λ (R m + R c ) . (1)
In

Decoder conditioning

During the encoding and decoding process, the latent variables of AIVC are mapped to a binary code using the arithmetic coder torchac [START_REF] Mentzer | Practical full resolution learned lossless image compression[END_REF]. This step is particularly sensitive to a potential drift due to floating point computations. Such a drift might arise as the encoding and decoding happen on two different devices. To circumvent this, the decoder is made resilient to cross-platform encoding/decoding through a light quantization of its internal parameters.

Coding choices competition

A per-sequence competition among the different coding choices of AIVC is implemented to obtain better quality at both challenge rate targets. Given a set of coding choices C = {c 1 , . . . , c N }, AIVC performs the coding of the video sequence with each coding choice c i to obtain its rate-distortion cost:

J ci (λ) = D ci + λR ci , (2)
Where D denotes the distortion (based on the MS-SSIM), R the rate and λ an external rate constraint. Finally, the optimal coding choice c is chosen in order to minimize the rate-distortion cost of the video sequence:

c = argmin ci∈ C J ci (λ) . (3)
Frames structure-The CLIC sequences exhibit various temporal behaviors: some sequences present important motions while others have large motionless areas. In order to take into account this diversity, different frame structures are tested by the AIVC encoder. The ability of AIVC to process I, P and B frames is leveraged by evaluating several intra periods (distance between I frames) and GOP sizes (distance between references). As such, an optimal frame structure is chosen per-sequence. The green and yellow curves in Fig. 3 present the benefits of frame structure competition over the initial models with a fixed frame structure.

Rate allocation-Some video sequences of the CLIC 2022 dataset can be compressed into a smaller number of bits while still offering an acceptable visual quality. As such, it is relevant to save bits for these easy-to-compress sequences in order to invest those bits into more challenging sequences. In practice, each sequence is compressed with the 8 encoder-decoder pairs and the best one is chosen sequence-wise. The orange curve in Fig. 3 presents the benefits of adding the rate allocation competition to the frame structure competition. This extended competition allows for a significant increase in quality at the 1 Mbit/s rate target. Yet, the 100 kbit/s target remains unreachable for our current systems.

Preprocessing-In order to compress videos at lower rates, an optional preprocessing step is added to AIVC. This preprocessing consists of a bilinear spatial downsampling of the video, which removes high-frequency content known to be notably hard to compress. The video is then upsampled at the decoder-side to recover the original resolution. The usage of the downsampling preprocessing is added as a supplementary coding choice for the sequence-wise competition. The red curve in Fig. 3 presents the benefits of adding the downsampling option to the frame structure and rate allocation competitions. While this preprocessing option is added with the low-rate target in mind, it turns out to be also slightly beneficial at higher rates.

In the end, performing per-sequence competition of the available coding modes yields a significant performance increase compared to the raw AIVC models. Indeed, using coding mode competition offers a BD-rate of -26 % i.e. it requires 26 % less rate to achieve the same quality. This results in the submissions to the challenge validation stage shown in Table 1. The details of the different coding choices selected for both submissions is presented in Fig. 4. Compared to the high-rate submission, the low-rate one more often uses the downsampling option and relies on lower quality levels for the rate allocation.

Intra period

Lower

Quality level Higher Downsampling 32 64 128 320 Two modern video coding standards (HEVC and VVC) are used as anchors in Fig. 3. For fair comparison, these coding standards also benefit from rate allocation competition and also feature the downsampling option. While our learned codec AIVC offers promising performance, conventional approaches such as HEVC and VVC still obtain the best results. This may be due to their extensive usage of competition, where each pixel of a video can be processed in many different ways. This allows for fine-grain content adaptation and leads to better coding performance.

Q 1 Q 2 Q 3 Q 4 Q 5 Q 6 Q 7 Q 8 0 10

Limitations

Even though AIVC results show that learned video coding is a promising field, a few limitations still have to be overcome. The most promising area for improvement is the introduction of more content adaptation mechanisms within the codec, as discussed in Section 3. In this section, two others limitations of AIVC are discussed.

Quality metric-The issue of the quality metric used during the training stage is yet to be solved. For convenience, this work relies solely on the MS-SSIM to assess the quality of the decoded videos. However, recent work by Mentzer et al. [START_REF] Mentzer | Neural video compression using gans for detail synthesis and propagation[END_REF] shows the inadequacy of traditional quality metrics (PSNR, MS-SSIM, VMAF [START_REF] Netflix | VMAF -video multi-method assessment fusion[END_REF], PIM [START_REF] Bhardwaj | An unsupervised information-theoretic perceptual quality metric[END_REF], LPIPS [START_REF] Zhang | The unreasonable effectiveness of deep features as a perceptual metric[END_REF], FID [START_REF] Heusel | Gans trained by a two time-scale update rule converge to a local nash equilibrium[END_REF]) to predict the actual (subjective) quality of video content. The same work hints that an additional GAN-based distortion yields significant quality improvements. A similar conclusion is reached by the CLIC 2021 image track, where most of the top performing systems feature a GAN-based distortion term. We believe that AIVC could obtain better perceptual quality through the introduction of a GAN-based loss.

Test-train mismatch-A second limitation of AIVC is due to a train-test mismatch. To achieve reasonable training time, AIVC is trained using the smallest possible coding configuration which features a 2-frame intra period. For the CLIC 2022 challenge, the shortest intra period used is 32 frames and the longest is 320 frames. This causes an important change in the I frame importance between the training stage and the test stage. Consequently, AIVC learns a rate allocation strategy targeting a 2-frame intra period, which largely deviates from the test stage. This inconsistency may have an impact on the rate-distortion performance. This needs to be solved by using a bigger training configuration, at the cost of a longer training time.

Conclusion

This paper presents the AIVC submission to the CLIC 2022 video track. AIVC is a fully learned video codec, based on two conditional autoencoders. Thanks to its flexibility in frame structure and rate allocation, AIVC allows the performing of sequence-wise competition. Consequently, the optimal coding configuration is used for each sequence. This results in a rate reduction of 26 %.

By design, learned video codecs offer some interesting features for subjective quality as they do not operate through block-based operations. Yet, learned codecs are still outperformed by conventional video coding algorithms (HEVC, VVC) for objective metrics such as MS-SSIM. We strongly believe that the importance of competition in conventional systems allows for more content adaptation, resulting in state-of-the-art performance. This hints at relevant future works for learned coding, which should foster competition and content adaptation through the introduction of additional coding modes.

Figure 1 .

 1 Figure 1. Block diagram of AIVC. Γenc and Γ dec are feature-wise quantization gains as proposed in [9].

  the above equation, D denotes the distortion function between the original and compressed frame. It is implemented based on the MS-SSIM. The hyperparameter λ balances the distortion with the sum of MNet rate R m and CNet rate R c . The whole model is learned end-to-end from scratch and 8 different hyperparameters λ are used to obtain 8 encoder-decoder pairs, addressing various qualities.

Figure 2 .

 2 Figure 2. Training configuration.

Figure 3 .

 3 Figure 3. Benefits of per-sequence competition. FS stands for frame structure competition and DS denotes the possibility of downsampling. The black dots indicates the AIVC submissions to the challenge. Quality is measured as MS-SSIM dB = -10 log 10 (1 -MS-SSIM).

Figure 4 .

 4 Figure 4. Coding options selected for the CLIC 2022 validation set.

Table 1 .

 1 Submissions for the validation stage.

	Name	Decoder size Data size PSNR Decoding [MBytes] [MBytes] [dB] time [s]
	AIVC	884.7	3.55	26.198	16 069
	AIVC	884.9	36.63	30.994	25 364


F Montheillet
email: montheil@emse.fr

G Damamme

D Piot
email: cpiot@emse.fr

S L Semiatin
email: dlee.semiatin@wpafb.af.mil

Keywords: dynamic recrystallization, solute drag, Zener pinning, grain boundary mobility, modeling

A simple analytical model is proposed for estimating grain boundary mobility during dynamic recrystallization in metallic alloys. The combined effects of solutes (solute drag) and second phase particles (Zener pinning) on mobility are considered. The approach is based on (and is consistent with) a recently published mesoscale model of discontinuous dynamic recrystallization. The dependence of grain boundary mobility on solute concentration and particle size is summarized in the form of two-dimensional maps.

Grain boundary migration plays an important role in dynamic recrystallization because it is one of the main parameters controlling the final grain size after hot working of a material. In metallic alloys, the grain boundary mobility M is generally decreased by both solute atoms (solute drag effect) and second phase particles (Zener pinning) [1]. Within the range of large grain-boundary velocities involved in classical "discontinuous" dynamic recrystallization (DDRX), M is expected to drop monotonically with increasing solute concentration. By contrast, the grain boundary migration rate either falls to zero or remains unchanged according to whether the driving force is less or greater than the Zener pressure P z . Such discontinuous behaviour precludes any straightforward introduction of Zener pinning into models of DDRX, and it is therefore necessary to estimate an value of the mobility pertaining to a whole grain over its lifetime.

In a mesoscale "average field" model for DDRX recently published [2, 3], each grain is considered as a spherical "inclusion" of current diameter D and (homogeneous) dislocation density ρ interacting with a matrix of average dislocation density ρ . The grain size changes according to:

( )( ) dD d 2M ε = τ ε ρ -ρ , (1)
in which ε and ε are the strain and strain rate, respectively, and

2 µb τ ≈
is the line energy of dislocations. According to Eq. 1, each grain grows whenever its dislocation density is less than ρ , and shrinks in the opposite case. The evolution of dislocation density reflects strain hardening and dynamic recovery. Various equations have been proposed to describe such phenomena; most of them involve numerical computations. In the present work, however, the following simple power law is used, because it leads to closed-form analytical expressions:

1 d d H ν+ ν ρ ε = ρ , (2)
in which 0 ν ≥ , and H has the dimension of dislocation density (µm -2 ). Note that Eq. 2 is associated with the classical macroscopic (power law) equation

( ) s n 1 K σ = ε + ε
, in which K, ε 1 , and the macroscopic strain-hardening parameter ( ) s n 1 2 2 = + ν are constants. During the of DDRX, ρ remains constant. Integration and combination of Eqs. 1 and 2 then lead to:

1 2M D H 1 2 ν+   τ ρ ρ ρ   = -     ε ν + ν +     . ( 3
)
When the grain vanishes, its dislocation density reaches its maximum value ! " Schematic dependence of mobility with respect to the dislocation density in the grain

M 1 M ρ ρ 2 z ρ end ρ 0
The average mobility pertaining to the grain over its lifetime (or, equivalently, pertaining to the whole set of grains under the DDRX steady state) is then given by:

1 M S S = , in which ( ) ( ) end 2 1 0 S M D d ρ ν = ρ ρ ρ ρ ∫ and ( ) end 2 0 S D d ρ ν = ρ ρ ρ ∫ (5)
In Eq. 5, the average of M(ρ) is weighted by the current surface of the grain. The additional factor ρ ν occurs because of the change of variable from time t to dislocation density ρ. Two cases are distinguished for evaluating the integral for S 1 :

-

If z end ρ + ρ ≤ ρ , , ( ) z 1 ρ ≤ ρ ν + , ( ) ( ) z end z 2 2 1 1 1 0 S M D d M D d ρ-ρ ρ ν ν ρ+ ρ = ρ ρ ρ + ρ ρ ρ ∫ ∫ (6a) -If z end ρ + ρ > ρ , , ( ) z 1 ρ > ρ ν + , ( ) z 2 1 1 0 S M D d ρ-ρ ν = ρ ρ ρ ∫ (6b)
Closed formed expressions are then obtained for the above integrals using Eq. 3 (steady state DDRX). Figure 2 shows that M drops rapidly with increasing Zener pressure P z for given deformation conditions, i.e., a given ρ . However, the influence of precipitates decreases for low values of ν, , when strain hardening is strong (per Eq. 2). ( )

1 z z M M 1 k = - ρ ρ in which ( )( )( )( ) ( ) 3 3 3 5 z k 3 3 3 4 3 5 1 2 ν+ ν+ = ν + ν + ν + ν + ν + (7)
It is interesting to note that a linear equation similar to the above has been recently proposed by Hutchinson .

[1].

$% &' (

The influence of on the grain boundary mobility can be described by the classical equation:

0 1 m M M 1 C = + β (8)
pertaining to the range of large migration rates occurring during [4]. Here, M 0 is the mobility in the pure metal, C m is the atomic concentration (atoms/m 3 ) of solute in the matrix, and β a constant. It is more convenient to write Eq. 8 in a slightly modified form:

( )

0 1 m s M M 1 C C = + α (8a)
in which the maximum ( ) solute concentration C s (which is a function of temperature, and may be modified under deformation conditions) has been introduced, and α is a non-dimensional constant. Contrary to the case of Zener pinning, it is not possible here to use a linear expansion of Eq. 8a, since m s C C is expected to vary over the whole range between 0 and 1, or even exceed unity (supersaturation).

The grain boundary mobility in particle and solute-containing metals undergoing DDRX is therefore obtained by combining Eqs. 7 (assuming here that its validity range extends up to M = 0) and 8a, viz., ( ) ( )

z z 0 m s 1 k M M 1 C C - ρ ρ = + α ( 9
)
) * )

Assuming spherical particles, the Zener pressure is given by [4]:

( ) 2 z P 2 n d = π γ (10)
in which γ is the surface energy of the precipitates, n is the number of precipitates per unit volume, and d denotes their diameter. In addition, alloy atom conservation leads to the following equation:

( ) 3 m p C 6 d n C C + π = (11)
in which p C is the concentration (atoms/m 3 ) of alloy element in each precipitate, and C is the overall alloy concentration. Combining Eqs. 10 and 11 yields:

m z p C C P 3 C d - = γ . ( 12
)
Eq. 9 can then be written in the form:

s m s z 0 m s C C C C 1 k d M M 1 C C - -δ = + α with p s 3 C C γ δ = τ ρ (13)
Here, δ is a constant (with units of length) for given deformation conditions. The dependence of 0 M M on d and C m can then be plotted in a two-dimensional diagram, for given overall concentration C. However, an additional condition must be fulfilled, ,

( ) c L d L d 1 > > , in
which L denotes the average center-to-center distance between precipitates, and the critical ratio

( ) c
L d means that the Zener pinning theory is likely to hold only for sufficiently widely-spaced precipitates. Using 3 n 1 L = , Eq. 11 can then be recast in the form:

1 3 p s s m s C C L d 6 C C C C   π =   -   . ( 14
)
Substitution of this expression for L d in the above inequality and solving for m s C C leads to the condition:

( ) p s m 3 s s c C C C C C C 6 L d π > - (15)
to be fulfilled by the solute concentration C m .

An example calculation of the grain-boundary mobility as a function of material and alloy parameters is shown in Figure 3

+ ,

A model has been developed to estimate the combined effect of solutes and precipitates on the grain boundary mobility under conditions of dynamic recrystallization. Although the various material parameters are not well known, it nevertheless indicates general trends and orders of magnitude that can be used as inputs for modeling DDRX in metallic alloys. Conversely, a recently-published, mesoscale model of DDRX enables the mobility to be determined from the steady-state flow stress and average grain size measurements [3]. It is thus also possible to estimate unknown material parameters from such data.

, +

This work was conducted as part of a research program on the modeling of the thermomechanical processing of superalloys, supported by Universal Technology Corporation, Dayton, OH, USA, under Contract N° 08-S587-002-C1. The support and encouragement of the Air Force Office of Scientific Research (Dr. Joan Fuller, Program Manager) is also greatly appreciated.

  setting D = 0 in Eq. 3. (The other solution, ρ = 0, corresponds to the nucleation of a new grain.)When stable, incoherent are present in the material, they exert a drag (Zener) pressure P z that opposes grain boundary motion. ≤ ρ , the migration rate is zero because the boundary is pinned by precipitates, > ρ , the boundary moves with mobility M 1 (the mobility in the absence of Zener drag), possibly affected by solute atoms (see below), as illustrated in Figure1. (However, M 1 is likely to depend also on the Zener pressure, a question which is left for later investigation.)

  Dependence of the grain boundary mobility M on Zener pressure ρ z (solid lines) and the corresponding linear approximations at low values of ρ z (broken lines). Numerical values of the slope, k z (Eq. 7), are given for ν = 0, 1, and 4, , for n s = 0.5, 0.25, and 0.1, respectively It appears that the linear approximations of M given by the initial slopes of the curves in Figure 2 are quite acceptable for 1 M M 0.3 > . This is relevant because DDRX requires sufficient grain boundary mobility for it to occur. For z 1 ρ ρ << , first order polynomial expansion of the integrals in Eq. 6a leads to a relation for M/M 1 :

C

  . For this example, p C = 2.23 × 10 28 atoms/m 3 was estimated for the case of niobium in hexagonal Ni 3 Nb precipitates, and it was assumed that s parameters are specified in the caption. In the cross-hatched area, the grain boundary mobility is zero. M values are meaningful only for according to the above analysis. Furthermore, the diagram exhibits a critical particle diameter d c . For d < d c , the mobility with C m (because the particle spacing becomes larger, thus weakening the Zener pressure). For d > d c , the mobility with increasing C m because solute effects predominate. For d = d c , grain boundary mobility is of the solute concentration.

  Diagram showing the dependence of the grain boundary mobility (M/M 0 ) on the particle diameter and solute concentration for an overall alloy concentration s C C = 0.5. Other parameters assumed for the model calculations comprised γ = 0.5 J/m 2 ; k z = 1.88 (associated with ν = 0 and a macroscopic strain hardening exponent of 0.5); τ = 3.306 × 10 -9 J/m and ρ = 510.2 /µm 2 (both estimated for a Ni-Nb alloy at 900°C, 10 -1 s -1 ); p C = 2.23 × 10 28 atoms/m 3 (for niobium in hexagonal Ni 3 Nb); C s = 0.85 × 10 28 atoms/m 3 (for niobium in nickel at 900 °C); and α = 2 [1] C.R. Hutchinson, H.S. Zurob, C.W. Sinclair and Y.J.M. Brechet: Scripta Mater. Vol. 59 (2008), p. 635. [2] J.P. Thomas, F. Montheillet and S.L. Semiatin: Metall. Mater. Trans. Vol. 38A (2007), p. 2095. [3] F. Montheillet, O. Lurdos and G. Damamme: Acta Mater. Vol. 57 (2009), p. 1602. [4] F.J. Humphreys, M. Hatherly: (Elsevier 2004).


Mnacho Echenim

Nicolas Peltier

Two Results on Separation Logic With Theory Reasoning

Introduction

In Separation Logic (see, e.g., [START_REF] Samin | Bi as an assertion language for mutable data structures[END_REF][START_REF] Reynolds | Separation Logic: A Logic for Shared Mutable Data Structures[END_REF]), recursive data structures are usually specified using inductively defined predicates. The recursive rules defining the semantics of these predicates may be provided by the user. This specification mechanism is similar to the definition of a recursive data type in an imperative programming language. For instance, a nonempty list segment may be specified by using the inductive rules below, where the atom x → (y) states that the memory location corresponding to x is allocated and refers to y. The symbol * is a special logical connective denoting the disjoint composition of heaps. ls(x, y) ⇐ x → (y) ls(x, y) ⇐ ∃x ′ . (x → (x ′ ) * ls(x ′ , y))

Sorted lists with elements inside the interval [u, v] may be specified as follows.

ils(x, y, u, v) ⇐ (x → (y) ∧ x ≤ v ∧ x ≥ u) ils(x, y, u, v) ⇐ ∃x ′ . (x → (x ′ ) * ils(x ′ , y, x, v) ∧ x ≤ v ∧ x ≥ u)

Many verification tasks can be reduced to an entailment problem in this logic. For example, to verify that some formula φ is a loop invariant, we have to prove that the weakest pre-condition of φ w.r.t. a finite sequence of transformations is a logical consequence of φ. Since techniques exist for computing automatically such pre-conditions, the problem may be reduced to an entailment problem between two SL formulas. Entailment problems can also be used to express typing properties. For instance one may have to check that the entailment ils(x, y, u, v) |= ls(x, y) holds, i.e., that a sorted list is a list, that v ≤ v ′ ∧ ils(x, y, u, v) |= ils(x, y, u, v ′ ) holds (if v is an upper bound then any number greater than v is also an upper bound) or that ils(x, y, u, v) * ils(y, z, v, v ′ ) |= ils(x, y, u, v ′ ) (the composition of two sorted lists is a sorted list). In general, the entailment problem is undecidable [START_REF] Iosif | Deciding entailments in inductive separation logic with tree automata[END_REF], and a lot of effort has been devoted to identifying decidable fragments and devising proof procedures, see e.g., [START_REF] Berdine | A decidable fragment of separation logic[END_REF][START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF][START_REF] Cook | Tractable reasoning in a fragment of separation logic[END_REF][START_REF] Enea | On automated lemma generation for separation logic with inductive definitions[END_REF][START_REF] Enea | Compositional entailment checking for a fragment of separation logic[END_REF][START_REF] Demri | Separation logic with one quantified variable[END_REF]. In particular, a very general class of decidable entailment problems is described in [START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF]. This fragment does not allow for any theory predicate other than equality and is defined by restricting the form of the inductive rules, which must fulfill 3 conditions, formally defined below: the progress condition (every rule allocates a single memory location), the connectivity condition (the set of allocated locations has a tree-shaped structure) and the establishment condition (every existentially quantified variable is eventually allocated). More recently, a 2-EXPTIME algorithm was proposed for such entailments [START_REF] Pagel | Complete entailment checking for separation logic with inductive definitions[END_REF], and we showed in [START_REF] Echenim | Entailment checking in separation logic with inductive definitions is 2-exptime hard[END_REF] that this bound is tight. To tackle entailments such as those given above, one must be able to combine spatial reasoning with theory reasoning, and the combination of SL with data constraints has been considered by several authors (see, e.g., [START_REF] Piskac | Automating separation logic using SMT[END_REF][START_REF] Qiu | Natural proofs for structure, data, and separation[END_REF][START_REF] Antonio | Separation logic modulo theories[END_REF][START_REF] Xu | Satisfiability of compositional separation logic with tree predicates and data constraints[END_REF][START_REF] Loc | Compositional satisfiability solving in separation logic[END_REF]). It is therefore natural to ask whether the above decidability result extends to the case where theory reasoning is considered. In the present paper, we show that this is not the case, even for very simple theories. More precisely, we establish two new results. First, we show that the entailment problem is undecidable for rules satisfying the above conditions if theory reasoning is allowed (Theorem 9). The result holds for a very wide class of theories, even for theories with a very low expressive power. For instance, it holds for the natural numbers with only the successor function, or with only the predicate ≤ (interpreted as usual). Second, we show that every entailment can be reduced to an entailment not containing equality (Theorem 13). The intuition is that all the equality and disequality constraints can be encoded in the formulas describing the shape of the data structures. The transformation increases the number of rules exponentially but it increases the size of the rules only polynomially (hence it preserves the complexity results in [6]). This result shows that the addition of the equality predicate does not increase the expressive power. It may be useful to facilitate the definition of proof procedures for the considered fragment.

Preliminaries

In this section, we define the syntax and semantics of the fragment of separation logic that is considered in the paper (see for instance [START_REF] O'hearn | Local reasoning about programs that alter data structures[END_REF][START_REF] Reynolds | Separation Logic: A Logic for Shared Mutable Data Structures[END_REF][START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF] for more details).

Syntax. Let V be a countably infinite set of variables. We consider a set P T of T -predicates (or theory predicates, denoting relations in an underlying theory of locations) and a set P S of spatial predicates, disjoint from P T . Each symbol p ∈ P T ∪P S is associated with a unique arity #(p). We assume that P T contains in particular two binary symbols ≈ and ≈ and a nullary symbol false.

Definition 1. Let κ be some fixed natural number. The set of SL-formulas (or simply formulas) φ is inductively defined as follows:

φ := emp x → (y 1 , . . . , y κ ) φ 1 ∨ φ 2 φ 1 * φ 2 p(x 1 , . . . , x #(p) ) ∃x. φ 1
where φ 1 , φ 2 are SL-formulas, p ∈ P T ∪ P S and x, x 1 , . . . , x #(p) , y 1 , . . . , y κ are variables.

A formula of the form x → (y 1 , . . . , y κ ) is called a points-to atom, and a formula p(x 1 , . . . , x #(p) ) with p ∈ P S is called a predicate atom. A spatial atom is either a points-to atom or a predicate atom. A T -atom is a formula of the form p(x 1 , . . . , x #(p) ) with p ∈ P T . An atom is either a spatial atom or a T -atom. A T -formula is either emp or a separating conjunction of T -atoms. A formula of the form ∃x 1 . . . . .∃x n . φ (with n ≥ 0) is denoted by ∃x. φ, where x = (x 1 , . . . , x n ). A formula is predicate-free (resp. disjunction-free, resp. quantifier-free) if it contains no predicate symbol in P S (resp. no occurrence of ∨, resp. of ∃). It is in prenex form if it is of the form ∃x.φ, where φ is quantifier-free and x is a possibly empty vector of variables. A symbolic heap is a prenex disjunction-free formula, i.e., a formula of the form ∃x.φ, where φ is a separating conjunction of atoms.

Let fv (φ) be the set of variables freely occurring in φ. We assume (using α-renaming if needed) that all existential variables are distinct from free variables and that distinct occurrences of quantifiers bind distinct variables. A substitution σ is a function mapping variables to variables. The domain dom(σ) of a substitution σ is the set of variables x such that σ(x) = x, and we let img(σ) = σ(dom(σ)). For any expression (variable, tuple of variables or formula) e, we denote by eσ the expression obtained from e by replacing every free occurrence of a variable x by σ(x) and by {x i ← y i | 1 ≤ i ≤ n} (where the x 1 , . . . , x n are pairwise distinct) the substitution such that σ(x i ) = y i and dom(σ) ⊆ {x 1 , . . . , x n }. For all sets E, card (E) is the cardinality of E. For all sequences or words w, w denotes the length of w. We sometimes identify vectors with sets, if the order is unimportant, e.g., we may write x \ y to denote the vector formed by the components of x that do not occur in y.

We assume that the symbols in P S ∪ P T ∪ V are words over a finite alphabet of some constant size, strictly greater than 1. For any expression e, we denote by size(e) the size of e, i.e., the number of occurrences of symbols1 in e. We define the width of a formula as follows:

width(φ1 ∨ φ2) = max(width(φ1), width(φ2)) width(∃x.φ) = width(φ) + size(∃x) width(φ1 * φ2) = width(φ1) + width(φ2) + 1 width(φ) = size(φ) if φ is an atom
Note that width(φ) coincides with size(φ) if φ is disjunction-free.

Inductive Rules. The semantics of the predicates in P S is given by user-defined inductive rules. To ensure decidability in the case where the theory only contains the equality predicate, these rules must satisfy some additional conditions (defined in [START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF]):

Definition 2. A (progressing and connected) set of inductive rules (pc-SID) R is a finite set of rules of the form p(x 1 , . . . , x n ) ⇐ ∃u. x 1 → (y 1 , . . . , y κ ) * φ where fv (x 1 → (y 1 , . . . , y κ ) * φ) ⊆ {x 1 , . . . , x n } ∪ u, φ is a possibly empty separating conjunction of predicate atoms and T -formulas, and for every predicate atom q(z 1 , . . . , z #(q) ) occurring in φ, we have z 1 ∈ {y 1 , . . . , y κ }. We let size(p(x) ⇐ φ) = size(p(x)) + size(φ), size(R) = Σ ρ∈R size(ρ) and width(R) = max ρ∈R size(ρ).

In the following, R always denotes a pc-SID. Note that the right-hand side of every inductive rule contains exactly one points-to atom, the left-hand side of which is the first argument x 1 of the predicate symbol (this condition is referred to as the progress condition), and that this points-to atom contains the first argument of every predicate atom on the right-hand side of the rule (the connectivity condition). Definition 3. We write p(x 1 , . . . , x #(p) ) ⇐ R φ if R contains a rule (up to αrenaming) p(y 1 , . . . , y #(p) ) ⇐ ψ, where x 1 , . . . , x #(p) are not bound in ψ, and

φ = ψ{y i ← x i | i ∈ {1, . . . , #(p)}}.
The relation ⇐ R is extended to all formulas as follows: φ ⇐ R φ ′ if one of the following conditions holds:

(i) φ = φ 1 • φ 2 (modulo AC, with • ∈ { * , ∨}), φ 1 ⇐ R φ ′ 1 , no free or existential variable in φ 2 is bound in φ ′ 1 and φ ′ = φ ′ 1 • φ 2 ; or (ii) φ = ∃x. ψ, ψ ⇐ R ψ ′ , x is not bound in ψ ′ and φ ′ = ∃x. ψ ′ . We denote by ⇐ +
R the transitive closure of ⇐ R , and by ⇐ * R its reflexive and transitive closure. A formula ψ such that φ ⇐ * R ψ is called an R-unfolding of φ. We denote by ≥ R the least transitive and reflexive binary relation on P S such that p ≥ R q holds if R contains a rule of the form p(y 1 , . . . , y #(p) ) ⇐ ψ, where q occurs in ψ. If φ is a formula, we write φ ≥ R q if p ≥ R q for some p ∈ P S occurring in φ.

Semantics.

Definition 4. Let L be a countably infinite set of locations. An SL-structure is a pair (s, h) where s is a store, i.e. a total function from V to L, and h is a heap, i.e. a partial finite function from L to L κ (written as a relation:

h(ℓ) = (ℓ 1 , . . . , ℓ κ ) iff (ℓ, ℓ 1 , . . . , ℓ κ ) ∈ h).
The size of a structure (s, h) is the cardinality of dom(h).

For every heap h, we define: loc(h) = {ℓ i | (ℓ 0 , . . . , ℓ κ ) ∈ h, i = 0, . . . , κ}. A location ℓ (resp. a variable x) is allocated in a heap h (resp. in a structure (s, h)) if ℓ ∈ dom(h) (resp. s(x) ∈ dom(h)). Two heaps h 1 , h 2 are disjoint if dom(h 1 ) ∩ dom(h 2 ) = ∅, in this case h 1 ⊎ h 2 denotes the union of h 1 and h 2 .

Let |= T be a satisfiability relation between stores and T -formulas, satisfying the following properties: s |= T x ≈ y (resp. s |= T x ≈ y) iff s(x) = s(y) (resp. s(x) = s(y)), s |= T false and s |= T χ * ξ iff s |= T χ and s |= T ξ. For all T -formulas χ, ξ, we write χ |= T ξ if s |= T χ =⇒ s |= T ξ holds for all stores s. Definition 5. Given formula φ, a pc-SID R and a structure (s, h), we write (s, h) |= R φ and say that (s, h) is an R-model (or simply a model if R is clear from the context) of φ if one of the following conditions holds.

φ = x → (y 1 , . . . , y κ ) and h = {(s(x), s(y 1 ), . . . , s(y κ ))}.

-

φ is a T -formula, h = ∅ and s |= T φ. -φ = φ 1 ∨ φ 2 and (s, h) |= R φ i , for some i = 1, 2. -φ = φ 1 * φ 2 and there exist disjoint heaps h 1 , h 2 such that h = h 1 ⊎ h 2 and (s, h i ) |= R φ i , for all i = 1, 2.
φ = ∃x. φ and (s ′ , h) |= R φ, for some store s ′ coinciding with s on all variables distinct from x.

-φ = p(x 1 , . . . , x #(p) ), p ∈ P S and (s, h) |= R ψ for some ψ such that φ ⇐ R ψ. If Γ is a sequence of formulas, then we write (s, h) |= R Γ if (s, h) satisfies at least one formula in Γ .
We emphasize that a T -formula is satisfied only in structures with empty heaps. This convention is used to simplify notations, because it avoids having to consider both standard and separating conjunctions. Note that Definition 5 is wellfounded because of the progress condition: the size of h decreases at each recursive call of a predicate atom. We write

φ |= R ψ if every R-model of φ is an R-model of ψ and φ ≡ R ψ if φ |= R ψ and ψ |= R φ.
Every formula can be transformed into prenex form using the well-known equivalences:

(∃x.φ) • ψ ≡ ∃x.(φ • ψ), for all • ∈ {∨, * }, where x ∈ fv (ψ).
Establishment. The notion of establishment [START_REF] Iosif | The tree width of separation logic with recursive definitions[END_REF] is defined as follows: Definition 6. A pc-SID is established if for every atom α, every predicate-free formula ∃x.φ such that α ⇐ * R ∃x.φ (up to a transformation into prenex form) and φ is quantifier-free, and every x ∈ x, φ is of the form x ′ → (y 1 , . . . , y κ ) * χ * ψ, where χ is a separating conjunction of equations (possibly emp) such that χ |= T x ≈ x ′ .

In the remainder of the paper, we assume that every considered pc-SID is established.

Sequents. We consider sequents denoting entailment problems and defined as follows: Definition 7. A sequent is an expression of the form φ 0 ⊢ R φ 1 , . . . , φ n , where R is a pc-SID and φ 0 , . . . , φ n are formulas. A sequent is disjunction-free if φ 0 , . . . , φ n are disjunction-free, and established if R is established. We define:

size(φ0 ⊢R φ1, . . . , φn) = Σ n i=0 size(φi) + size(R), fv (φ1, . . . , φn) = n i=0 fv (φi),
width(φ0 ⊢R φ1, . . . , φn) = max{width(φi), width(R), card (

n i=0 fv (φi)) | 0 ≤ i ≤ n}. Definition 8. A structure (s, h) is a countermodel of a sequent φ ⊢ R Γ iff s is injective, (s, h) |= R φ and (s, h) |= R Γ . A sequent is valid if it has no countermodel.
Two sequents are equivalent if they are both valid or both nonvalid2 .

The restriction to injective countermodels is for technical convenience only and does not entail any loss of generality.

An Undecidability Result

This section contains the main result of the paper. It shows that no terminating procedure for checking the validity of (established) sequents possibly exists, even for theories with a very low expressive power.

Theorem 9. The validity problem is undecidable for established sequents φ ⊢ R ψ if P T contains predicates S and S, where:

-S is interpreted as a relation S satisfying the following property: there exists a set of pairwise distinct locations x,y) and ¬S(x, y) are interpreted equivalently when x and y refer to distinct locations.

{α i , α ′ i , α ′′ i | i ∈ N} such that for all i ∈ N, (α i , α ′ i ) ∈ S, (α ′′ i , α ′ i ) ∈ S, and for all locations ℓ ∈ {α j , α ′ j , α ′′ j | j ∈ N} if α i = ℓ, (α i , ℓ) ∈ S and (α ′′ i , ℓ) ∈ S, then ℓ = α ′ i ; -S(
For instance, the hypotheses of Theorem 9 are trivially satisfied on the natural numbers if S is the successor function or if S is the usual order ≤, and S is ≥ (with

α i = 3.i, α ′ i = 3.i + 1, α ′′ i = 3.i + 2 in both cases, since α i + 1 ≈ ℓ ⇒ α ′ i ≈ ℓ and α i ≤ ℓ ∧ α ′′ i > ℓ ∧ ℓ = α i ⇒ α ′ i ≈ ℓ.
). More generally, the conditions hold if the domain is infinite and S is any injective function f such that f (x) = x. In this case, the sequences α i , α ′ i , α ′′ i may be constructed inductively: for every i ∈ N, α i is any element e such that both e and f (e) do not occur in

{α j , α ′ j , α ′′ j | j < i}, α ′ i is f (α i ) and α ′′ i is any element not occurring in {α j , α ′ j , α ′′ j | j < i} ∪ {α i , α ′ i }.
Note that in this case the locations α ′′ i are actually irrelevant, but these locations play an essential rôle in the undecidability proof when S is ≤. The remainder of the section is devoted the proof of Theorem 9.

Proof. The proof goes by a reduction from the Post Correspondence Problem (PCP). We recall that the PCP consists in determining, given two sequences of words u = (u 1 , . . . , u n ) and v = (v 1 , . . . , v n ), whether there exists a nonempty sequence (i 1 , . . . , i k ) ∈ {1, . . . , n} k such that u i1 . . . . , u i k = v i1 . . . . , v i k . It is wellknown that this problem is undecidable. We assume, w.l.o.g., that u i > 1 and v i > 1 for all i ∈ {1, . . . , n}. A word w such that w = u i1 . . . . , u i k = v i1 . . . . , v i k is called a witness. Positions inside words of the sequences (u 1 , . . . , u n ) and (v 1 , . . . , v n ) will be denoted by pairs (i, j), encoding the j-nth character of the words u i or v i . More formally, if p = (i, j), and w ∈ {u, v}, then we denote by w(p) the j-th symbol of the word w i , provided this symbol is defined. We write p ⊳ q if both u(p) and v(q) are defined and u(p) = v(q). Let m = max{ u i , v i | i ∈ {1, . . . , n}}. We denote by P the set of pairs of the form (i, j) with i ∈ {1, . . . , n} and j ∈ {1, . . . , m}, and by B the set of pairs of the form (i, 1). For w ∈ {u, v}, we denote by E w the set of pairs of the form (i, w i ), where i ∈ {1, . . . , n}, and we write (i, j) → w (i ′ , j ′ ) either i ′ = i, j < w i and j ′ = j + 1, or j = w i and j ′ = 1. Note that i ′ is arbitrary in the latter case (intuitively (i, j) → w (i ′ , j ′ ) states that the character corresponding to the position (i, j) may be followed in a witness by the character at position (i ′ , j ′ )). Let v be a vector of variables, where all elements p ∈ P are associated with pairwise distinct variables in v. To simplify notations, we will also denote by p the variable associated with p. We assume the vector v also contains a special variable ⊥, distinct from the variables p ∈ P. We construct a representation of potential witnesses as heaps. The encoding is given for κ = 6, although in principle this encoding could be defined with κ = 2 by encoding tuples as binary trees. Witnesses are encoded by linked lists, with links on the last argument, and starting with a dummy element (⊥, . . . , ⊥). Except for the first dummy element, each location in the list refers to two locations associated with pairs p, q ∈ P denoting positions inside the two sequences u 1 , . . . , u n and v 1 , . . . , v n respectively, and to three additional allocated locations the rôle of which will be detailed below.

W (x, v) ⇐ ∃x ′ . x → (⊥, ⊥, ⊥, ⊥, ⊥, x ′ ) * Wp,p(x ′ , v) where p ∈ B Wp,q(x, v) ⇐ ∃x ′ , y, z, u. x → (p, q, y, z, u, x ′ ) * W p ′ ,q ′ (x ′ , v) * P (y, ⊥) * P (z, ⊥) * P (u, ⊥)
where p ⊳ q, p → u p ′ and q → v q ′ Wp,q(x, v) ⇐ ∃y, z, u. x → (p, q, y, z, u, ⊥) * P (y, ⊥) * P (z, ⊥) * P (u, ⊥) where p = (i, ui ), q = (i, vi ), and p ⊳ q P (x, y) ⇐ x → (y, y, y, y, y, y) By construction, the structures that validate W (x, v) are of the form (s, h), where the store s verifies:

s(x) = ℓ and s(⊥) = ℓ ′ ; -for all i = 1, . . . , m ′ , s(p i ) = ℓ p i and s(q i ) = ℓ q i , where p i , q i ∈ P are such that p i ⊳ q i , p i → u p i+1 and q i → v q i+1 , and the heap h is of the form (with ℓ m ′ +1 = ℓ ′ ):

h = {(ℓ, ℓ ′ , ℓ ′ , ℓ ′ , ℓ ′ , ℓ ′ , ℓ 1 )} ∪ {(ℓ i , ℓ p i , ℓ q i , ℓ y i , ℓ z i , ℓ u i , ℓ i+1 ) i = 1, . . . , m ′ } ∪ {(ℓ y i , ℓ ′ , ℓ ′ , ℓ ′ , ℓ ′ , ℓ ′ , ℓ ′ ) i = 1, . . . , m ′ } ∪ {(ℓ z i , ℓ ′ , ℓ ′ , ℓ ′ , ℓ ′ , ℓ ′ , ℓ ′ ) i = 1, . . . , m ′ } ∪ {(ℓ u i , ℓ ′ , ℓ ′ , ℓ ′ , ℓ ′ , ℓ ′ , ℓ ′ ) i = 1, . . . , m ′ } .
Still by construction, we have p 1 = q 1 ∈ B, p m ′ ∈ E u and q m ′ ∈ E v , and there exists i such that p m ′ and q m ′ are of the form (i, u i ) and (i, v i ), respectively. This entails that the words u(p 1 ). . . . , u(p m ′ ) and v(p 1 ). . . . , v(p m ′ ) are of form u i1 . . . . .u i k and v j1 . . . . .v j k ′ , for some sequences (i 1 , . . . , i k ) and (j 1 , . . . , j k ′ ) of elements in {1, . . . , n}, and both words are identical. However the sequences (i 1 , . . . , i k ) and (j 1 , . . . , j k ′ ) may be distinct (but we have i 1 = j 1 and i k = j k ′ ).

To check that the PCP has a solution, we must therefore verify that there exists a structure of the form above such that (i 1 , . . . , i k ) = (j 1 , . . . , j k ′ ). To this purpose, we introduce predicates that are satisfied when this condition does not hold, i.e., such that either k = k ′ or i l = j l for some l ∈ {2, . . . , k-1}. This is done by using the additional locations ℓ y i , ℓ z i and ℓ u i to relate the indices I l = u i1 . . . . , u i l-1 +1 and J l = v j1 . . . . , v j l-1 + 1, corresponding to the beginning of the words u i l and v j l respectively in u i1 . . . . .u i k and v j1 . . . . .v j k ′ . The predicates relate the locations of the form ℓ y i , ℓ z i and ℓ u i using the relation S. More precisely, they are associated with rules that guarantee that all the countermodels of the right-hand side of the sequent will satisfy the following properties:

1. k = k ′ and for all l ∈ {1, . . . , k}, (ℓ y I l , ℓ z J l ) ∈ S and (ℓ u I l , ℓ z J l ) ∈ S. 2. i l = j l for 1 ≤ l ≤ k. Note that the hypothesis of the theorem ensures that the locations ℓ y i , ℓ z i and ℓ u i can be chosen in such a way that there is a unique location ℓ z i satisfying (ℓ y I l , ℓ z i ) ∈ S ∧ (ℓ u J l , ℓ z i ) / ∈ S, thus property 1 above can be used to relate the indices I l and J l , which, in turns, allows us to enforce property 2. Two predicates are used to guarantee that condition 1 holds for the countermodels. Predicate A is satisfied by those structures for which the condition is not satisfied for l = 1, and B is satisfied for those structures for which either k = k ′ or there is an l ∈ {1, . . . , k -1} such that the condition is satisfied at l, but not at l + 1. Thus the structures that satisfy W (x, v) and that are countermodels of the disjunction of A and B are exactly the structures for which k = k ′ and (ℓ y

I l , ℓ z J l ) ∈ S ∧ (ℓ u I l , ℓ z J l ) / ∈ S for l = 1, . . . , k.
Predicate C is then used to guarantee that for all 1 ≤ l ≤ k, p I l = q J l : this predicate is satisfied by the structures for which there is an l such that (ℓ y I l , ℓ z J l ) ∈ S ∧ (ℓ u I l , ℓ z J l ) / ∈ S holds but p I l = q J l . We first give the rules for predicate A. For conciseness, we allow for disjunctions in the right-hand side of the rules (they can be eliminated by transformation into dnf).

A(x, v) ⇐ ∃x ′ . x → (⊥, ⊥, ⊥, ⊥, ⊥, x ′ ) * A ′ (x ′ , v) A ′ (x, v) ⇐ ∃x ′ , y, z, u. x → (p, q, y, z, u, x ′ ) * W p ′ ,q ′ (x, v) * P (y, ⊥)
* P (z, ⊥) * P (u, ⊥) * (S(y, z) ∨ S(u, z)), for every p, q, p ′ , q ′ ∈ P Note that since y, z, u are allocated in distinct predicates, they must be distinct, hence S(y, z) is equivalent to ¬S(y, z) and S(u, z) is equivalent to ¬S(u, z).

We now define the rules for predicate B, which is meant to ensure that the condition "(ℓ y I l , ℓ z J l ) ∈ S and (ℓ u I l , ℓ z J l ) ∈ S" ( †) propagates, i.e., that if it holds for some l then it also holds for l + 1. This predicate has additional parameters y, y ′ , z, z ′ , u, u ′ corresponding to the locations ℓ y I l , ℓ y I l+1 , ℓ z Jj , ℓ z Jj+1 , ℓ u I l , ℓ u I l+1 which "break" the propagation of ( †). By definition y, y ′ , z, z ′ , u, u ′ must be chosen in such a way that the T -formula S(y, z) * S(u, z) * (S(y ′ , z ′ ) ∨ S(u ′ , z ′ )) holds. The predicates B a,b with a, b ∈ {0, 1, 2} allocate all the locations ℓ 1 , . . . , ℓ m ′ and in particular the "faulty" locations associated with y, y ′ , z, z ′ , u, u ′ . Intuitively, a (resp. b) denote the number of variables in {y, y ′ } (resp. {z, z ′ }) that have been allocated. The rules for predicates B a,b are meant to guarantee that the following conditions are satisfied for variables y and y ′ (similar constraints hold for z and z ′ ):

y is allocated before y ′ , -y is allocated for a variable p corresponding to the beginning of a word (p ∈ B), -when y has been allocated, no variable p ∈ B can occur on the right-hand side of a points-to atom until y ′ is allocated.

Several cases are distinguished depending on whether the locations associated with y and z (resp. y ′ and z ′ ) are in the same heap image of a location or not. Note that u and u ′ are allocated in the same rules as y and y ′ respectively. The predicate B also tackles the case where k = k ′ . This corresponds to the case where the recursive calls end with B 1,2 or B 2,1 in the last rule below, meaning that ( †) holds for some i, with either i = k and i < k ′ or i = k ′ and i < k. For the sake of conciseness and readability, we denote by w the vector of variables v, y, y ′ , z, z ′ , u, u ′ in the rules below. We also denote by φ ′ (y, z, u) the formula P (y, ⊥) * P (z, ⊥) * P (u, ⊥).

B(x, w) ⇐ x → (⊥, ⊥, ⊥, ⊥, ⊥, x ′ ) * B0,0(x ′ , w) * S(y, z) * S(u, z) * (S(y ′ , z ′ ) ∨ S(u ′ , z ′ )) B a,b (x, w) ⇐ ∃x ′ , y ′′ , z ′′ , u ′′ .x → (p, q, y ′′ , z ′′ , u ′′ , x ′ ) * B a,b (x ′ , w) * φ ′ (y ′′ , z ′′ , u ′′ ) if (a = 1 or p ∈ B) and (b = 1 or q ∈ B) B0,0(x, w) ⇐ ∃x ′ .x → (p, q, y, z, u, x ′ ) * B1,1(x ′ , w) * φ ′ (y, z, u) if p, q ∈ B B0,1(x, w) ⇐ ∃x ′ .x → (p, q, y, z ′ , u, x ′ ) * B1,2(x ′ , w) * φ ′ (y, z ′ , u) if p, q ∈ B B1,0(x, w) ⇐ ∃x ′ .x → (p, q, y ′ , z, u ′ , x ′ ) * B2,1(x ′ , w) * φ ′ (y ′ , z, u ′ ) if p, q ∈ B B1,1(x, w) ⇐ ∃x ′ .x → (p, q, y ′ , z ′ , u ′ , x ′ ) * B2,2(x ′ , w) * φ ′ (y ′ , z ′ , u ′ ) if p, q ∈ B B 0,b (x, w) ⇐ ∃x ′ , z ′′ .x → (p, q, y, z ′′ , u, x ′ ) * B 1,b (x ′ , w) * φ ′ (y, z ′′ , u) if p ∈ B and (b = 1 or q ∈ B) B 1,b (x, w) ⇐ ∃x ′ , z ′′ .x → (p, q, y ′ , z ′′ , u ′ , x ′ ) * B 2,b (x ′ , w) * φ ′ (y ′ , z ′′ , u ′ ) if p ∈ B and (b = 1 or q ∈ B) Ba,0(x, w) ⇐ ∃x ′ , y ′′ , u ′′ .x → (p, q, y ′′ , z, u ′′ , x ′ ) * Ba,1(x ′ , w) * φ ′ (y ′′ , z, u ′′ ) if q ∈ B and (a = 1 or p ∈ B) Ba,1(x, w) ⇐ ∃x ′ , y ′′ , u ′′ .x → (p, q, y ′′ , z ′ , u ′′ , x ′ ) * Ba,2(x ′ , w) * φ ′ (y ′′ , z ′ , u ′′ ) if q ∈ B and (a = 1 or p ∈ B) B a,b (x, w) ⇐ ∃y ′′ , z ′′ , u ′′ .x → (p, q, y ′′ , z ′′ , u ′′ , ⊥) * φ ′ (y ′′ , z ′′ , u ′′ ) if (a, b) ∈ {(2, 2), (2, 1), (1, 2)}
A straightforward induction permits to verify that if the considered structure does not satisfy the formula A(x, v) ∨ ∃y, z, y ′ , z ′ , u, u ′ .B(x, w) then necessarily k = k ′ and for all l ∈ {1, . . . , k}, we have (ℓ y I l , ℓ z J l ) ∈ S ∧ (ℓ u I l , ℓ z J l ) ∈ S. There remains to check that p Ii = q Ji for all i ∈ {1, . . . , k}. To this aim, we design an atom C(x, v) that will be satisfied by structures not validating this condition, assuming the condition ( †) above is fulfilled. This predicate allocates the location ℓ and introduces existential variables y, z, u denoting the faulty locations ℓ y Ii , ℓ z Ji and ℓ u Ii , i.e., the locations corresponding to the index i such that p Ii = q Ji . By ( †), these locations must be chosen in such a way that the constraints S(y, z) and S(y, z) are satisfied. The predicate C(x, v) also guesses pairs p, q such that p = q (denoting the distinct pairs p xi and q yi ) and invokes the predicate C (0,0) p,q to allocate all the remaining locations. As for the previous rules, the predicates C a,b p,q , for p, q ∈ B a, b ∈ {0, 1} allocate ℓ 1 , . . . , ℓ m ′ , where a (resp. b) denotes the number of variables in {y} (resp. {z}) that have already been allocated. In the rules below, we denote by u the vector v, y, z, u. In all the rules we have p ′ , q ′ ∈ P.

C(x, v) ⇐ ∃y, z, u. x → (⊥, ⊥, ⊥, ⊥, ⊥, x ′ ) * C 0,0 p,q (x ′ , u) * S(y, z) * S(u, z) if p = q and p, q ∈ B C a,b p,q (x, u) ⇐ ∃x ′ , y ′′ , z ′′ , u ′′ .x → (p ′ , q ′ , y ′′ , z ′′ , u ′′ , x ′ ) * C a,b p,q (x, u) * φ ′ (y ′′ , z ′′ , u ′′ ) C 0,0 p,q (x, u) ⇐ ∃x ′ .x → (p, q, y, z, u, x ′ ) * C 1,1 p,q (x, u) * φ ′ (y, z, u) C 0,b p,q (x, u) ⇐ ∃x ′ , z ′′ .x → (p, q ′ , y, z ′′ , u, x ′ ) * C 1,b p,q (x, u) * φ ′ (y, z ′′ , u) C a,0 p,q (x, u) ⇐ ∃x ′ , y ′′ , u ′′ .x → (p ′ , q, y ′′ , z, u ′′ , x ′ ) * C a,1 p,q (x, u) * φ ′ (y ′′ , z, u ′′ ) C 1,1 p,q (x, u) ⇐ ∃y ′′ , z ′′ , u ′′ .x → (p ′ , q ′ , y ′′ , z ′′ , u ′′ , ⊥) * φ ′ (y ′′ , z ′′ , u ′′ )
The PCP has a solution iff the sequent

W (x, v) ⊢ R A(x, v), ∃y, z, y ′ , z ′ , u, u ′ .B(x, w), C(x, u)
has a countermodel. Indeed, if a structure satisfying the atom W (x, v) but not the disjunction A(x, v) ∨ ∃y, z, y ′ , z ′ , u, u ′ .B(x, w) ∨ C(x, u) exists, then as explained above, there exists a word u i1 . . . . .u i k = v j1 . . . . .v j k ′ , with (i 1 , . . . , i k ) = (j 1 , . . . , j k ′ ). Conversely, if a solution of the PCP exists, then by using the locations α l , α ′ l , α ′′ l in the hypothesis of the lemma as ℓ y I l , ℓ z J l , ℓ u I l it is easy to construct a a structure satisfying W (x, v). Further, by hypothesis, since (α l , α ′ l ) ∈ S and (α ′′ l , α ′ l ) ∈ S, we have (ℓ y I l , ℓ z J l ) ∈ S and (ℓ u I l , ℓ z J l ) / ∈ S for all l = 1, . . . , k. Thus A(x, v) and ∃y, z, y ′ , z ′ , u, u ′ .B(x, w) do not hold. To fulfill ¬C(x, u) we have to ensure that, for all i, j ∈ {1, . . . , k}, we have (ℓ y Ii , ℓ z Jj ) ∈ S ∧ (ℓ u Ii , ℓ z Jj ) ∈ S =⇒ p Ii = q Ji . Since the considered word is a solution of the PCP, we have p Ii = q Ji for all i = 1, . . . , k, hence ¬C(x, u) is satisfied.

⊓ ⊔

Eliminating Equations and Disequations

In this section, we show that the equations and disequations can always be eliminated from established sequents (in exponential time), while preserving equivalence. The intuition is that the equations can be discarded by instantiating the inductive rules, while the disequations can be replaced by assertions that the considered variables are allocated in disjoint parts of the heap. We first introduce an additional restriction on pc-SIDs that is meant to ensure that the set of free variables allocated by a predicate atom is the same in every unfolding. The pc-SID satisfying this condition are called alloc-compatible. We will show that every pc-SID can be reduced to an equivalent alloc-compatible set. Let alloc be a function mapping each predicate symbol p to a subset of {1, . . . , #(p)}. For any disjunction-free formula φ, we denote by alloc(φ) the set of variables x ∈ fv (φ) such that φ contains an atom of the form x → (y 1 , . . . , y κ ) or p(z 1 , . . . , z n ), with x = z i for some i ∈ alloc(p).

Definition 10. An established pc-SID R is alloc-compatible if for all rules α ⇐ φ in R, we have alloc(α) = alloc(φ) . A sequent φ ⊢ R Γ is alloc-compatible if R is alloc-compatible.
Lemma 11. There exists an algorithm which, for every sequent φ ⊢ R Γ , computes an equivalent alloc-compatible sequent φ ′ ⊢ R ′ Γ ′ . Moreover, this algorithm runs in exponential time and width(φ

′ ⊢ R ′ Γ ′ ) = O(width(φ ⊢ R Γ ) 2 ).
Proof. We associate all pairs (p, A) where p ∈ P S and A ⊆ {1, . . . , #(p)} with fresh, pairwise distinct predicate symbols p A ∈ P S , with the same arity as p, and we set alloc(p A ) = A. For each disjunction-free formula φ, we denote by φ * the set of formulas obtained from φ by replacing every predicate atom p(x) by an atom p A (x) with A ⊆ {1, . . . , #(p)}. Let R ′ be the set of alloc-compatible rules of the form p A (x) ⇐ ψ, where p(x) ⇐ φ is a rule in R and ψ ∈ φ * . Note that the symbols p A may be encoded by words of length O( p + #(p)), thus for every ψ ∈ φ * we have width(ψ) = O(width(φ) 2 ), hence width(R ′ ) = O(width(R) 2 ). We show by induction on the satisfiability relation that the following equivalence holds for every structure (s, h): (s, h) |= R φ iff there exists ψ ∈ φ * such that (s, h) |= R ′ ψ. For the direct implication, we also prove that alloc(ψ

) = {x ∈ fv (φ) | s(x) ∈ dom(h)}.
-The proof is immediate if φ is a T -formula, since φ * = {φ}, and the truth value of φ does not depend on the considered pc-SID. Also, by definition alloc(φ) = ∅ and all the models of φ have empty heaps. -If φ is of the form x → (y 1 , . . . , y n ), then φ * = {φ} and the truth value of φ does not depend on the considered pc-SID. Also, alloc(φ) = {x} and we have dom(h) = {s(x)} for every model (s, h) of φ. -Assume that φ = p(x 1 , . . . , x #(p) ). If (s, h) |= R φ then there exists a formula γ such that φ ⇐ R γ and (s, h) |= R γ. By the induction hypothesis, there exists ψ ∈ γ * such that (s, h) |= R ′ ψ and alloc(ψ

) = {x ∈ fv (γ) | s(x) ∈ dom(h)}. Let A = {i ∈ {1, . . . , #(p)} | s(x i ) ∈ dom(h)}, so that alloc(ψ) = {x i | i ∈ A}. By construction p A (x 1 , . . . , x n ) ⇐ ψ is alloc-compatible, and therefore p A (x 1 , . . . , x n ) ⇐ R ′ ψ, which entails that (s, h) |= R ′ p A (x 1 , . . . , x n ). By definition of A, alloc(p A (x 1 , . . . , x n )) = {x ∈ fv (φ) | s(x) ∈ dom(h)}.
Conversely, assume that (s, h) |= R ψ for some ψ ∈ φ * . Necessarily ψ is of the form p A (x 1 , . . . , x n ) with A ⊆ {1, . . . , #(p)}. We have p A (x 1 , . . . , x n ) ⇐ R ′ ψ ′ and (s, h) |= R ψ ′ for some formula ψ ′ . By definition of R ′ , we deduce that p(x 1 , . . . , x n ) ⇐ R γ, for some γ such that ψ ∈ γ * . By the induction hypothesis, (s,

h) |= R γ, thus (s, h) |= R p(x 1 , . . . , x #(p) ). Since p(x 1 , . . . , x #(p) ) = φ, we have the result. -Assume that φ = φ 1 * φ 2 . If (s, h) |= R φ then there exist disjoint heaps h 1 , h 2 such that (s, h i ) |= R φ i , for all i = 1, 2 and h = h 1 ⊎ h 2 .
By the induction hypothesis, this entails that there exist formulas

ψ i ∈ φ * i for i = 1, 2 such that (s, h i ) |= R ′ ψ i and alloc(ψ i ) = {x ∈ fv (φ i ) | s(x) ∈ dom(h i )}. Let ψ = ψ 1 * ψ 2 . It is clear that (s, h) |= R ′ ψ 1 * ψ 2 and alloc(ψ) = alloc(ψ 1 * ψ 2 ) = alloc(ψ 1 ) ∪ alloc(ψ 2 ) = {x ∈ fv (φ 1 ) ∪ fv (φ 2 ) | s(x) ∈ dom(h)} = {x ∈ fv (φ) | s(x) ∈ dom(h)}. Since ψ 1 * ψ 2 ∈ φ * , we obtain the result. Conversely, assume that there exists ψ ∈ φ * such that (s, h) |= R ′ ψ. Then ψ = ψ 1 * ψ 2 with ψ i ∈ φ *
i , and we have (s,

h i ) |= R ′ ψ i , for i = 1, 2 with h = h 1 ⊎ h 2 .
Using the induction hypothesis, we get that (s,

h i ) |= R φ i , hence (s, h) |= R φ. -Assume that φ = ∃y.γ. If (s, h) |= R φ then (s ′ , h) |= R γ,
for some store s ′ coinciding with s on every variable distinct from y. By the induction hypothesis, this entails that there exists ψ ∈ γ * such that (s ′ , h) |= R ′ ψ and alloc(ψ) = {x ∈ fv (γ) | s ′ (x) ∈ dom(h)}. Then (s, h) |= R ′ ∃y.ψ, and we have ∃y.ψ ∈ φ * . Furthermore, alloc(∃y.ψ) = alloc(ψ)

\ {y} = {x ∈ fv (γ) \ {y} | s ′ (x) ∈ dom(h)} = {x ∈ fv (φ) | s(x) ∈ dom(h)}.
Conversely, assume that (s, h) |= R ψ, with ψ ∈ φ * . Then ψ is of the form ∃y.ψ ′ , with ψ ′ ∈ γ * , thus there exists a store s ′ , coinciding with s on all variables other than y such that (s ′ , h) |= R ψ ′ . By the induction hypothesis, this entails that (s ′ , h) |= R ψ, thus (s, h) |= R ∃y.γ. Since ∃y.γ = φ, we have the result. Let φ ′ , Γ ′ be the sequence of formulas obtained from φ, Γ by replacing every atom α by the disjunction of all the formulas in α * . It is clear that width(φ

′ ⊢ R ′ Γ ′ ) ≤ width(φ ⊢ R Γ ) 2 . By the previous result, φ ′ ⊢ R ′ Γ ′ is equivalent to φ ⊢ R Γ , hence φ ′ ⊢ R ′ Γ ′
fulfills all the required properties. Also, since each predicate p is associated with 2 #(p) predicates p A , it is clear that φ ′ ⊢ R ′ Γ ′ can be computed in time O(2 size(φ⊢RΓ ) ).

⊓ ⊔ Definition 12. Let P ⊆ P T . A formula φ is P -constrained if for every formula ψ such that φ ⇐ R ψ, and for every symbol p ∈ P T occurring in ψ, we have p ∈ P . A sequent φ ⊢ R Γ is P -constrained if all the formulas in φ, Γ are Pconstrained.

Theorem 13. Let P ⊆ P T . There exists an algorithm that transforms every P -constrained established sequent φ ⊢ R Γ into an equivalent (P \ {≈, ≈})constrained established sequent φ ′ ⊢ R ′ Γ ′ . This algorithm runs in exponential time and width(φ

′ ⊢ R ′ Γ ′ ) is polynomial w.r.t. width(φ ⊢ R Γ ).
Proof. We consider a P -constrained established sequent φ ⊢ R Γ . This sequent is transformed in several steps.

Step 1. The first step consists in transforming all the formulas in φ, Γ into disjunctions of symbolic heaps. Then for every symbolic heap γ occurring in the obtained sequent, we add all the variables freely occurring in φ or Γ as parameters of every predicate symbol occurring in unfoldings of γ (their arities are updated accordingly, and these variables are passed as parameters to each recursive call of a predicate symbol). We obtain an equivalent sequent φ 1 ⊢ R1 Γ 1 , and if v = card (fv (φ)∪fv (Γ )) denotes the total number of free variables occurring in φ, Γ , then it is easy to check (since the size of each of these variables is bounded by width

(φ ⊢ R Γ )) that width(φ 1 ⊢ R1 Γ 1 ) ≤ v • width(φ ⊢ R Γ ) 2 . By Definition 7, we have v ≤ width(φ ⊢ R Γ ), thus width(φ 1 ⊢ R1 Γ 1 ) = O(width(φ ⊢ R Γ ) 3 ).
Step 2. All the equations involving an existential variable can be eliminated in a straightforward way by replacing each formula of the form ∃x.(x ≈ y * φ) with φ{x ← y}. We then replace every formula ∃y.φ with free variables x 1 , . . . , x n by the disjunction of all the formulas of the form ∃z.φσ * * z∈z,z ′ ∈z∪{x1,...,xn},z =z ′ z ≈ z ′ , where σ is a substitution such that dom(σ) ⊆ y, z = y\dom(σ) and img(σ) ⊆ y ∪{x 1 , . . . , x n }. Similarly we replace every rule p(x 1 , . . . , x n ) ⇐ ∃y.φ by the the set of rules p(x 1 , . . . , x n ) ⇐ ∃z.φσ * * z∈z,z ′ ∈z∪{x1,...,xn},z =z ′ z ≈ z ′ , where σ is any substitution satisfying the conditions above. Intuitively, this transformation ensures that all existential variables are associated to pairwise distinct locations, also distinct from any location associated to a free variable. The application of the substitution σ captures all the rule instances for which this condition does not hold, by mapping all variables that are associated with the same location to a unique representative. We denote by φ 2 ⊢ R2 Γ 2 the sequent thus obtained. Let v ′ be the maximal number of existential variables occurring in a rule in R. We have v ′ ≤ width(φ ⊢ R Γ ) (since the transformation in Step 1 adds no existential variable). Since at most one disequation is added for every pair of variables, and since the size of every variable is bounded by width(φ

⊢ R Γ ), it is clear that width(φ 2 ⊢ R2 Γ 2 ) = width(φ 1 ⊢ R1 Γ 1 ) + v ′ • (v + v ′ ) • (1 + 2 * width(φ ⊢ R Γ )) = O(width(φ ⊢ R Γ ) 3 ).
Step 3. We replace every atom α = p(x 1 , .

3 ⊢ R3 Γ 3 is equivalent to φ ⊢ R Γ .
By a straightforward induction on the derivation, we can show that all atoms occurring in an unfolding of the formulas in the sequent φ 3 ⊢ R3 Γ 3 are of the form q(y 1 , . . . , y #(q) ), where y 1 , . . . , y #(q) are pairwise distinct, and that the considered unfolding also contains the disequation y i ≈ y j , for all i = j such that either y i or y j is an existential variable (note that if y i and y j are both free then y i ≈ y j is valid, since the considered stores are injective). This entails that the rules that introduce a trivial equality u ≈ v with u = v are actually redundant, since unfolding any atom q(y 1 , . . . , y #(q) ) using such a rule yields a formula that is unsatisfiable. Consequently such rules can be eliminated without affecting the status of the sequent. All the remaining equations are of form u ≈ u hence can be replaced by emp. We may thus assume that the sequent φ 3 ⊢ R3 Γ 3 contains no equality. Note that by the above transformation all existential variables must be interpreted as pairwise distinct locations in any interpretation, and also be distinct from all free variables. It is easy to see that the fresh predicates p α may be encoded by words of size at most width

(φ ⊢ R Γ ), thus width(φ 3 ⊢ R3 Γ 3 ) ≤ width(φ ⊢ R Γ ) • width(φ 2 ⊢ R2 Γ 2 ) = O(width(φ ⊢ R Γ ) 4 )
. By Lemma 11, we may assume that φ 3 ⊢ R3 Γ 3 is alloc-compatible (note that the transformation given in the proof of Lemma 11 does not affect the disequations occurring in the rules).

Step 4. We now ensure that all the locations that are referred to are allocated. Consider a symbolic heap γ occurring in φ 3 , Γ 3 and any R 3 -model (s, h) of γ, where s is injective. For the establishment condition to hold, the only unallocated locations in h of γ must correspond to locations s(x) where x is a free variable. We assume the sequent contains a free variable u such that, for ev-ery tuple (ℓ 0 , . . . , ℓ κ ) ∈ h, we have s(u) = ℓ κ . This does not entail any loss of generality, since we can always add a fresh variable u to the considered problem: after Step 1, u is passed as a parameter to all predicate symbols, and we may replace every points-to atom z 0 → (z 1 , . . . , z κ ) occurring in φ 3 , Γ 3 or R 3 , by z 0 → (z 1 , . . . , z κ , u) (note that this increases the value of κ by 1). It is clear that this ensures that h and u satisfy the above property. We also assume, w.l.o.g., that the sequent contains at least one variable u ′ distinct from u. Note that, since s is injective, the tuple (s(u ′ ), . . . , s(u ′ )) cannot occur in h, because its last component is distinct from s(u). We then denote by φ 4 ⊢ R4 Γ 4 the sequent obtained from φ 3 ⊢ R3 Γ 3 by replacing every symbolic heap γ in

φ 3 , Γ 3 by * x∈(fv(φ3)∪fv (Γ3))\alloc(γ) x → (u ′ , . . . , u ′ ) * γ It is straightforward to check that (s, h) |= γ iff there exists an extension h ′ of h such that (s, h ′ ) |= * x∈(fv (φ3)∪fv (Γ3))\alloc(γ) x → (u ′ , . . . , u ′ ) * γ, with loc(h) = loc(h ′ ) = dom(h ′ ) and h ′ (ℓ) = (s(u ′ . . . , s(u ′ )) for all ℓ ∈ dom(h ′ ) \ dom(h). This entails that φ 4 ⊢ R4 Γ 4 is valid if and only if φ ⊢ R Γ is valid.
Consider a formula γ in φ 4 , Γ 4 and some unfolding γ ′ of γ. Thanks to the transformation in this step and the establishment condition, if γ ′ contains a (free or existential) variable x then it also contains an atom x ′ → y and a separating conjunction of equations χ such that χ |= T x ≈ x ′ . Since all equations have been removed, χ = emp, thus x = x ′ . Consequently, if γ ′ contains a disequation x 1 ≈ x 2 with x 1 = x 2 , then it also contains atoms x 1 → y 1 and x 2 → y 2 . This entails that the disequation x 1 ≈ x 2 is redundant, since it is a logical consequence of x 1 → y 1 * x 2 → y 2 . We deduce that the satisfiability status of φ 4 ⊢ R4 Γ 4 is preserved if all disequations are replaced by emp.

⊓ ⊔ Example 14. We illustrate all of the steps in the proof above.

Step 1. Consider the sequent p(x 1 , x 2 ) ⊢ R r(x 1 ) * r(x 2 ), where R is defined as follows: R = {r(x) ⇐ x → (x)}. After Step 1 we obtain the sequent p(x 1 , x 2 ) ⊢ R1 r ′ (x 1 , x 2 ) * r ′ (x 2 , x 1 ), where R 1 = {r ′ (x, y) ⇐ x → (x)}.

Step 2. This step transforms the formula ∃y 1 ∃y 2 . p(x, y 1 ) * p(x, y 2 ) into the disjunction:

∃y 1 , y 2 . p(x, y 1 ) * p(x, y 2 ) * y 1 ≈ y 2 * y 1 ≈ x * y 2 ≈ x ∨ ∃y 2 . p(x, x) * p(x, y 2 ) * y 2 ≈ x ∨ ∃y 1 . p(x, y 1 ) * p(x, x) * y 1 ≈ x ∨ p(x, x) * p(x, x)

Similarly, the rule p(x) ← ∃z∃u. x → (z) * q(z, u) is transformed into the set: p(x) ← x → (x) * q(x, x) p(x) ← ∃z. x → (z) * q(z, x) * z ≈ x p(x) ← ∃u. x → (x) * q(x, u) * u ≈ x p(x) ← ∃z∃u. x → (z) * q(z, u) * z ≈ x * u ≈ x * z ≈ u

Step 3. Assume that R contains the rules p(y 1 , y 2 , y 3 ) ⇐ y 1 → (y 2 ) * q(y 2 , y 3 ) * y 1 ≈ y 3 and p(y 1 , y 2 , y 3 ) ⇐ y 1 → (y 2 ) * r(y 2 , y 3 ) * y 1 ≈ y 2 and consider the sequent p(x, y, x) ⊢ R emp.

Step 3 generates the sequent p α (x, y) ⊢ R ′ emp (with α = p(x, y, x)) where R ′ contains the rules p α (y 1 , y 2 ) ⇐ y 1 → (y 2 ) * q(y 2 , y 1 ) * y 1 ≈ y 1 and p α (y 1 , y 2 ) ⇐ y 1 → (y 2 ) * r(y 2 , y 1 ) * y 1 ≈ y 2 . The second rule is redundant, because p α (y 1 , y 2 ) is used only in a context where y 1 ≈ y 2 holds. Step 4. Let γ = p(x, y, z, z ′ ) * q(x, y, z, z ′ ) * z ′ → (z ′ ), assume alloc(γ) = {x, z}, and consider the sequent γ ⊢ R emp. Then γ is replaced by p(x, y, z, z ′ , u) * q(x, y, z, z ′ , u) * z ′ → (z ′ , u) * u → (x, x) * y → (x, x) (all non-allocated variables are associated with (x, x), where x plays the rôle of the variable u ′ in Step above). Also, every points-to atom z 0 → (z 1 ) in R is replaced by z 0 → (z 1 , u).

Discussion

The presented undecidability result is very tight. Theorem 9 applies to most theories and the proof only uses very simple data structures (namely simply linked lists). The proof of Theorem 9 could be adapted (at the cost of cluttering the presentation) to handle quantifier-free entailments and even simpler inductive systems with at most one predicate atom on the right-hand side of each rule, in the spirit of word automata.

Our logic has only one sort of variables, denoting locations, thus one cannot directly describe structures in which the heap maps locations to tuples containing both locations and data, ranging over disjoint domains. This is actually not restrictive: indeed, data can be easily encoded in our framework by considering a non-injective function d(x) mapping locations to data, and adding theory predicates constructed on this function, such as d(x) ≈ d(y) to state that two (possibly distinct) locations x, y are mapped to the same element. The obtained theory falls within the scope of Theorem 9 (using d(x) ≈ d(y) as the relation S(x, y)), provided the domain of the data is infinite. This shows that entailments with data disjoint from locations are undecidable, even if the theory only contains equations and disequations, except when the data domain is finite.

  . . , x n ) occurring in φ 2 , Γ 2 or R 2 with pairwise distinct variables x i1 , . . . , x im (with m ≤ n and i 1 = 1), by an atom p α (x i1 , . . . , x im ), where p α is a fresh predicate symbol, associated with rules of the form p α (y i1 , . . . , y im ) ⇐ ψ{y i ← x i | i ∈ {1, . . . , n}}θ, where p(y 1 , . . . , y

n ) ⇐ ψ is a rule in R and θ denotes the substitution {x i k ← y i k | i ∈ {1, . . . , m}}. By construction, p α (x i1 , . . . , x im ) is equivalent to α. We denote by φ 3 ⊢ R3 Γ 3 the resulting sequent. It is clear that φ

Each symbol s in PS ∪ PT ∪ V is counted with a weight equal to its length s , and all the logical symbols have weight 1.

Hence two non-valid sequents with different countermodels are equivalent.

Acknowledgments. This work has been partially funded by the the French National Research Agency (ANR-21-CE48-0011). The authors wish to thank Radu Iosif for his comments on an earlier version of the paper and for fruitful discussions.