Yiqiang Chen

Stefan Duffner

Andrei Stoian

Jean-Yves Dufour

Atilla Baskurt

List-wise Learning-to-rank with Convolutional Neural Networks for Person Re-identification

Keywords: similarity metric learning, learning-to-rank, person re-identification, Deep Learning, image retrieval

In this paper, we present a novel machine learning-based image ranking approach using Convolutional Neural Networks (CNN). Our proposed method relies on a similarity metric learning algorithm operating on lists of image examples and a loss function taking into account the ranking in these lists with respect to different query images. This comprises two major contributions: (1) Rank lists instead of image pairs or triplets are used for training, thus integrating more explicitly the order of similarity and relations between sets of images. (2) A weighting is introduced in the loss function based on two evaluation measures: the mean average precision and the rank 1 score. We evaluated our approach on two different computer vision applications that are commonly formulated as ranking problems: person re-identification and image retrieval with several public benchmarks and showed that our new loss function outperforms other common functions and that our method achieves state-of-the-art performance compared to existing approaches from the literature.

Introduction

In many applications related to image and video indexation, video surveillance, recommendation systems or mobile robotics, we face the problem of retrieving similar images from a large dataset with known identities or categories. Due to the complexity and variability of the input data, different types of noise and the difficulty to capture the inherent similarities with simple metrics or rules leads to approaches that aim at directly learning this similarity metric from annotated image examples. This allows to construct complex, non-linear metrics that encode relations on a higher semantic level and that are robust to the various types of noise that are commonly present in realistic image data. In this work, we focus on the challenging problem of person re-identification from images that have been captured by different surveillance cameras with non-overlapping fields of view. In this setting, face recognition and other fine biometric cues are not always available due to the low image resolution. Therefore, the appearance of the whole person (e.g. clothing, hair style or other physical traits) is mainly exploited for this task. Moreover, person re-identification is necessary for many critical applications such as cross-camera tracking [START_REF] Beyer | Towards a principled integration of multicamera re-identification and tracking through optimal bayes filters[END_REF], multi-camera behaviour analysis [START_REF] Chaaraoui | A vision-based system for intelligent monitoring: Human behaviour analysis and privacy by context[END_REF] and forensic search [START_REF] Vezzani | People reidentification in surveillance and forensics: A survey[END_REF].

However, this problem remains challenging due to the large variations of viewpoint and background. The images from the same individual can have very different appearance, and, different individuals may look similar in appearance. It can be difficult even for humans given the severe lighting and pose differences between images.

To tackle these problems, existing person re-identification approaches generally either build a discriminative feature representation [START_REF] Farenzena | Person re-identification by symmetry-driven accumulation of local features[END_REF][START_REF] Ma | Local descriptors encoded by fisher vectors for person reidentification[END_REF][START_REF] Mignon | Pcca: A new approach for distance learning from sparse pairwise constraints[END_REF][START_REF] Li | Locally aligned feature transforms across views[END_REF][START_REF] Zhao | Person re-identification by salience matching[END_REF] or learn a distance metric [START_REF] Koestinger | Large scale metric learning from equivalence constraints[END_REF][START_REF] Pedagadi | Local fisher discriminant analysis for pedestrian re-identification[END_REF][START_REF] Xiong | Person re-identification using kernel-based metric learning methods[END_REF][START_REF] Liao | Person re-identification by local maximal occurrence representation and metric learning[END_REF]. The extracted features should be robust to challenging factors like pose variation while preserving the identity information. Metric learning approaches try to learn the semantic similarities (and dissimilarities) between images from the same and from different persons. They either learn a distance metric or a projection of the features into a subspace, where intra-class distances are minimised and inter-class distances are maximised.

Many recent person re-identification approaches are based on Convolutional Neural Networks (CNN). The advantage of these models is that they learn feature representations and a distance metric jointly in an integrated framework. To train these neural networks, different loss functions have been proposed such as contrastive loss, triplet loss or quadruplet loss. However, minimising such loss functions based on pairs, triplets or quadruplets only take into account constraints between few (two to four) examples and do not incorporate any information about a more global ranking or order of the instances. Also, the exact ranking order is usually not known or only partially defined. For example, a good match must be before an incorrect one, but there is not necessarily an order among good matches. To address these issues, in this work, we propose a novel list-wise loss function which we call the Rank-Triplet loss. It is based on the predicted and ground truth ranking of a list of instances with respect to a query image. To incorporate partial order constraints, our approach specifically focuses on mis-ranked instances.

Furthermore, existing deep learning methods are solely based on the minimisation of a loss function defined on a certain similarity metric between different examples. However, the final evaluation measures are computed on the overall ranking accuracy. Inspired by the learning-to-rank method LambdaRank [START_REF] Burges | Learning to rank with nonsmooth cost functions[END_REF], our optimisation approach directly incorporates these evaluation measures in the loss function. During training, each image in the training batch is used as probe image in turn and the rest as gallery. For each query, the mean average precision and rank 1 score are calculated. Triplets are formed by the probe image and a pair of mis-ranked true and false correspondence.

The loss of one triplet is weighted by the improvement of these evaluation measures by swapping the rank positions of the true and false correspondences, as shown in Fig. 1. This evaluation measure-based weighting makes better use of difficult triplets which can bring a larger rank improvement and are more effective for the learning, and, at the same time, keep the learning stable by using all misranked pairs. Only using the hardest examples can, in practice, lead to bad local minima early during training.

The main contributions of this paper can be summarised as follows:

-A novel list-wise loss function and training strategy for neural networks that combine the triplet loss and LambdaRank, where, in each training iteration, triplets are formed effectively according to the rankings in the given list. -A new weighting term in the loss function, based on the combination of two ranking measures: the mean average precision and the rank 1 score. This new loss function considers image retrieval and re-identification problems in a conceptually more natural way than previous work by directly taking into account the ranking evaluation scores. -A thorough experimental evaluation showing that the proposed loss function outperforms other common functions and that our approach achieves state-ofthe-art results on three challenging person re-identification datasets as well as an image retrieval dataset.

The rest of the paper is organised as follows. Section 2 introduces related work in the literature. In Section 3, we explain the proposed method in detail, and, in Section 4, we present the results of an extensive experimental evaluation of our approach and a comparison with state-of-the-art algorithms. Finally, conclusions are drawn in Section 5.

Related work

Learning-to-rank

Learning-to-rank is a class of techniques that learns a model for optimal ordering of a list of items. It is widely applied in information retrieval and natural language processing. Many learning-to-rank methods of different categories have been proposed in the literature.

The pairwise learning-to-rank approaches try to compare the relevance of every two documents, then rank all the documents based on all these comparison results. For example, RankSVM [START_REF] Herbrich | Large margin rank boundaries for ordinal regression[END_REF] seek to learn a ranking function in a higher dimensional feature space where true matches and wrong matches become more separable than the original feature space via the kernel trick. Prosser et al . [START_REF] Prosser | Person re-identification by support vector ranking[END_REF] reformulated the person re-identification problem as a ranking problem. Their method learns a set of weak RankSVMs, each computed on a small set of data, and then combines them to build a stronger ranker using ensemble learning. And Ranknet [START_REF] Burges | Learning to rank using gradient descent[END_REF] is the first neural network based learning-to-rank method. Query dependent features are extracted as the inputs of the network. To learn the model, the cross entropy cost function is minimised. It penalises the deviation of the model output probabilities from the desired probabilities: let P ij = {-1, 1} be the known probability that training x i should be ranked higher than training x j . Then the loss function is

L ranknet = -P ij logP ij -(1 -P ij )log(1 -P ij ) . (1)
The list-wise learning-to-rank approaches tries to directly compare the relevance of list of documents, instead of trying to get one ranking score for each document as pointwise methods do. It is motivated by the fact that the objective of pairwise learning is formalised as minimising errors in ranking document pairs, rather than minimising errors in ranking the document list. For example, Lamb-daRank [START_REF] Burges | Learning to rank with nonsmooth cost functions[END_REF] is the improved and list-wise version of RankNet. ListNet [START_REF] Cao | Learning to rank: from pairwise approach to listwise approach[END_REF] defined loss function as cross entropy between predicted and ground truth parameterised probability distributions of permutations. ListMLE [START_REF] Xia | Listwise approach to learning to rank: theory and algorithm[END_REF] maps a list of similarity scores to a probability distribution, then utilises the negative log likelihood of ground truth permutations as the loss function. Later, Wang et al . [START_REF] Wang | Deeplist: Learning deep features with adaptive listwise constraint for person reidentification[END_REF] applied the ListMLE method to the person re-identification problem.

Person re-identification

Classical person re-identification approaches focus on two key points: developing a powerful feature for image representation and learning an effective metric that represents semantic similarities and dissimilarities between same and different persons.The features used for re-identification are mainly variants of colour histograms [START_REF] Li | Locally aligned feature transforms across views[END_REF][START_REF] Zhao | Person re-identification by salience matching[END_REF], Local Binary Patterns (LBP) [START_REF] Li | Locally aligned feature transforms across views[END_REF][START_REF] Zhao | Person re-identification by salience matching[END_REF] or Gabor features [START_REF] Li | Locally aligned feature transforms across views[END_REF]. For example, Farenzena et al . [START_REF] Farenzena | Person re-identification by symmetry-driven accumulation of local features[END_REF] partitioned the human body into meaningful parts exploiting the asymmetry and symmetry in images. On each part, the weighted colour histogram, the maximally stable colour regions and the recurrent highstructured patches are computed. Ma et al . [START_REF] Ma | Local descriptors encoded by fisher vectors for person reidentification[END_REF] used local descriptors based on colour and gradient information and encode them using high-dimensional Fisher vectors. Mignon et al . [START_REF] Mignon | Pcca: A new approach for distance learning from sparse pairwise constraints[END_REF] used a feature vector composed of a mixture of colour (RGB, HSV and YCbCr) and texture (LBP) from six horizontal stripe regions. Liao et al . [START_REF] Liao | Person re-identification by local maximal occurrence representation and metric learning[END_REF] analyse the horizontal occurrence of local features and maximise this occurrence to improve the robustness of features. The main metric learning methods include Mahalanobis-like metrics like KISSME [START_REF] Koestinger | Large scale metric learning from equivalence constraints[END_REF], Local Fisher discriminant Analysis (LFDA) [START_REF] Pedagadi | Local fisher discriminant analysis for pedestrian re-identification[END_REF], Marginal Fisher Analysis(MFA) [START_REF] Xiong | Person re-identification using kernel-based metric learning methods[END_REF] and Cross-view Quadratic Discriminant Analysis (XQDA) [START_REF] Liao | Person re-identification by local maximal occurrence representation and metric learning[END_REF].

Recently, deep learning approaches have achieved state-of-the-art results for person re-identification. Deep learning approaches for person re-identification learn visual feature representations and a similarity metric jointly. Recently, these approaches try to leverage geometric and semantic knowledge that helps the model to focus on specific images regions (e.g. head, torso, legs, feet) by means of semantic segmentation [START_REF] Kalayeh | Human semantic parsing for person re-identification[END_REF][START_REF] Tian | Eliminating background bias for robust person re-identification[END_REF] or other attention mechanisms [START_REF] Song | Mask-guided contrastive attention model for person re-identification[END_REF][START_REF] Li | Harmonious attention network for person re-identification[END_REF][START_REF] Xu | Attention-aware compositional network for person re-identification[END_REF][START_REF] Si | Dual attention matching network for context-aware feature sequence based person re-identification[END_REF]. Other approaches improve on the re-identification performance by generating additional artificial training samples (e.g. by Generative Adversarial Networks) [START_REF] Huang | Multi-pseudo regularized label for generated samples in person re-identification[END_REF][START_REF] Zheng | Joint discriminative and generative learning for person reidentification[END_REF] and effectively combining them with the real images. Also, some works propose neural architectures and training strategies combining the semi-supervised training with some sort of additional supervision (e.g. from person identities or other factors) [START_REF] Zheng | A discriminatively learned CNN embedding for person reidentification[END_REF][START_REF] Chang | Multi-level factorisation net for person reidentification[END_REF].A These recently proposed improvements are mostly independent and could eventually be combined with our similarity metric learning approach.

Here we mainly review the related deep learning methods that learn a nonlinear projection into a feature space in which the similarity of pedestrian is well represented. In this regard, several loss functions are proposed or applied in person re-identification. Yi et al . [START_REF] Yi | Deep metric learning for person re-identification[END_REF] first proposed to use a Siamese network to person reidentification. And Ahmed et al . [START_REF] Ahmed | An improved deep learning architecture for person reidentification[END_REF] and Li et al . [START_REF] Li | Deepreid:deep filter pairing neural network for person re-identification[END_REF] consider the re-identification task as an image pair classification problem deciding whether an image pair is from the same person or not. One disadvantage of pairwise approaches is the data imbalance since there are much more possible negative pairs than positive pairs in the training set. This may lead to over-fitting when using a pairwise loss function. A class weighting can be applied to solve the problem, but it adds a free parameter that may be different for different datasets. Some approaches use the triplet loss or its variants. The triplet loss forces the similarity between positive matching pairs to be larger than that of negative matching pairs. Ding et al . [START_REF] Ding | Deep feature learning with relative distance comparison for person re-identification[END_REF] first applied the triplet loss to train a CNN for person re-identification. Cheng et al . [START_REF] Cheng | Person re-identification by multichannel parts-based cnn with improved triplet loss function[END_REF] proposed an improved variant of the triplet loss function by combining the contrastive loss and a CNN network processing parts and the entire body. Chen et al . [START_REF] Chen | Beyond triplet loss: a deep quadruplet network for person re-identification[END_REF] applied a quadruplet loss which samples four images from three identities and minimises the difference between a positive pair from one identity and a negative pair from two different identities and they combine this quadruplet loss with the triplet loss.

Using triplets reduces the imbalance problem in Siamese networks, but another drawback of both Siamese and triplet loss learning is that the trivial pairs or triplets become inactive at a later training stage. To tackle this problem, some methods exploit hard example mining to enhance convergence and overall performance. Ahmed et al . [START_REF] Ahmed | An improved deep learning architecture for person reidentification[END_REF], for example, used the difference of feature maps to measure the similarity and performed hard negative example pair mining. Shi et al . [START_REF] Shi | Embedding deep metric for person re-identification: A study against large variations[END_REF] proposed to perform moderate positive and negative example mining to ensure a stable training process and avoid perturbing the manifold learning by using hard examples. On the contrary, Hermans et al . [START_REF] Hermans | In defense of the triplet loss for person re-identification[END_REF] proposed to use the hardest positive and negative examples in each training batch to perform an effective triplet learning. Our approach is inspired by these strategies by selecting mis-ranked examples from the global ordered retrieval results. But instead of simply focusing or retraining on these errors, we principally incorporate the ranking score gain or loss in the global minimisation framework.

Proposed Method

In the following, we will first outline the basic learning-to-rank method Lamb-daRank and its limitations in our context. Then, we will present the ranking evaluation measures that we integrate into the training algorithm. And finally, we will describe the proposed training algorithm based on our Rank-Triplet loss and list-wise ranking. An overview of our approach is shown in Fig. 2.

Learning-to-rank with LambdaRank

RankNet [START_REF] Burges | Learning to rank using gradient descent[END_REF] uses a neural network model that is trained using the cross entropy cost. Thus, it is minimising the number of pairwise errors and does not consider other information retrieval measures. To directly optimise these measures is difficult as they are not differentiable, thus leading to a non-convex problem that cannot be solved with gradient descent-based algorithms commonly used for neural network models. To tackle this problem, Burges et al . [START_REF] Burges | Learning to rank with nonsmooth cost functions[END_REF] proposed LambdaRank which, at each training iteration, simply scales the gradient of the loss function by the difference of the document retrieval evaluation measure Normalised Discounted Cumulative Gain (NDCG) incurred by swapping the rank positions of two items, as shown in Eq. 2. The authors showed that this approach improves the overall ranking performance.

λ = ∂L ranknet s ij • ∆N DCG . (2)
The triplet learning has shown good performance on verification problems like image classification [START_REF] Wang | Learning fine-grained image similarity with deep ranking[END_REF], face recognition [START_REF] Schroff | Facenet: A unified embedding for face recognition and clustering[END_REF] and person re-identification [START_REF] Ding | Deep feature learning with relative distance comparison for person re-identification[END_REF][START_REF] Cheng | Person re-identification by multichannel parts-based cnn with improved triplet loss function[END_REF][START_REF] Hermans | In defense of the triplet loss for person re-identification[END_REF]. However, in triplet learning for person re-identification, we face a similar problem to RankNet. The classical triplet loss is defined on the partial order relations among identities, However, the final ranking performance is calculated on the global order. That means that the triplet loss iteratively enforces pairwise order relationships w.r.t. reference examples. It ignores the fact that ranking is a prediction task on list of objects. So it is difficult to generalise this approach for optimising the global order. In this regard, a list-wise ranking is a better approximation of this global order relation, and we adapted it to the person re-identification problem, as explained in Section 3.3.

Person re-identification evaluation measure

Cumulated Matching Characteristics (CMC) and mean average precision (mAP) are widely used performance measures for person re-identification. CMC evaluates the top n nearest images in the gallery set w.r.t. one probe image. If a correct match of a query image is at the k th position (k n), then this query is considered a success of rank n. In most cases, we look at the success of rank 1 (R1), i.e. the person has been correctly re-identified. The CMC curve shows the probability that a query identity appears in different-sized ordered candidate lists. As for mAP, for each query, we calculate the area under the Precision-Recall curve, which is known as average precision (AP):

AP = 1 0 P (R) dR , (3)
where P (R) is the precision for a given recall R. Then, the mean value of AP of all queries, i.e. mAP = 1 n i=1 n AP i , where n is the number of queries, which considers both precision and recall of an algorithm, thus providing a more suitable evaluation for the setting in which there are several true correspondences in gallery set.

Since P (•) and R(•) are discrete functions, the area under the precision-recall curve is approximated as [START_REF] Zheng | Scalable person reidentification: A benchmark[END_REF]:

AP = N k=1 p(k) + p(k -1) 2 [r(k) -r(k -1)] , (4)
where k is the rank in the sequence of retrieved items. p(k) and r(k) are respectively the precision and recall at the rank k position. We define also p(0) = 1 and r(0) = 0. N is the number of images in the gallery set. Since in our method the AP is calculated at each iteration during training, we propose to simplify this computation. In ranking problems, recall is the fraction of the items that are relevant to the query that are successfully retrieved, the variation r(k)-r(k -1) is different from zero only when a relevant item is retrieved through the sequence of retrieved items. We only need to take into account the true correspondence ranking position and the variation of recall equals always 1 M , where M is the number of the true correspondences of a query. Thus AP can be calculated as:

AP = 1 2M [1 + p(π 1 ) + M i=2 p(π i ) + p(π i-1 ))] , (5)
where π i is the rank index of the i th true correspondence. Precision is defined as the proportion of retrieved non-relevant items out of all non-relevant items available. Thus the precision at ranking position π i is: p(π i ) = i π i . We can further simplify the equation to:

AP = 1 M M i=1 [ i π i ] - 1 2π M + 1 2M . (6)

Rank-Triplet loss

The triplet loss uses triplets of examples to train the network with an anchor image a, a positive image p from the same person as a and a negative image n from a different person. Training imposes that the projection of the positive example is placed closer to the anchor than the projection of the negative example. This constraint is defined as:

f (a i ) -f (p i ) 2 2 < f (a i ) -f (n i ) 2 2 . ( 7
)
The weights of the network for the three input images are shared, and to train the network, the constraint of Eq. 7 is formulated as the minimisation of the following triplet loss function is minimised:

E triplet = - 1 N N i=1 [max( f (a i ) -f (p i ) 2 2 -f (a i ) -f (n i ) 2 2 +m, 0)] , (8)
where N is the number of triplets, f is the projection of the network, and m is a margin. With the triplet loss function, the network learns a semantic distance metric by "pushing" the negative image pairs apart and "pulling" the positive images closer in the feature space.

In order to update the weights of the network, it is crucial to select triplets that violate the triplet constraint in Eq. 7. However, in practice, the majority of the triplets does not violate the constraint at a later learning stage. Hard triplet mining is an effective way to tackle this problem, but some too hard triplets may distort the manifold [START_REF] Burges | Learning to rank using gradient descent[END_REF]. We propose to select the triplets according to the ranking order, i.e. only mis-ranked matches will be selected. Given a query and a ranking, an example is declared mis-ranked if a wrong match is ranked before it (i.e. considered more similar to the query). Not only using the hardest examples stabilises the training, and weighting the triplets according to their contribution makes the learning more effective.

The overall training procedure is presented in Algorithm 1. In order to optimise directly the AP and R1 scores, we estimate the gain for AP and R1 of the triplets from the ranking within a training batch. A training batch is formed by M images of N identities. For each example in the batch, we preform a ranking among the rest of images in the batch. For the sake of a robust metric, we add a margin m to the distance of ranking positions between the true correspondences and the probe before ranking. The AP and R1 scores are computed for each query ranking. Then, with respect to one probe, we form all possible mis-ranked pairs (false correspondences ranked before the true correspondence), and we re-calculate the new AP and R1 scores by swapping positions of the pair in the ranking and thus obtain the gains ∆AP and ∆R1, respectively. The loss of each triplet is weighted by the sum of these gains. The final Rank-Triplet loss is calculated as follows:

E Rank-T riplet = 1 M N M N i=1 1 K i j∈T C i k∈F C i r i k <r i j [ f (x i ) -f (x j ) 2 2 -f (x i ) -f (x k ) 2 2 +m] • (∆AP i jk + ∆R1 i jk ), (9)
where x i is the i th training example in a training batch, K i is the number of misranked pairs w.r.t. the i th example as query, and r i j is the rank of the j th example w.r.t. the i th image as query. T C i /F C i is the true/false correspondence set of the i th example. ∆AP i jk is the gain of AP by swapping the j th and k th examples w.r.t. the i th example as query and analogously for R1.

With our evaluation based weighting, we make a trade-off between the moderate hard examples and hardest examples, i.e. more weight is given to the hardest examples to make the learning efficient, and, at the same time, the less hard example are used to stabilise the training.

Experiments and results

In this section, we report the experiment results carried out on the person reidentification datasets Market-1501 [START_REF] Zheng | Scalable person reidentification: A benchmark[END_REF], DukeMTMC-Reid [START_REF] Zheng | Unlabeled samples generated by gan improve the person re-identification baseline in vitro[END_REF] and CUHK03 [START_REF] Li | Deepreid:deep filter pairing neural network for person re-identification[END_REF] to compare our approach with the state-of-the-art approaches. We also perform a comparison with other loss functions commonly used in the literature. We further perform a more detailed analysis of the proposed method in several aspects, like its convergence behaviour and training time. Finally, to show the genericity of our approach, we applied it to an image retrieval task. We performed experimental evaluations on the Holidays dataset and compared it to the state-of-the-art methods and results.

Person re-identification

Datasets

The Market-1501 dataset [START_REF] Zheng | Scalable person reidentification: A benchmark[END_REF] is one of the largest publicly available datasets 130 for human re-identification with 32,668 annotated bounding boxes of 1501 subjects. All images are resized to 128×48. The dataset is split into 751 identities for training and 750 identities for testing as in [START_REF] Zheng | Scalable person reidentification: A benchmark[END_REF].

The DukeMTMC-Reid dataset [START_REF] Zheng | Unlabeled samples generated by gan improve the person re-identification baseline in vitro[END_REF] is collected with 8 cameras and used for cross-camera tracking. It contains 36,411 total bounding boxes from 1,404 identities. Half is used for training and the rest for testing. In total, it has 36,411 total bounding boxes including 16,522 training images, 2,228 queries, and 17,661 gallery images.

The CUHK03 dataset [START_REF] Li | Deepreid:deep filter pairing neural network for person re-identification[END_REF] is a challenging dataset collected in the CUHK campus with 13,164 images of 1,360 identities from two camera views. Each identity is captured by two disjoint camera views and has an average of 4.8 images 140 in each view. There are two settings: labelled with human-annotated bounding boxes and the more challenging detected with automatically generated bounding boxes. Our experiments will be conducted on the detected version of CUHK03 which is a more realistic scenario. We followed the new test protocol proposed in [START_REF] Zhong | Re-ranking person re-identification with k-reciprocal encoding[END_REF] which splits the CUHK03 dataset into training set and testing set similar to that of Market-1501, which consist of 767 identities and 700 identities respectively. Some examples images of the datasets are shown in Fig 3 . All the three datasets follow the same test protocol. The authors randomly select one image from each camera as the query for each identity and use the rest of images to construct the gallery set. In evaluation, true matched images captured from the same camera as the query are not considered. Thus, these images have no influence on the re-identification accuracy.

Implementation Details

We used Alexnet [START_REF] Krizhevsky | Imagenet classification with deep convolutional neural networks[END_REF] and Resnet-50 [START_REF] He | Deep residual learning for image recognition[END_REF] as the model architecture and the weights pre-trained on the ImageNet dataset are used as initialisation. We replaced the final layer of the models by a fully-connected layer with 256 output dimensions. Each input image is resized to 256 ×128 pixels. Data augmentation is performed by randomly flipping the images and cropping central regions with random perturbation. Adam optimiser is used and the initial learning rate is set to 10 4 . Each 80 epochs the learning rate is decreased by a factor of 0.1. The weight decay is set to 0.0005. The training is performed in 200 epochs. And the batch size is set to 128 from 32 identities with 4 images each. The 32 identities are randomly selected without replacement. In principle, for better balance in a training batch, we recommend to use the same number of images per person. We also require at least 2 images per person, in order to form the positive pairs in the loss function. The 4 images provide more flexibility in forming positive pairs while still giving enough possibilities for wrong rankings (negative pairs).

Experimental results

Comparison of different neural network models. To demonstrate the effectiveness of our approach, the well-known Alexnet and Resnet models have been The result of our re-implementation of [START_REF] Hermans | In defense of the triplet loss for person re-identification[END_REF]. To notice that we did not use the same training parameters and fc layer settings as [START_REF] Hermans | In defense of the triplet loss for person re-identification[END_REF] and in [START_REF] Hermans | In defense of the triplet loss for person re-identification[END_REF], the test data augmentation is performed. used in our experiments as they have been proven very successful for various computer vision applications. For training both models, we implemented the Hardbatch triplet loss (Eq. 11), a baseline that is our method without (Eq. 9) the ranking-based weighting term and our complete approach, called Rank-Triplet (cf. Eq. 9). Table 1 shows the re-identification results on the Market-1501 dataset.

The Resnet50-based model trained with Rank-Triplet shows a better performance than the Alexnet-based model by a margin of 9.9% point for R1 and 18.2% points for mAP. Integrating our evaluation measure gain weighting of Rank-Triplet raised the mAP by 1.8% points and 0.8% points and R1 by 1.8% points and 1.5% points with Alexnet and Resnet respectively. The Hardbatch approach with Alexnet cannot converge on the Market-1501 dataset. This demonstrates that hard example mining can make the learning more effective, but only using the hardest examples may severely perturb the learning process.

Comparison of different loss functions. We conducted experiments with different loss results are shown in Table 2. For the supervised classification with identity labels, the softmax cross entropy loss is used. The margin in the Siamese loss and triplet loss is fixed to the default value m =1. For the pairwise Siamese learning the contrastive loss is used, we generate all possible pairs of images within a batch. The loss is calculated as follows:

L contrastive = 1 N N i=1 l f (x i )-f (x j ) 2 2 +(1-l) max(m-f (x i )-f (x j ) 2 2 , 0) , ( 10
)
where N is the number of pairs, x i , x j are feature embeddings for two images, l is 1 for images from the same person (positive pairs) and 0 for images from different persons (negative pair).

The triplet loss is calculated according to Eq. 8. And the Hardbatch triplet loss is computed using only the hardest positive image and negative image with respect to a query x i :

L Hardbatch = 1 N N i=1 max( max j∈T C i f (x i ) -f (x j ) 2 2 -min k∈F C i ) f (x i ) -f (x k ) 2 2 +m, 0) , ( 11
)
where N is the number of triplets, T C i /F C i is the true/false correspondence set of the i-th example.

The quadruplet loss in [START_REF] Chen | Beyond triplet loss: a deep quadruplet network for person re-identification[END_REF] propose to, based on triplets, pushes away also negative pairs from positive pairs w.r.t different probe images. The loss is formulated as:

E quadruplet = - 1 N N i=1 [max( f (x i ) -f (x j ) 2 2 -f (x i ) -f (x k ) 2 2 +m 1 , 0) + max( f (x i ) -f (x j ) 2 2 -f (x k ) -f (x l ) 2 2 +m 2 , 0)], (12)
where x j is the feature embeddings of an image from the same identity as x i and x k ,x l are from different identities. As [START_REF] Chen | Beyond triplet loss: a deep quadruplet network for person re-identification[END_REF], we set the m 1 = 1, m 2 = 0.5. Finally, we implement a baseline with the Rank-Triplet loss function (Eq. 9) without the term of evaluation gain weighting. But the triplet selection is still based on online ranking orders.

Rank-Triplet achieved the best performance among these loss functions. The Rank-Triplet improves the baseline by a margin of 1.5% points for R1 and 0.8% points for mAP. This shows the effectiveness of the list-wise evaluation measurebased weighting. The Rank-Triplet gives also better results than the Hardbatch. This shows that using moderate difficult examples and weighting them helps the metric learning. In fact, Hardbatch is a particular weighting with weight=1 given to the hardest examples and 0 given to the rest. Also Hardbatch shows better performance than the normal triplet loss, confirming the effectiveness of the hardest example mining in [START_REF] Ahmed | An improved deep learning architecture for person reidentification[END_REF][START_REF] Hermans | In defense of the triplet loss for person re-identification[END_REF]. Using the quadruplet loss also slightly improves the performance with respect to triplets. This could eventually be combined with our loss.

Comparison with state-of-the-art methods. We compared our method with state-of-the-art methods on the three benchmark datasets. The results are shown in Table 3. We followed the same standard evaluation protocol for all the compared methods and datasets.

Our method Rank-Triplet achieves better results than most of the other methods on the three benchmarks. Only on Market-1501, HA-CNN obtains a better R1 score with a lower mAP, and DPFL and HA-CNN achieve a better R1 score on DukeMTMCReid with a much lower mAP also. This could be due to the multiscale approach of DPFL and an effective attention-mechanism in HA-CNN. Note that these techniques could also easily be applied to our model. Also the fact that the R1 score is slightly higher but not the mAP indicates the overall ranking produced by our method is generally more consistent and accurate. For the CUHK03 dataset, the performance of these methods is clearly below the one of our Rank-Triplet approach. This may be explained by the smaller number of images per person in CUHK03 (4.8 images an average), which may not be enough for training these large models. Note that, as many state-of-the-art approaches, we employed re-ranking [START_REF] Zhong | Re-ranking person re-identification with k-reciprocal encoding[END_REF][START_REF] Yu | Divide and fuse: A re-ranking approach for person reidentification[END_REF] which uses information from nearest neighbours in the gallery and significantly improves the performance. On the CUHK03 benchmark, our methods achieves the superior results. Since EDPF and SVDNet are based on classification loss. The CUHK03 datasets contains less images per person. That is not enough to train a good classifier. However, triplet loss is not much affected because we could still form a large number of triplets even there's less images per person. Since the main contribution of these two state-or-the-art methods focus on the network architecture, their methods could eventually combine with our loss function.

The Hardbatch triplet learning on DukeMTMC-Reid had difficulty to converge with an initial learning rate of 10 -4 . The convergence improved when the learning rate was reduced to 2 × 10 -5 . But it still gave an inferior final performance. Some representative successful and failed top-10 Rank-Triplet results are shown in Fig. 4. As can be seen, most of the errors are due to the high clothing similarity among pedestrians and to some partial occlusion. Even for a human, it is difficult to decide if they represent a real match or not.

Analysis of the proposed method

Evolution of R1 and mAP during training. The online calculation of R1 and mAP could be also used as a training index to observe the progression of the training. We further analysed the R1 and mAP values computed for each batch during training. Further, a separate validation batch is formed with 128 random images from 32 persons that were not used for training We evaluate the mAP, R1, number of mis-ranked pairs and loss for each epoch. The curves showing the evolution of these measures during training are shown in Fig. 5.

We can observe that the R1 and mAP computed on the training batches converge to 1 and the number of mis-ranked pairs almost converges to 0. The validation mAP and R1 also increase and converge during training. The number of mis-ranked pairs decrees with fluctuation, and finally converges. The validation loss naturally increases because the loss is the average among the mis-ranked pairs, and after solving the simple cases, it remains only the mis-ranked pairs giving a high loss with a large evaluation weighting. Thus, validation loss is not suitable to observe the training process, as discussed In [START_REF] Hermans | In defense of the triplet loss for person re-identification[END_REF]. The online validation mAP and R1 that we proposed to observe can be better training index.

Training time analysis. In order to analyse the complexity of Rank-Triplet, we compared its training time with the one of Hardbatch. The results are shown in Table 4. All algorithms are implemented in Pytorch. The training was performed with Intel i7-5930K 3.50GHZ CPU and 2 Nvidia GTX Titan Maxwell GPUs. The Hardbatch triplet loss has first been implemented with Eq. 11. Surprisingly, this implementation takes about 1 hour more for training than our Rank-Triplet. A probable explanation is that the Hinge function slowed down the training. That means, even if the triplets do not violate the constraint, the gradient is still calcu- Method mAP (in%) Neural codes [START_REF] Babenko | Neural codes for image retrieval[END_REF] 75.9 R-MAC [START_REF] Tolias | Particular object retrieval with integral max-pooling of cnn activations[END_REF] 85.2 NetVLAD [START_REF] Arandjelovic | Netvlad: Cnn architecture for weakly supervised place recognition[END_REF] 83.1 Cross-dimension weighting [START_REF] Kalantidis | Cross-dimensional weighting for aggregated deep convolutional features[END_REF] 84.9 Hard Siamese [START_REF] Radenović | Cnn image retrieval learns from bow: Unsupervised fine-tuning with hard examples[END_REF] 82.5 ROI-Triplet [START_REF] Gordo | Deep image retrieval: Learning global representations for image search[END_REF] 90.7 Baseline 85.1 Rank-Triplet 85.8

Table 5: Experimental evaluation on the Holidays dataset.

Image retrieval

To further evaluate our method, we tested our Rank-Triplet loss on a more general content-based image retrieval problem, where the task is to retrieve images from a gallery set that belong to the same category as the probe image or are similar to it. As with the person re-identification task, the challenges are translation, rotation and scaling transformations of the objects of interest in the images and also illumination changes. We use the INRIA Holidays [START_REF] Jegou | Hamming embedding and weak geometric consistency for large scale image search[END_REF] dataset to perform the evaluation. Images are considered from the same category/class, i.e. relevant to a specific query, if they are taken in the same scene or showing the same object under different viewpoints. The dataset contains 500 queries and 991 corresponding relevant images. For the training, we used the landmark dataset as in [START_REF] Babenko | Neural codes for image retrieval[END_REF][START_REF] Gordo | Deep image retrieval: Learning global representations for image search[END_REF]. However, we were only able to use a subset of the dataset due to broken URLs.

In total, we used 28777 images of 560 landmarks for training. For the training and the test, the input images are randomly cropped to 320×320 from 362×362. Since there is a high variance of translation and scale of relevant objects inside the images, we replaced the last global average pooling by a global max-pooling as in [START_REF] Tolias | Particular object retrieval with integral max-pooling of cnn activations[END_REF]. All other experimental settings remain the same. Table 5 shows the comparison with the state-of-the-art methods and with the baseline. Our method performs slightly better than the baseline and is superior to most state-of-the-art results. The ROI-triplet method uses also a triplet network and integrates a pretrained ROI pooling to localise the salient image content. This technique could also be integrated in our model to further improve the instance retrieval performance.

Conclusion

In this paper, we proposed a new learning-to-rank approach to perform similarity learning with images using Convolution Neural Networks. We introduced a novel list-wise loss function directly integrating ranking evaluation measures inspired by the idea of LambdaRank. An online ranking within training batches is performed to evaluate the importance of different triplets composed of probe, mis-ranked true and false correspondences and to weight the loss with the rank improvement for a given query. We experimentally showed that taking into account the evaluation measures during training and calculating the loss in a list-wise way improves the overall ranking and recognition performance on the given task of person re-identification. Further, our proposed loss function outperforms other common functions in the literature and achieved state-of-the-art results on three different benchmarks. Finally, we applied the proposed approach to a more general image retrieval problem with photographs of very diverse content. Without any major modifications, our algorithm outperformed most state-of-the-art methods on the Holiday benchmark showing the general applicability of our approach.

Fig. 1 :

 1 Fig. 1: Schematic illustration of Rank-Triplet. An image of a person of interest on the left (the query) is used to rank images from a gallery according to how closely they match that person. The correct match, highlighted in a blue box, can be difficult to find given the similar negative images, pose and viewpoint variations and occlusions. During training, we propose to estimate the importance of misranked pairs by the gain of the evaluation measure incurred by swapping the rank positions and to weight the loss according to their importance. In this example, swapping the falsely ranked (positive) image on the right with the leftmost one would lead to the biggest improvement (∆Eval).

Fig. 2 :

 2 Fig. 2: Overview of the training procedure of the proposed Rank-Triplet approach.

Algorithm 1 : 2 Randomly sample M identities 3 Randomly sample K images for each identity 4 Form 5 Forward 6 Y = fw(X) 7 L = 0 8 for i = 1 ...KM do 9 D 10 foreach j that Id i = Id j do 11 D j ← D j + margin 12 end 13 R 20 L

 123456781910111320 Similarity learning with Rank-Triplet loss Input: Training image set, identity label set, learning rate λ Output: The network weights W 1 Initialise W for t = 1...T do the training batch with images and identity labels X = {x i } KM i=1 , ID = {Id i } KM i=1 pass to obtain image embeddings Y = {y i }: ← dist(y i , y j=1...KM,j =i ) ← sort(D) 14 AP, R1 ← calculateAP R1(R) 15 foreach j with Id i = Id j do 16 foreach k with R k < R j and Id k = Id j do 17 R ← swap(R k , R j ) 18 AP , R1 ← calculateAP R1(R ) 19 eval gain ← AP -AP + R1 -R1 ← L + (D j -D k ) × eval gain

Fig. 3 :

 3 Fig. 3: Some image examples from different person re-identification datasets

Fig. 4 :

 4 Fig. 4: Some ranking results. The query image is on the left, the true matches are surrounded by green boxes and false matches are surrounded by red boxes. The two top rows are from Market-1501, the tow middle rows are from DukeMTMC-Reid, and the two bottom rows are from CUHK03.

Fig. 5 :

 5 Fig. 5: Evolution of training and validation mAP, R1 and number of mis-ranked pairs.

Table 1 :

 1 Re-identification performance on the Market-1501 dataset in terms of rank 1 (R1) and mean average precision (mAP) (in %) for different loss functions and neural network models.

		Resnet	Alexnet
		R1	mAP	R1	mAP
	Hardbatch	81.0	63.9	-	-
	Baseline	82.1	66.5	70.9	47.3
	Rank-Triplet	83.6	67.3	72.7	49.1
	Loss function	R1	mAP
	Classification loss	74.3	51.0
	Siamese loss	62.9	46.6
	Triplet loss	74.3	56.5
	Quadruplet loss	74.9	58.1
	Hardbatch*	81.0	63.9
	Baseline	82.1	66.5
	Rank-Triplet	83.6	67.3

Table 2 :

 2 Re-identification results(in %) on Market-1501 with different loss functions.

*:

Table 3 :

 3 Comparison with state-of-the-art methods on person re-identification.

Table 4 :

 4 Training time on Market-1501. lated on these triplets. Then we optimise the Hardbatch code by adding a condition flow in order to calculate the loss only for the necessary triplets. The training time for Rank-Triplet is considerably reduced. After this optimisation, the Hardbatch takes about 40 minutes less than the Rank-Triplet loss. That difference roughly corresponds to the time of ranking, evaluation measure computation and the use of more triplets at each iteration. However, we consider that this is a reasonable extra cost given the overall performance improvement.


Alexandre Fernandez

Luidnel Maignan

Antoine Spicher

Antoine Spicher Cellular Automata

Extensions. Kan

Cellular Automata and Kan Extensions

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Cellular automata are usually presented either as a local behavior extended to a global and uniform one or as a continuous uniform global behavior for the appropriate topology [START_REF] Ceccherini-Silberstein | Cellular Automata and Groups[END_REF]. We offer here a third, fruitful, point of view easing many generalizations of the concepts pioneered by cellular automata, e.g. via so-called global transformation [START_REF] Maignan | Global graph transformations[END_REF][START_REF] Fernandez | Lindenmayer systems and global transformations[END_REF]. The goal of this paper is not to elaborate on these generalizations but to focus on some simple foundational bridges allowing these generalizations. In particular, we focus on Kan extensions, a categorical notion allowing, as we show here, to capture local/global descriptions [START_REF] Maclane | Categories for the Working Mathematician[END_REF]. While categories are generalizations of monoids and posets, the case of cellular automata can be fully treated in terms of posets only. Once the involved structures made clear via posets, the transition to category is precisely what enables the generalizations in a surprisingly smooth way as discussed in the final section.

In this paper, we recall the direct definitions of cellular automata on groups, local transition function, global transition function, shift action, and also consider the counterparts of these functions on arbitrary partial configurations. This bigger picture allows to show that the various local/global relations between these objects are all captured by left and right Kan extensions, the latter providing a alternative definition of these objects. The proofs are provided in detail to show how the concept can be easily manipulated once understood. We also introduce slightly more generality that one would typically need in order to enrich the presentation of Kan extensions in a hopefully useful way. In the final section, we comment on the link with Curtis-Hedlung theorem and discuss briefly the smooth transition to more general systems where the space itself has to evolve.

Cellular Automata and Kan Extensions

Let us give some basic definitions to fix the notations. We also note small caveats early on, to avoid having to deal with many unrelated details at the same time in a single proof or construction latter on.

Cellular Automata

Definition 1. A group is a set G with a binary operation -• -: G × G → G which is associative, which has a neutral element 1 and for which any g ∈ G has inverse g -1 . A right action of the group on a set X is a binary operation -◭ -: X × G → X such that x ◭ 1 = x and (x ◭ g) ◭ h = x ◭ (g • h).

In cellular automata, the group G represents the space, each element g ∈ G being at the same time an absolute and a relative position. This space is decorated with states that evolve through local interactions only. The classical formal definitions go as follows and work with the entire, often infinite, space.

Q G ×G → Q G is defined on Q G by (c ◭ g)(h) = c(g • h). The global transition function ∆ : Q G → Q G of such a cellular automaton is defined as ∆(c)(g) = δ((c ◭ g) ↾ N ).
Proposition 3. The latter right action is indeed a right action.

Proof. For any

g, h ∈ G, we have ((c ◭ g) ◭ h)(i) = (c ◭ g)(h.i) = c(g • h • i) = (c ◭ (g • h))(i) for any i ∈ G, so ((c ◭ g) ◭ h) = (c ◭ (g • h)) and also (c ◭ 1)(i) = c(1 • i) = c(i) as required by Definition 1 of right actions.
This choice of definition and right notation for the so called shift action has two advantages. Firstly, the definition of the action is a simple associativity. Secondly, when instantiated with G = Z with sum, the content of c ◭ 5 is the content of c shifted to the left, as the symbols indicates. Indeed, for

c ′ = c ◭ 5, c ′ (-5) = c(0) and c ′ (0) = c(5). Proposition 4. For all c ∈ Q G and g ∈ G, ∆(c)(g) is only function of c ↾ g •N . Proof. Indeed, ∆(c)(g) = δ((c ◭ g) ↾ N ) so the value is determined by (c ◭ g) ↾ N . But for any n ∈ N , (c ◭ g)(n) = c(g • n) by definition of ◭.
In common cellular automata terms, this proposition means that the neighborhood of g is g • N , in this order. Let us informally call objects of the form c ↾ g • N ∈ g∈G Q g•N a shifted local configuration. Note that, at our level of generality, two different positions g = g ′ ∈ G might have the same neighborhood g • N = g ′ • N . Although the injectivity of the function (-• N ) could be a useful constraints to add, which is often verified in practice, we do not impose it so the reader should keep this in mind. A second thing to keep in mind is that we do not require here that the neighborhood should be finite. This is done only because this property is not used in the formal development below. Because of this, it is useful to replace the shifted local configurations, i.e. the union g∈G Q g•N , by the disjoint union g∈G ({g} × Q g•N ). The elements of the latter are of the form (g ∈ G, c ∈ Q g•N ) and keep track of the considered "center" of the neighborhood. More explicitly, two elements (g 0 , c

↾ g 0 • N ), (g 1 , c ↾ g 1 •N ) ∈ g∈G ({g}×Q g•N ) are different as soon as g 0 = g 1 even if g 0 •N = g 1 •N .
This encodes things according to the intuition of a centered neighborhood.

The Poset of (Partial) Configurations

In the previous formal statements, one sees different kinds of configurations, explicitly or implicitly:

global configurations c ∈ Q G , local configurations (c ◭ g) ↾ N ∈ Q N , shifted local configurations c ↾ g • N ∈ Q g•N ,
and their resulting "placed states" (g → ∆(c)(g)) ∈ Q {g} . In the cellular automata literature, one often considers configurations defined on other subsets of the space, e.g. finite connected subsets. More generally, we are interested in all partial configurations Q S for arbitrary subsets S ⊆ G. The restriction operation (-↾ -) used many times above gives a partial ordering of these partial configurations. Proposition 7. The latter right action is well-defined and is a right action.

Proof. The configuration c ◭ g is well-defined on all of its support. Indeed for any h ∈ |c ◭ g|, (c ◭ g)(h) = c(g • h) and g • h ∈ |c| by definition of h. The right action property is verified as in the proof of Proposition 3.

Let us restate Proposition 4 more precisely using Definition 6.

Proposition 8. For all c ∈ Q G and g ∈ G, (c ◭ g) ↾ N = (c ↾ g • N ) ◭ g. Proof. Indeed, |(c ↾ g • N ) ◭ g| = {h ∈ G|g • h ∈ |(c ↾ g • N )|} = {h ∈ G|g • h ∈ g • N } = N = |(c ◭ g) ↾ N |. Also for any n ∈ N , ((c ◭ g) ↾ N )(n) = (c ◭ g)(n) = c(g • n) and ((c ↾ g • N ) ◭ g)(n) = (c ↾ g • N )(g • n) = c(g • n).
Definition 9. A partial order on a set X is a binary relation ⊆ X × X which is reflexive, transitive, and antisymmetric. A set endowed with a partial order is called a partially ordered set, or poset for short. Definition 10. Given any two configurations c, c ′ ∈ Conf, we set c c ′ if and only if ∀g ∈ |c|, g ∈ |c ′ | ∧ c(g) = c ′ (g). This is read "c is a subconfiguration of c ′ " or "c ′ is a superconfiguration of c". Proof. As can be readily seen, since each global configuration restricts to many shifted local configurations, and recalling that an antichain is a subset S of the poset such that neither x x ′ nor x ′ x hold for any two different x, x ′ ∈ S.

Kan Extensions (in the 2-Category of Posets)

Given three sets A, B and C such that A ⊆ B, we say that a function g :

B → C extends a function f : A → C if g ↾ A = f , or equivalently if g • i = f
where i is the obvious injective function from A to B. For a given f : A → C, there are typically many possible extensions. Roughly speaking, Kan extensions formalizes, among many things, the mathematical practice where extensions are rarely arbitrary. One usually chooses the "best" or "most natural" extensions. There is therefore an implicit comparison considered between the extensions. This is the reason why Kan extensions are formally defined at the level of 2-categories: A, B, C are objects, f , g, i, and all (not necessarily "most natural") extensions are 1-morphisms between these objects, and the "naturality" comparison between 1-morphisms are 2-morphisms. However, we do not need to discuss things at this level of generality here. For our particular case, the objects are posets, the 1-morphisms are monotonic functions and the monotonic functions are compared pointwise.

Definition 12. Given two posets (X, X ) and (Y, Y ), a function f : X → Y is said to be monotonic if for all x, x ′ ∈ X, x X x ′ implies f (x) Y f (x ′ ).
Proposition 13. For any g ∈ G, the function (-◭ g) : Conf → Conf is monotonic.

Proof. Given any c, c ′ ∈ Conf such that c c ′ , this claim is equivalent to:

(c ◭ g) (c ′ ◭ g) (by Def 12) ⇐⇒ ∀h ∈ |c ◭ g|; h ∈ |c ′ ◭ g| ∧ (c ◭ g)(h) = (c ′ ◭ g)(h) (Def 10) ⇐⇒ ∀h ∈ G s.t. g • h ∈ |c|; g • h ∈ |c ′ | ∧ c(g • h) = c ′ (g • h) (Def 6)
which is true by the application of Definition 10 of c c ′ on g • h.

Definition 14. Given two posets (X, X ) and (Y, Y ), we define the binary relation -⇒on the set of all monotonic functions from

X to Y by f ⇒ f ′ ⇐⇒ ∀c ∈ Conf, f (c) Y f ′ (c).
Proposition 15. Given two posets (X, X ) and (Y, Y ), the set of monotonic functions between them together with this binary relation forms a poset.

Proof. As one can easily check.

Definition 16. In this setting, given three posets A, B and C, and three monotonic functions i : A → B, f : A → C and g : B → C, g is said to be the left (resp. right) Kan extension of f along i if g is the ⇒-minimum (resp. ⇒maximum) element in the set of monotonic functions {h :

B → C | f ⇒ h • i} (resp. {h : B → C | h • i ⇒ f }).
This concept is particularly useful because, whenever it applies, it is also a complete characterization as stated in the following proposition in the left case.

Proposition 17. The left Kan extension g is unique when it exists.

Proof. It is defined as the minimum of a set, and a minimum is always unique when it exists.

Another suggestive way to read the concept of Kan extensions with respect to this paper is to say that a function g on a poset can be summarized into, or generated by, a part of its behavior f on just a small part of the poset. Note however that i does not need to be injective in this definition.

Kan Extensions in Cellular Automata

A First Approach To Partial Configurations

The first, intuitive, approach is to take a configuration c, look for all places g where the whole neighborhood g • N is defined and to take the local transition result of these places only. We first give a direct formal definition, and then show that this is a left Kan extension. This shows in particular that the global transition function is the left Kan extension of the "fully shifted" local transition. The sense of "fully shifted" is described below and is only necessary because we restrict ourselves to posets, as discussed in the final section of this paper.

c ∈ Q g•M , |Φ(c)| = ∅. Also, for any c ∈ Q G , |Φ(c)| = ∆(c).
Proof. By Definition 19 of Φ.

Characterization as a Left Kan Extension

The coarse transition function Φ is defined on the set of all configurations Conf and we claim that it is generated, in the Kan extension sense, by the local transition function δ shifted everywhere. We define the latter, with Proposition 5 in mind.

Definition 23. We define Loc to be the poset Loc = g∈G ({g} × Q g•N ) with trivial partial order (g, c) Proof. Indeed, take c, c ′ ∈ Conf such that c c ′ . We want to prove that Φ(c) Φ(c ′ ) and this is equivalent to:

(g ′ , c ′ ) ⇐⇒ (g, c) = (g ′ , c ′ ).
∀g ∈ |Φ(c)|, g ∈ |Φ(c ′ )| ∧ Φ(c)(g) = Φ(c ′ )(g) ⇐⇒ ∀g ∈ int(|c|), g ∈ int(|c ′ |) ∧ δ(c ◭ g ↾ N ) = δ(c ′ ◭ g ↾ N ) ⇐⇒ ∀g ∈ G s.t. g • N ⊆ |c|, g • N ⊆ |c ′ | ∧ δ(c ◭ g ↾ N ) = δ(c ′ ◭ g ↾ N ),
by Definition 6 of , Definition 19 of Φ, and Definition 18 of int. The final statement is implied by: Proof. By Definition 16 of left Kan extensions, we need to prove firstly that Φ is such that δ ⇒ Φ • π 2 , and secondly that it is smaller than any other such monotonic functions.

∀g ∈ G s.t. g • N ⊆ |c|, g • N ⊆ |c ′ | ∧ c ◭ g ↾ N = c ′ ◭ g ↾ N ⇐⇒ ∀g ∈ G s.t. g • N ⊆ |c|, g • N ⊆ |c ′ | ∧ ∀n ∈ N, (c ◭ g)(n) = (c ′ ◭ g)(n) ⇐⇒ ∀g ∈ G s.t. g • N ⊆ |c|, g • N ⊆ |c ′ | ∧ ∀n ∈ N, c(g • n) = c ′ (g • n),
For the first part, δ ⇒ Φ • π 2 is equivalent to: ∀(g, c) ∈ Loc, δ(g, c) Φ(c) (Defs. 14 and 23 of ⇒ and π 2 )

⇐⇒ ∀(g, c) ∈ Loc, ∀h ∈ |δ(g, c)|, h ∈ |Φ(c)| ∧ δ(g, c)(h) = Φ(c)(h) (D. 10 of ) ⇐⇒ ∀(g, c) ∈ Loc, g ∈ |Φ(c)| ∧ δ(c ◭ g) = Φ(c)(g) (Def. 23 of δ) ⇐⇒ ∀(g, c) ∈ Loc, g • N ∈ |c| ∧ δ(c ◭ g) = δ((c ◭ g) ↾ N ) (Defs 18, 19 of Φ).
This last statement is true by Definition 23 of Loc, since c ∈ Q g•N .

For the second part, let F : Conf → Conf be a monotonic function such that δ ⇒ F • π 2 . We want to show that Φ ⇒ F , which is equivalent to:

∀c ∈ Conf, Φ(c) F (c) (Def. 14 of ⇒) ⇐⇒ ∀c ∈ Conf, ∀g ∈ |Φ(c)|, g ∈ |F (c)| ∧ Φ(c)(g) = F (c)(g) (Def. 10 of ) ⇐⇒ ∀c ∈ Conf, ∀g ∈ int(|c|), g ∈ |F (c)| ∧ F (c)(g) = δ((c ◭ g) ↾ N ) (Def. 19)
So take c ∈ Conf and g ∈ int(|c|), and consider As a sidenote, remark that in order to have the equality δ = Φ•π 2 , one needs to have the injectivity of neighborhood function. Indeed, without injectivity, we have two different g, g ′ ∈ G having the same neighborhood M , i.e. M = g • N = g ′ • N . This means that, given any local configuration c ∈ Q M on this neighborhood, each pair (g, c), (g ′ , c) ∈ Loc have different results δ(g, c) ∈ Q {g} and δ(g ′ , c) ∈ Q {g ′ } with different support {g} and {g ′ }. However, their common projection π 2 (g, c) = π 2 (g ′ , c) = c have a unique result Φ(c) with a support such that {g, g ′ } ⊆ |Φ(c)|. So we have a strict comparison δ ⇒ Φ • π 2 . When the neighborhood function is injective, π 2 is also injective and the previous situation can not occur so we have equality δ = Φ • π 2 .

d g = c ↾ g • N . Since d g c and F is monotonic, we have F (d g ) F (c). Moreover δ ⇒ F • π 2 and (g, d g ) ∈ {g} × Q g•N ⊆ Loc, so δ(g, d g ) F (d g )

A Second Approach To Partial Configurations

For some applications, the previous definitions are too naive. For example, it is common to consider two cellular automata to be essentially the same if they generate the same global transition functions. However, here, two such cellular automata give different coarse transition function if they have a different neighborhood.

To refine the previous definitions, a second approach is to take a configuration c, and look at all places for which the result is already determined by the partial data defined in c. So we consider all g ∈ G for which all completions of the data present on the defined neighborhood g • N ∩ |c| into a configuration on the complete neighborhood g • N always lead to the same result by δ.

A Direct Definition

Definition 27. For any c ∈ Conf and g ∈ G, let

c g = c ↾ (g • N ∩ |c|). Definition 28. Given a configuration c ∈ Conf, its determined subset is det(c) = {g ∈ G | ∃q ∈ Q, ∀c ′ ∈ Q g•N , c ′ ↾ |c g | = c g =⇒ δ(c ′ ◭ g) = q}.
For any g ∈ det(c), we denote q c,g ∈ Q the unique state q having the mentioned property.

Note that this definition depends on the cellular automaton local transition function δ and on the data of the configuration c, contrary to Definition 18 of interior that only depends on its neighborhood N and on the support of the configuration.

Definition 29. Given a cellular automaton, its fine transition function φ :

Conf → Conf is defined as |φ(c)| = det(c) and φ(c)(g) = q c,g , i.e. φ(c)(g) = δ(c ′ ◭ g) for any c ′ ∈ Q N such that c ′ ↾ |c g | = c g .
Proposition 30. The fine transition function φ is well defined.

Proof. This is the case precisely because we restrict the support of φ(c) to the determined subset of the c.

Proposition 31. Consider the constant cellular automaton δ(c) = q ∀c ∈ Q N for a specific q ∈ Q and regardless of the neighborhood N chosen to represent it. We have |φ(c)| = G for any c ∈ Conf.

Proof. Indeed, even with no data at all, i.e. for c such that |c| = ∅, the result at all position is determined and is q.

Characterization as a Right Kan Extension

As for the coarse transition function, the fine transition function φ is defined on the set of all configurations Conf and we claim that it is generated, in the Kan extension sense. We consider two ways to generate it and start by the simplest one. The second one is considered in the following section using sublocal configurations in order to be closer to the direct definition and to be a "from local to global" characterization.

Proposition 32. For any g ∈ G, the functiong : Conf → Conf of Definition 27 is monotonic.

Proof. As one can easily check.

Proposition 33. The fine transition function φ is monotonic.

Proof. Indeed, take c 0 , c 1 ∈ Conf such that c 0 c 1 . We want to prove that φ(c 0 ) φ(c 1 ) and this is equivalent to:

∀g ∈ |φ(c 0 )|, g ∈ |φ(c 1 )| ∧ φ(c 0 )(g) = φ(c 1 )(g) (Def 10 of ) ⇐⇒ ∀g ∈ det(c 0 ), g ∈ det(c 1 ) ∧ q c0,g = q c1,g (Def 29 of φ)
Take g ∈ det(c 0 ). We want to prove that g ∈ det(c 1 ), which means by Definition 28 of det(c 1 ):

∃q ∈ Q, ∀c 2 ∈ Q g•N , c 2 ↾ |(c 1 ) g | = (c 1 ) g =⇒ δ(c 2 ◭ g) = q
We claim that the property is verified with q = q c0,g . Indeed, take any

c 2 ∈ Q g•N such that c 2 ↾ |(c 1 ) g | = (c 1 ) g . We also have that c 2 ↾ |(c 0 ) g | = (c 0 ) g since the hypothesis c 0 c 1 implies (c 0 ) g (c 1
) g by Proposition 32. By Definition 28 of det(c 0 ), we obtain that δ(c 2 ◭ g) = q c0,g , so q = q c0,g has the wanted property, which implies that g ∈ det(c 1 ) as wanted. But the above property of q set it to be precisely what we denote by q c1,g (Def 28 of q c1,g ), so q c0,g = q c1,g .

Proposition 34. The fine transition function φ is the right Kan extension of the global transition function ∆ along the inclusion

i : Q G → Conf.
Proof. By Definition 16 of right Kan extensions, we need to prove firstly that φ is such that φ • i ⇒ ∆, and secondly that it is greater than any other such monotonic functions.

For the first part, we actually have φ

• i = ∆ since for any c ∈ Q G , |φ(c)| = det(c) = G = |∆(c)| and for any g ∈ G, we have φ(c)(g) = q c,g = δ(c g ◭ g) = δ((c ↾ g • N ) ◭ g) = δ((c ◭ g) ↾ N ) = ∆(c)(g)
by Defs. 29, 28, 27, 2 of φ, det, c g and ∆ and Prop. 8.

For the second part, let f : Conf → Conf be a monotonic function such that f • i ⇒ ∆. We want to show that f ⇒ φ, which is equivalent to:

∀c ∈ Conf, f (c) φ(c) (Def. 14 of ⇒) ⇐⇒ ∀c ∈ Conf, ∀g ∈ |f (c)|, g ∈ |φ(c)| ∧ f (c)(g) = φ(c)(g) (Def. 10 of ) ⇐⇒ ∀c ∈ Conf, ∀g ∈ |f (c)|, g ∈ det(c) ∧ f (c)(g) = q c,g (Def. 35 of φ) ⇐⇒ ∀c ∈ Conf, ∀g ∈ |f (c)|, ∀c ′ ∈ Q g•N , c c ′ =⇒ f (c)(g) = δ(c ′ ◭ g) (D. 28) So take c ∈ Conf and g ∈ |f (c)| and c ′ ∈ Q g•N such that c c ′ . Consider any c ′′ ∈ Q G such that c ′ c ′′ (or equivalently c ′′ ↾ g •N = c ′ ). Since f is monotonic, we have f (c) f (c ′′ ), which means that f (c)(g) = f (c ′′ )(g) by Def. 10. But since f • i ⇒ ∆, we have f (c)(g) = ∆(c ′′ )(g) = δ((c ′′ ◭ g) ↾ N ) by Def. 14 of ⇒ and Def. 2 of ∆. But by Prop. 8, (c ′′ ◭ g) ↾ N = (c ′′ ↾ g • N ) ◭ g = c ′ ◭ g.

Introducing Sub-Local Configurations

The direct definition of the fine transition function is explicitly about assigning a result for a configuration c at a given g ∈ G even when the whole neighborhood g • N is not complete. By isolating these "shifted sub-local configuration" in the poset of configurations, we can (right-)extend the local transition to them and show that, in the same way as the coarse transition function is the left Kan extension of the local transition function, the fine transition function is the left Kan extension of the sub-local transition function.

Direct Definition

Definition 35. We define Sub = g∈G,M⊆N ({g} × Q g•M ) with partial order defined as (g, c) (g ′ , c ′ ) if and only if g = g ′ and c c ′ . The "fully shifted sublocal transition function" δ : Sub → Conf is defined, for any g ∈ G, any M ⊆ N and any c ∈

Q g•M , as |δ(g, c)| = {g}∩det(c) and, if g ∈ det(c), δ(g, c)(g) = q c ′ ,g , i.e. δ(g, c)(g) = δ(c ′ ◭ g) for any c ′ ∈ Q g•N such that c = c ′ ↾ |c|. The second projection of Sub is the function π 2 : Sub → Conf defined as π 2 (g, c) = c.
In this definition, a given sub-local configuration can result either in an empty configuration when the transition is not determined, or in a configuration with only singleton support when the transition is determined.

Note that for a given cellular automaton, it is possible to restrict the poset Sub to an antichain. Indeed, any time a result is determined by a sub-local configuration (g, c), all bigger sub-local configuration (g, c ′ ) with c c ′ does not contribute anything new. We do not elaborate on this because this antichain would be different for each cellular automaton, blurring the global picture presented below.

Characterization as a Right Kan Extension

Proposition 36. The fully shifted sub-local transition function δ is monotonic Proof. As usual, take (g, c), (g ′ , c ′ ) ∈ Sub such that (g, c) (g ′ , c ′ ). First note that g = g ′ by Definition 35. We want to prove that δ(g, c) δ(g, c ′ ) and this is equivalent to: Proof. By Definition 16 of right Kan extensions, we need to prove firstly that δ is such that δ • i ⇒ δ, and secondly that it is greater than any other such monotonic functions.

∀h ∈ |δ(c)|, h ∈ |δ(c ′ )| ∧ δ(c)(h) = δ(c ′ )(h) ⇐⇒ ∀h ∈ {g} ∩ det(c), h ∈ {g} ∩ det(c ′ ) ∧ q c,g = q c ′ ,g ⇐⇒ g ∈ det(c) =⇒ g ∈ det(c ′ ) ∧ q c,g = q c ′ ,g ′ ,
For the first part, δ • i ⇒ δ is equivalent to: This last statement is true by Def. 28 of q c,g . For the second part, let f : Sub → Conf be a monotonic function such that f • i ⇒ δ. We want to show that f ⇒ δ, which is equivalent to: Proof. By Definition 16 of left Kan extensions, we need to prove firstly that φ is such that δ ⇒ φ • π 2 , and secondly that it is smaller than any other such monotonic functions.

∀(g, c) ∈ Loc, δ(g, c) δ(g, c) (Def. 14 of ⇒) ⇐⇒ ∀(g, c) ∈ Loc, ∀h ∈ |δ(g, c)|, h ∈ |δ(g, c)| ∧ δ(g, c)(h) = δ(g, c)(h) (D.
∀(g, c) ∈ Sub, f (g, c) δ(g, c) (Def. 14 of ⇒) ⇐⇒ ∀(g, c) ∈ Sub, ∀h ∈ |f (g, c)|, h ∈ |δ(g, c)| ∧ f (g, c)(h) = δ(g, c)(h) (Def. 10) ⇐⇒ ∀(g, c) ∈ Sub, ∀h ∈ |f (g, c)|, h ∈ {g} ∩ det(c) ∧ f (g, c)(h) = q c,g (Def. 35) So take (g, c) ∈ Sub and h ∈ |f (g, c)|. Consider any c ′ ∈ Loc such that c c ′ . Since f is monotonic, we have f (g, c) f (g, c ′ ), which means that h ∈ |f (g, c ′ )| and f (c)(h) = f (c ′ )(h) by Def. 10. But since f • i ⇒ δ, we have h ∈ |δ(g, c ′ )| = {g} and f (g, c ′ )(h) = δ(g, c ′ )(h) = δ(c ′ ◭ g)
For the first part, δ ⇒ φ • π 2 is equivalent to: ∀(g, c) ∈ Sub, δ(g, c) φ(c) (Defs. 14 and 35 of ⇒ and π 2 )

⇐⇒ ∀(g, c) ∈ Sub, ∀h ∈ |δ(g, c)|, h ∈ |φ(c)| ∧ δ(g, c)(h) = φ(c)(h) (Def 10 of ) ⇐⇒ ∀(g, c) ∈ Sub, g ∈ det(c) =⇒ g ∈ |φ(c)| ∧ q c,g = φ(c)(g) (Def. 35 of δ) ⇐⇒ ∀(g, c) ∈ Sub, g ∈ det(c) =⇒ g ∈ det(c) ∧ q c,g = q c,g (Def 29 of φ),
a most trivial statement.

For the second part, let f : Conf → Conf be a monotonic function such that δ ⇒ f • π 2 . We want to show that φ ⇒ f , which is equivalent to:

∀c ∈ Conf, φ(c) f (c) (Def. 14 of ⇒) ⇐⇒ ∀c ∈ Conf, ∀g ∈ |φ(c)|, g ∈ |f (c)| ∧ φ(c)(g) = f (c)(g) (Def. 10 of ) ⇐⇒ ∀c ∈ Conf, ∀g ∈ det(c), g ∈ |f (c)| ∧ q c,g = f (c)(g) (Def. 29 of φ)
So take c ∈ Conf and g ∈ det(c). Since c g c (Def 27) and f is monotonic, we have f (c g ) f (c). Moreover δ ⇒ f • π 2 and (g, c g ) ∈ Sub so δ(g, c g ) f (c g ) by Definitions 14 and 23 of ⇒ and π 2 . By transitivity δ(g, c g ) f (c). By Definition 35 of δ and Definition 10 of , we therefore have g ∈ |f (c)|, and f (c)(g) = δ(g, d g )(g) = q c,g as wanted.

Final Discussion

There are additional simple structural facts to note about the monotonic functions considered. The first one is that the shift action on partial configurations, as given in Definition 6, is the right Kan extension of the shift action on global configurations, as given in Definition 2. Another one is that Φ ⇒ φ, hence the names of these transition functions, coarse and fine. In fact, any monotonic function f : Conf → Conf such that δ ⇒ f • π 2 is necessarily such that Φ ⇒ f ⇒ φ. This shows, in some sense, the efficiency of the simple constraints of monotonicity and δ ⇒ f • π 2 .

In the formal development presented here, we explicitly "copy" a single local behavior δ on all g ∈ G to obtain δ and work with it. It is readily possible to put a different behavior on each g ∈ G, with no real modification to the proofs. The statements are therefore valid for non-uniform cellular automata and automata networks. As mentioned in the beginning, we did not even used the finiteness of the neighborhood either. At this point, the reader might have the feeling that these results are not really about cellular automata, and there are at least three answers to that. The first answer is that one could easily impose the shift and simultaneously prevent the use of a highly redundant "fully shifted local transition function", but this requires using a category of configuration instead of a poset of configurations. The latter is very similar to the poset, except that the yes/no question "is this configuration a subconfiguration of this other one ?" is replaced by the open-ended question "where does this configuration appear in this other one ?" [START_REF] Maignan | Global graph transformations[END_REF]. The goal of this paper is indeed to introduce the concepts needed for this other point of view, among many others. The second answer is that the proofs are more about the decomposition/composition process involved in the local/global definition of cellular automata. Because of the simplicity of cellular spaces, groups, the description is very simple to make "directly". In other situations, a Kan extension presentation can be the most effective way to describe the spatial extensions/restriction, for example when the space is an evolving graph [START_REF] Maignan | Global graph transformations[END_REF][START_REF] Fernandez | Lindenmayer systems and global transformations[END_REF]. The third answer is that, with small modifications, this result is closely related to the Curtis-Hedlung theorem. Indeed, if one restores the finite neighborhoods and finite states constraints, one can see that the poset of finite support configurations is a "generating" part of the poset of open subsets of the product topology. In this case, the fine transition function φ can be viewed as encoding an important part of the topological behavior of the global transition function ∆ [START_REF] Ceccherini-Silberstein | Cellular Automata and Groups[END_REF].

To finish, let us mention an important aspect of the Kan extensions considered here and in other papers of the author [START_REF] Maignan | Global graph transformations[END_REF][START_REF] Fernandez | Lindenmayer systems and global transformations[END_REF]. They have the property to be pointwise. Intuitively, this means that they can be computed "algorithmically" using simple building blocks. This formulation in terms of building blocks is completely equivalent and is the one used in the other papers, firstly because it is via these building blocks that the authors discovered these links between spatially-extended dynamical systems and category theory, and secondly because this formulation is closer to the software implementations of the considered models. In fact, it is possible to have an implementation completely generic over the particular kind of space considered, e.g. evolving graphs of any sort, evolving higher-order structures such as abstract cell [START_REF] Maignan | Global graph transformations[END_REF], evolving strings such as Lindenmayer systems [START_REF] Fernandez | Lindenmayer systems and global transformations[END_REF], or Cayley graphs as considered here.

Definition 2 .

 2 A cellular automaton on a group G is given by a neighborhood N ⊆ G, a finite set of states Q, and a local transition function δ : Q N → Q. The elements of the set Q N are called local configurations. The elements of the set Q G are called global configurations and a right action -◭ -:

Proposition 5 .

 5 The function -• N : G → 2 G is not necessarily injective. Proof. Considering any group G and N = G, we have g • N = G for any g ∈ G. Considering the group G = Z/2Z × Z and N = {(0, 0), (1, 0)}, we have (0, 0) + N = (1, 0) + N = {(0, 0), (1, 0)} because of the torsion.

Definition 6 .

 6 A (partial) configuration c is a partial function from G to Q. Its domain of definition is denoted |c| and called its support. The set of all configurations is denoted Conf = S⊆G Q S . We extend the previous right action ◭ and define it to map each c ∈ Conf to c ◭ g having support |c ◭ g| = {h ∈ G | g • h ∈ |c|} and states (c ◭ g)(h) = c(g • h).

Proposition 11 .

 11 The set Conf with this binary relation is a poset. In this poset, the shifted local configurations c ∈ g∈G Q g•N are subconfigurations of the (appropriate) global configurations c ′ ∈ Q G . Shifted local configurations form an antichain. Global configurations form an antichain.

3. 1

 1 .1 A Direct Definition Definition 18. The interior of a subset S ⊆ G is int(S) = {g ∈ G | g • N ⊆ S}. Definition 19. The coarse transition function Φ : Conf → Conf is defined for all c ∈ Conf as |Φ(c)| = int(|c|) and Φ(c)(g) = δ((c ◭ g) ↾ N ). Proposition 20. For any c ∈ Conf and g ∈ G, the statements g ∈ int(|c|), g • N ⊆ |c|, and N ⊆ |c ◭ g| are equivalent. (So Φ is well-defined in Definition 19.) Proof. The first and second statements are equivalent by Definition 18 of int. The second and third statements are equivalent by Definition 6 of ◭. Remember Proposition 5. If we do have injectivity of neighborhoods, we have int(g • N ) = {g}. But since we do not assume it, we only have the following. Proposition 21. Let S ⊆ G. In general, S ⊆ int(S • N ) but we do not necessarily have equality, even when S = {g} for some g ∈ G. Proof. Consider the examples in the proof of Proposition 5. Another useful remark on which we come back below is the following. Proposition 22. For any g ∈ G, any M N , and any

  The "fully shifted local transition function" δ : Loc → Conf is defined, for any (g, c) ∈ Loc as |δ(g, c)| = {g} and δ(g, c)(g) = δ(c ◭ g). The second projection of Loc is the monotonic function π 2 : Loc → Conf defined as π 2 (g, c) = c. Proposition 24. Loc is a poset and δ and π 2 are monotonic functions. Proof. Indeed, the identity relation is an order relation and any function respects the identity relation. Proposition 25. The coarse transition function Φ is monotonic.

  the last equivalence being by Definition 6. To prove it, take g ∈ G such that g • N ⊆ |c|, and n ∈ N . Since c c ′ and g • n ∈ |c|, we have g • n ∈ |c ′ |, and c(g• n) = c ′ (g • n) as wanted.Proposition 26. Φ is the left Kan extension of δ along π 2 : Loc → Conf.

  by Definitions 14 and 23 of ⇒ and π 2 . By transitivity δ(g, d g ) F (c). By Definition 23 of δ and Definition 10 of , we obtain g ∈ |F (c)|, and F (c)(g) = δ(g, d g )(g) = δ((c ◭ g) ↾ N ), as wanted.

by

  Definition 6 of and Definition 35 of δ. The end of this proof is similar to the one of Proposition 33. Proposition 37. The fully shifted sub-local transition function δ is the right Kan extension of the fully shifted local transition function δ along the inclusion i : Loc → Sub.

  10 ) ⇐⇒ ∀(g, c) ∈ Loc, g ∈ det(c) =⇒ g ∈ |δ(g, c)| ∧ q c,g = δ(g, c)(g) (Def. 35 of δ) ⇐⇒ ∀(g, c) ∈ Loc, g ∈ det(c) =⇒ g ∈ {g} ∧ q c,g = δ(c ◭ g) (Def 23 of δ).

  by Def. 14 of ⇒ and Def. 23 of δ. Since this is true for any c ′ , this establishes exactly the defining property of det(c) by Def. 28.

3. 3 . 3

 33 The Second Approach as a Left Kan Extension Proposition 38. The projection function π 2 : Sub → Conf is monotonic.Proof. As can be readily checked in Definition 35Proposition 39. φ is the left Kan extension of δ along π 2 : Sub → Conf.