Manish Narwaria

Matthieu Perreira

Da Silva

Patrick Le Callet

HDR-VQM: An Objective Quality Measure for High Dynamic Range Video

Keywords: High Dynamic Range (HDR) video quality, objective quality, spatio-temporal analysis

High Dynamic Range (HDR) signals fundamentally differ from the traditional low dynamic range (LDR) ones in that pixels are related (proportional) to the physical luminance in the scene (i.e. scenereferred). For that reason, the existing LDR video quality measurement methods may not be directly used for assessing quality in HDR videos. To address that, we present an objective HDR video quality measure (HDR-VQM) based on signal pre-processing, transformation, and subsequent frequency based decomposition. Video quality is then computed based on a spatio-temporal analysis that relates to human eye fixation behavior during video viewing. Consequently, the proposed method does not involve expensive computations related to explicit motion analysis in the HDR video signal, and is therefore computationally tractable. We also verified its prediction performance on a comprehensive, in-house subjective HDR video database with 90 sequences, and it was found to be better than some of the existing methods in terms of correlation with subjective scores (for both across sequence and per sequence cases).

A software implementation of the proposed scheme is also made publicly available for free download and use.

I. INTRODUCTION

The advent of better technologies in the field of visual signal capture and processing has fueled a paradigm shift in todays' multimedia communication systems. As a result, the notion of network-centric Quality of Service (QoS) in multimedia systems is being extended by relying on the concept of Quality of Experience (QoE) [START_REF] Callet | Qualinet white paper on definitions of quality of experience[END_REF]. In this quest of increasing the immersive video experience and the overall QoE of the end user, newer technologies such as 3D, ultra high definition (UHD) and, more recently, High Dynamic Range (HDR) imaging have gained prominence within the multimedia signal processing community. HDR in particular has attracted attention since it in a way revisits the way we capture and display natural scenes. This is motivated by the fact that natural scenes often exhibit large ranges of illumination values. However, such high luminance values often exceed the capabilities of the traditional low dynamic range (LDR) capturing and display devices. Consequently, it is not possible to properly expose the dark and the bright areas simultaneously in one image (or video) during capture. This may lead to overexposure (saturated pixels that are fully white) and/or under-exposure (very dark or noisy pixels as sensor's response falls below its noise threshold). In both cases, visual information is either lost or altered. HDR imaging focuses on minimizing such losses and therefore aims at improving the quality of the displayed pixels by incorporating higher contrast and luminance.

As a result, HDR imaging has attracted attention from both academia and industry, and there has been interest and effort to develop tools/algorithms for HDR video processing [START_REF] Banterle | Advanced High Dynamic Range Imaging: Theory and Practice[END_REF]. For instance, there have been recent efforts within the Moving Picture Experts Group (MPEG) for extending High Efficiency Video Coding (HEVC) to HDR. Likewise, the JPEG has announced extensions that will feature the original JPEG standard with support for HDR image compression.

However, there is lack of such effort to quantify and measure the impact of such tools on HDR video quality using both subjective and objective approaches. The issue assumes further significance given that most of the existing objective methods may not be directly applicable for HDR quality estimation [START_REF] Narwaria | Tone mapping-based high-dynamic-range image compression: study of optimization criterion and perceptual quality[END_REF], [START_REF] Valenzise | Performance evaluation of objective quality metrics for hdr image compression[END_REF] and [START_REF] Narwaria | On improving the pooling in HDR-VDP-2 towards better hdr perceptual quality assessment[END_REF] (note that these studies only deal with HDR images and not video). It is therefore important to develop objective methods for HDR video quality measurement and benchmark their performance against subjective ground truth.

With regards to visual quality measurement, both subjective and objective approaches can be used. The former involves the use of human subjects to judge and rate the quality of the test stimuli. With appropriate laboratory conditions and a sufficiently large subject panel, it remains the most accurate method. The latter quality assessment method employs a computational (mathematical) model to provide estimates of the subjective video quality. While such objective models may not mimic subjective opinions accurately in a general scenario, they can December 1, 2014 DRAFT be reasonably effective in specific conditions/applications. Hence, they can be an important tool towards automating the testing and standardization of HDR video processing algorithms such as HDR video compression, post-processing, inverse video tone mapping etc. especially when subjective tests may not be feasible. In light of this, we present a computationally tractable HDR video quality estimation method based on HDR signal transformation and subsequent analysis of spatio-temporal segments, and also verify its prediction performance based on a test bed of 90 subjectively rated compressed HDR video sequences. To the best of our knowledge, our study is amongst the first few efforts towards the design and verification of an objective quality measurement method for HDR video, and is therefore of interest to the video signal processing community both from subjective and objective quality view points.

II. BACKGROUND

Humans perceive the outside visual world through the interaction between luminance (measured in candela per square meter cd/m 2 ) and the eyes. Luminance first passes through the cornea, a transparent membrane. Then it enters the pupil, an aperture that is modified by the iris, a muscular diaphragm. Subsequently, light is refracted by the lens and hits the photoreceptors in the retina. There are two types of photoreceptors: cones and rods. The cones are located mostly in the fovea. They are more sensitive at luminance levels between 10 -2 cd/m 2 to 10 8 cd/m 2 (referred to as the photopic or daylight vision) [START_REF] Mather | Foundations of Perception[END_REF]. Further, color vision is due to three types of cones: short, middle and long wavelength cones. The rods, on the other hand, are sensitive at luminance levels between 10 -6 cd/m 2 to 10 cd/m 2 (scotopic or night vision). The rods are more sensitive than cones but do not provide color vision.

Pertaining to the luminance levels found in the real world, direct sunlight at noon can be of the order in excess of 10 7 cd/m 2 while a starlit night in the range of 10 -1 cd/m 2 . This corresponds to more than 8 orders of magnitude. With regards to human eyes, their dynamic range depends on the time allowed to adjust or adapt to the given luminance levels. Due to the presence of rods and cones, human eyes have a remarkable ability to adjust to varying luminance levels, both dynamically (i.e. instantaneous) and over a period of time (i.e. adaptation time). Given sufficient adaptation time, the dynamic range of human eyes is about 13 orders of magnitude. However, without adaptation, the instantaneous human vision range is smaller and they are capable of dynamically adjusting so that a person can see about 5 orders of magnitude throughout the HDR imaging technologies therefore aim to overcome the inadequacies of the LDR capture and display technologies via better video signal capture, representation and display, so that the dynamic range of the video can better match the instantaneous range of the eye. In particular, the major distinguishing factor of HDR imaging (in comparison to the traditional LDR one) is its focus on capturing and displaying scenes as natively (i.e. how they appear in the real world) as possible by considering physical luminance of the scene in question. Two important points should, however, be mentioned at the very outset. First, it may be emphasized that in HDR imaging one usually deals with proportional (and not absolute) luminance values. More specifically, unless there is a prior and accurate camera calibration, luminance values in an HDR video file represent the real world luminance upto an unknown scale 1 . This, nonetheless, is sufficient for most purposes. Secondly, the HDR displays currently available cannot display luminance beyond the specified limit, given the hardware limitations. This necessitates a preprocessing step for both subjective and objective HDR video quality measurement, as elaborated further in the next section. Despite the two mentioned caveats, HDR imaging can improve the viewer experience significantly as compared to LDR2 imaging and, thus an active research area. As already mentioned in the introduction, this paper seeks to address the issue of objective video quality measurement for HDR video. This is in light of the need to develop and validate such algorithms to objectively evaluate the perceptual impact of various HDR video processing tools on video quality. We describe the details of the method and verify its performance in the following sections.

III. THE PROPOSED OBJECTIVE HDR VIDEO QUALITY MEASURE

A block diagram outlining the major steps in the proposed HDR-VQM is shown in Figure 1. It takes as input the source and the distorted HDR video sequences. Note that throughout the paper we use the notation src (source) and hrc (hypothetical reference circuit) to respectively denote reference and distorted video sequences. As shown in the figure, the first two steps are meant to convert the native input luminance to perceived luminance. These can therefore be seen as pre-processing steps. Next, the impact of distortions is analyzed by comparing the different frequency and orientation subbands in src and hrc. The last step is that of error pooling which is achieved via spatio-temporal processing of the subband errors. This comprises of short term temporal pooling, spatial pooling and finally, a long term pooling. A separate block diagram explaining the error pooling in HDR-VQM is shown in Figure 3. In the following sub-sections, we elaborate on the various steps in HDR-VQM.

December 1, 2014 DRAFT

A. From native HDR values to emitted luminance: modeling the display processing

We begin with two observations with regard to HDR video signal representation. First, as emphasized in the previous section, native HDR signal values are, in general, only proportional to the actual scene luminance and not equal to it. Therefore, the exact scene luminance at each pixel location will be, generally, unknown. Second, since the maximum luminance values of real-world scenes can be vastly different, the concept of a fixed maximum (or the white point)

does not exist for HDR values. In view of these two observations, HDR video signals must be interpreted based on the display. Thus, their values should be re-calibrated according to the characteristics of the HDR display used to view them. This is unlike the case of LDR video where the format is more standardized (eg. for 8-bit representation, the maximum value will be 255 which would be mapped to the peak display luminance that does not typically exceed 500 cd/m 2 ). With regard to HDR displays, the inherent hardware limitations will impose a limit on the maximum luminance that can be displayed. Thus, a pre-processing of the HDR video signal is always required in order that the pre-defined maximum luminance point is not exceeded. Since this can affect distortion visibility, the said pre-processing for the transition from native HDR values (denoted as N src , N hrc in Figure 1), to the emitted luminance (denoted as E src , E hrc in Figure 1) is therefore an important step in the objective method design.

While one can adopt different strategies (from simple ones like linear scaling to more sophisticated ones) for the said display based pre-processing, this is not the main focus of the work.

However, for the purpose of the method described in this paper, it is sufficient to highlight that in the general case, it is important that the characteristics of the HDR display are taken into account and the HDR video transformed (pre-processed) accordingly i.e. N src → E src and N hrc → E hrc , for objective HDR video quality estimation. The specific pre-processing that we employed in our experiments in discussed in Section IV C.

B. Transformation from emitted to perceived luminance

The second step in the design of HDR-VQM concerns the transformation of the emitted luminance to perceived luminance i.e. E src → P src and E hrc → P hrc as indicated in Figure 1.

This is required since there exists a non-linear relationship between the perceived and emitted luminance values given the response of the human visual system (HVS) to different luminance levels. An implication of such non-linearity is that the changes introduced by an HDR video December 1, 2014 DRAFT processing algorithm in the emitted luminance may not have a direct correspondence to the actual modification of visual quality. This is different from the case of LDR representation in which the pixel values are typically gamma encoded. Thus, LDR video encodes information that is nonlinearly (the non-linearity arising due to the gamma curve) related to the scene luminance. As a result of such non-linear representation, the changes in LDR pixel values can be approximately linearly related to the actual change perceived by the HVS. Due to this, many LDR image/video quality measurement methods directly employ the said gamma encoded pixel values as input and assume that changes in LDR pixels (or changes in features extracted from those pixels) due to distortion can quantify quality degradation (the reference video is always assumed to be of perfect quality). Therefore, to achieve a similar functionality as the LDR domain, the said non-linearity of the HVS to the emitted luminance should be taken into account for objective HDR video quality evaluation. In this way, the input values to the objective HDR video quality estimator would be expected to be approximately linearly related to the changes induced due to distortions.

To that end, a simple solution is to employ the logarithmic transformation which can approximate the saturation effect. However, the HVS is known to exhibit an approximate logarithmic response only for higher luminance (values in typically in the range 1000 -10000 cd/m 2 ), and is more sensitive at lower luminance values [START_REF] Mantiuk | Lossy compression of high dynamic range images and video[END_REF]. We therefore explored the perceptually uniform December 1, 2014 DRAFT (PU) encoding proposed in [START_REF] Aydin | Extending quality metrics to full luminance range images[END_REF] which can transform luminance values in the range from 10 -5 to 10 8 cd/m 2 into approximately perceptually uniform code values. In order to compare the two mentioned transformations, we plot in Figure 2, the respective responses to an input which is in the range from 1 -10000 cd/m 2 . For a closer look, we have plotted the responses for luminance in the range 1 -200 cd/m 2 and above 1000 cd/m 2 . We notice from Figure 2(a) that the response of PU encoding is relatively more linear at lower luminance as compared to the logarithmic one. To further quantify this, it was found that the linear correlation between the original and transformed signals was 0.9334 for PU encoding and 0.9071 for logarithmic, for the range between 1 -200 cd/m 2 . On the other hand, both PU and logarithmic curves have a similar response for higher luminance values (above 1000 cd/m 2 ) as indicated in Figure 2(b). In this case, the linear correlations were 0.8703 and 0.8763 respectively for PU and logarithmic transformation. Thus, PU encoding can better approximate the response of HVS which is approximately linear at lower luminance and increasingly logarithmic for higher luminance values. Due to this, PU encoding is expected to better model the underlying non-linear relationship between HVS's response and emitted luminance. The study on HDR video compression in [START_REF] Koz | Optimized tone mapping with perceptually uniform luminance values for backward-compatible high dynamic range video compression[END_REF] provides further evidence of this where it was demonstrated that PU encoding resulted in better coding efficiency as compared to the logarithmic transformation. From objective image quality assessment view point also, PU encoding has been shown [START_REF] Valenzise | Performance evaluation of objective quality metrics for hdr image compression[END_REF] to be beneficial. Lastly, as described in the original paper [START_REF] Aydin | Extending quality metrics to full luminance range images[END_REF], PU encoding has been implemented as a look-up table operation, and therefore does not substantially increase the computational overhead. All these features render PU encoding a reasonably accurate and efficient alternative for transforming the emitted luminance values to the perceived ones.

C. Computation of subband error signal

The proposed HDR-VQM is based on spatio-temporal analysis of an error video whose frames denote the localized perceptual error between a source and distorted video. We first describe the steps to obtain the subband error signal and then present the details of the spatio-temporal processing.

We employed log-Gabor filters, introduced in [START_REF] Field | Relations between the statistics of natural images and the response properties of cortical cells[END_REF], to calculate the perceptual error at different scales and orientations. We note that log-Gabor filters have been widely used in image analysis and are a reasonable choice of features to compare intrinsic characteristics of natural scenes.

In our approach, the log-Gabor filters were used in the frequency domain and can be defined Video frames in the perceived luminance domain (i.e P src and P hrc ) were decomposed into a set of subbands by computing the inverse DFT of the product of the frames's DFT with frequency domain filter defined in [START_REF] Callet | Qualinet white paper on definitions of quality of experience[END_REF]. We denote the resulting subband values as {l

H s,o (f, θ) = exp(- log(f /f s ) 2 2(log(σ s /f s ) 2 ) × exp(- (θ -θ o ) 2 2σ 2 o ) (1)
(src)
t,s,o } and {l (hrc) t,s,o } respectively. Here, s = 1, 2, ..., N scale (the total number of scales), o = 1, 2, ..., N orient (the total number of orientations) and t = 1, 2...F (the total number of frames in the sequence). The next step is to compute the error in the subband values for each frame at different scale and orientation levels. To that end, we chose the following simple and bounded measure (similar to the one used in [START_REF] Wang | Multiscale structural similarity for image quality assessment[END_REF]):

Error t,s,o = 2 . l (src) t,s,o . l (hrc) t,s,o + k {l (src) t,s,o } 2 + {l (hrc) t,s,o } 2 + k (2)
Here k (a small constant) is added to avoid division by zero. We can then obtain the total error at each pixel in each video frame by pooling across scales and orientations. While more sophisticated methods such as those based on contrast sensitivity function (CSF) can be adopted for this purpose, a possible bottleneck is that of computing the desired CSF accurately (especially the one which may be applicable for both near-threshold and supra-threshold distortions). Therefore, in the current formulation, we limited the scope of application of the proposed HDR-VQM to supra-threshold distortions and chose to assign equal weighting as follows:

Error t = 1 N scale × N orient N scale s=1 N orient o=1 Error t,s,o (3)
Error t , which is a 2D distortion map, represents the error in each frame t due to processing of a source sequence by an HRC and the thus, the error video can be represented as Error video = {Error t } F t=1 . It can be noted that the Error video helps to quantify the effect of local distortions by assessing their impact across frequency and orientation. We can then exploit it further via spatiotemporal analysis in order to calculate short term quality in a spatially and temporally localized neighborhood, and subsequently obtain the overall HDR video quality score. We elaborate on this in the next sub-section. Stated differently, the impact of distortions introduced in video frames will not be limited just to the spatial dimension but will rather manifest spatio-temporally. In the light of this, a reasonable strategy for objective video quality measurement is by analyzing the video in a spatio-temporal (ST) dimension [START_REF] Pinson | A new standardized method for objectively measuring video quality[END_REF], [START_REF] Narwaria | Low-complexity video quality assessment using temporal quality variations[END_REF], [START_REF] Ninassi | Considering temporal variations of spatial visual distortions in video quality assessment[END_REF], so that the impact of distortions can be localized along both spatial and temporal axes. To incorporate this in HDR-VQM, we first obtained the error video

Error video = {Error t } F t=1 for the given pair of source and distorted HDR video. Then, the error video was divided into non-overlapping short-term ST tubes defined by a 3-dimensional region with x horizontal, y vertical and the z temporal data points i.e. a cuboid with dimensions

x × y × z, as illustrated in Figure 3. Note that the former two define the spatial axes while the latter determines the temporal resolution to be considered when evaluating quality at the level of ST tubes. The values of x and y together define the area of the fixated region. Therefore, these can be computed by taking into account the viewing distance, the central angle of the visual field in the fovea and the display resolution. On the other hand, a good range of z can be determined by considering the average fixation duration when viewing a video. While this can vary due to content and/or distortions, studies (for eg. [START_REF] Meur | Overt visual attention for free-viewing and quality assessment tasks: Impact of the regions of interest on a video quality metric[END_REF]) related to the analysis of eye-movement during video viewing indicate that values in the range of 300 -500 ms can be a reasonable choice.

                . . . . .

Short-term quality scores

Overall quality

Long term temporal pooling

Standard deviation

Subband errors

Spatial pooling

Fig. 3: Error pooling in HDR-VQM.

1) Short term temporal pooling: The aim of short term temporal pooling is to pool or fuse the data in local spatio-temporal neighborhoods (defined by ST regions). Keeping in mind that the goal is to characterize the effect of spatial distortions over short term duration (equal to fixation time), we computed the standard deviation of each ST tube in order to obtain a spatio-temporal subband error frame ST v,ts (as visually exemplified in Figure 3) where v represents the spatial co-ordinates and t s being the index of resulting spatio-temporal frames. By this definition, a video sequence with lower visual quality will have higher localized standard deviations while these will decrease as the signal quality improves. Thus, ST v,ts help to quantify signal coherence level in local neighborhoods. Also note that in our case, the error video was analyzed based on non-overlapping ST tubes. Thus we will have t s = 1, 2, ..., F/z. The final step is to perform spatial and long term temporal pooling to obtain the global video quality score.

2) Spatial and Long term temporal pooling: To obtain an overall video quality score that can quantify the level of annoyance in the video sequence, the local errors represented by spatiotemporal subband error frame ST v,ts are pooled further in two stages: (a) spatial pooling to generate a time series of short term quality scores, (b) long term temporal pooling to fuse short term quality scores in to a single number denoting the overall annoyance level. These stages are based on the premise that humans evaluate the overall video quality based on continuous assessments of the impact of short term errors or annoyance they came across while viewing the video. Therefore, we first perform spatial pooling on spatio-temporal error frames ST v,ts in order to obtain the short-term quality scores, as illustrated in Figure 3. We note that such short term December 1, 2014 DRAFT quality scores can be useful in providing information about the distortions temporally. Finally, a long term pooling is applied to compute the overall video quality score. We therefore use the following expression for HDR-VQM:

HDR-VQM = 1 |t s L p | × |v L p | ts Lp v Lp ST v,ts (4)
where L p denotes the set with lowest p% values, |.| stands for cardinality of the set. The reader will notice that both short term spatial and long term temporal pooling have been performed

over the lowest p% values. This is because the HVS does not process necessarily visual data in its entirety and makes certain choices to minimize the amount of data analyzed. It is, of course non-trivial to realize and integrate such exact HVS mechanisms into an objective method. In our case, we therefore employ the simple approach of percentile pooling keeping in mind that we are dealing with supra threshold distortions, and quality judgment would be based on how much the signal has been distorted (i.e. for a perfect quality video HDR-VQM will be zero). Finally, it is straightforward to use HDR-VQM to compute objective HDR image quality (obviously there will be no temporal index in this case).

IV. HDR VIDEO DATASET

To the best of our knowledge there are currently no publicly available subjectively annotated HDR video datasets dealing with the issue of visual quality. Therefore, for verifying the prediction performance of HDR-VQM and other objective methods, an in-house and comprehensive HDR video dataset was used. This section provides a brief description of the dataset.

A. Test material preparation

The dataset used 10 source HDR video sequences 3 . The frame resolution was full HD (1920 by 1080 pixels) and the frame rate was 25 frames per second (fps). The spatial versus temporal information measures (computed on tone mapped version of video frames) for each source sequence is shown in Figure 4. The source sequences were compressed at different bit rates to obtain the test stimuli. To that end, we employed a backward-compatible (in our context In general, any backward-compatible HDR compression scheme comprises [START_REF] Narwaria | High dynamic range visual quality of experience measurement: Challenges and perspectives[END_REF] of 3 steps: (a) forward tone mapping in order to convert HDR video to LDR (8-bit precision), (b) compression and decompression of the LDR video by a standard LDR video compression method, (c) inverse tone mapping of the decoded (decompressbed) LDR bit stream to reconstruct HDR video.The specific method that we used is described in [START_REF] Koz | Optimized tone mapping with perceptually uniform luminance values for backward-compatible high dynamic range video compression[END_REF]. It is not discussed here but the reader is encouraged to refer to [START_REF] Koz | Optimized tone mapping with perceptually uniform luminance values for backward-compatible high dynamic range video compression[END_REF] for details. The LDR video was encoded and decoded using H.264/AVC at different bit rates. For the subjective viewing tests, we selected 8 bit rates (by varying the quantization parameter QP) such that the resultant HDR video quality covered the entire rating scale, i.e., from excellent (rating 5) to bad (rating 1). With the inclusion of the source sequences, we obtained a total of 90 HDR video sequences (10 × 8 bit rates + 10) to be rated by the subjects.

B. Rating methodology

Our study involved 25 paid observers who were not expert in image or video processing. They were seated in a standardized room conforming to the International Telecommunication Union Recommendation (ITU-R) BT500-11 recommendations [START_REF]Methodology for the subjective assessment of the quality of television pictures[END_REF]. Prior to the test, observers were screened for visual acuity by using a Monoyer optometric table and for normal color vision by using Ishiharas tables. All of them had normal or corrected to normal visual acuity and normal color perception. For rating the test stimuli, we adopted the absolute category rating with hidden reference (ACR-HR), which is one of the rating methods recommended by the ITU December 1, 2014 DRAFT in Rec. ITU-T P.910 [START_REF]Subjective video quality assessment methods for multimedia applications[END_REF]. The ACR-HR is a category judgment method where the test stimuli are presented one at a time and rated independently on a category scale. The rating method also includes the source sequences (i.e. undistorted) to be shown as any other test stimulus without informing the observers. This is therefore termed a hidden reference condition, and the advantage is that it implicitly encourages the observers to rate video quality and not fidelity since there is no reference to compare with. To quantify the video quality, a five-level scale is used: 5 (Excellent), 4 (Good), 3 (Fair), 2 (Poor) and 1 (Bad). We chose a discrete five-level scale because it is more suitable for naive (non-experts in image processing) observers, and it is easier for them to quantify the quality based on an adjective ('Excellent', 'Good', 'Fair', 'Poor' and 'Bad'). We also employed post-experiment screening of the subjects in order to reject any outliers in accordance with the Video Quality Experts Group (VQEG) multimedia test plan [START_REF]Final report from the video quality experts group on the validation of objective quality metrics for video quality assessment[END_REF],

and in our case no observer was rejected.

C. Display

For displaying the HDR video sequences, SIM2 Solar47 HDR display was used which has a maximum displayable luminance of 4000 cd/m 2 . Since the HDR display luminance is relatively much higher as compared to the conventional display devices, we need much higher room illumination in order to reduce the visual discomfort of the subjects. In our study this was set to 200 cd/m 2 as it provided comfortable viewing conditions for the observers [START_REF]Tone mapping based HDR compression: Does it affect visual experience?[END_REF]. The viewing distance was set to three times the height of the screen (active part), i.e., approximately 178 cm.

It may be recalled from Section III A that we need to pre-process the HDR video signal in order that its luminance range fits that of the display i.e. N src → E src and N hrc → E hrc . With regard to the said pre-processing step, the most straightforward way is the use of maximum normalization i.e. scaling the values in each video frame independently by the maximum luminance value in that frame. We however observed that this approach suffers from at least two drawbacks.

First, because only a single luminance value (maximum) is used, it is susceptible to outliers.

Second, we also observed that it tends to reduce the overall luminance coherence of the HDR video due to the local (i.e at frame level) normalization. To ameliorate these two issues, we opted for a temporally more coherent strategy and the normalization factor was determined as the maximum of the mean of top 5% luminance values of all the frames in an HDR video sequence. Specifically, we first computed a vector M T 5 whose elements were the mean of top December 1, 2014 DRAFT 5% luminance values in each HDR video frame i.e. [START_REF] Narwaria | On improving the pooling in HDR-VDP-2 towards better hdr perceptual quality assessment[END_REF] where N denotes the native HDR values at spatial location v for frame t (F is the total number of frames), T 5 denotes the set with highest 5% luminance values in the frame. Then, the native HDR values N were converted to emitted luminance values E as

M T 5 =    1 |v T 5 | v T 5 N v,t    t=1,2...F (
E = N × 179 max(M T 5 ) (6)
where the multiplication factor of 179 is the luminous efficacy of equal energy white light that is defined and used by the Radiance file format (RGBE) for the conversion to actual luminance value. Finally, a clipping function was applied to limit the E values in the range defined by the black point (lowest displayable luminance) and the maximum displayable luminance (obviously both will depend on the display characteristics).

V. EXPERIMENTAL RESULTS

Before we compute the experimental results, it is necessary to determine the parameter values in HDR-VQM. First, to compute the values of x and y, we assume the central angle of the visual field in the fovea to be 2 • [START_REF] Green | Regional variations in the visual acuity for interference fringes on the retina[END_REF]. Then, we can define a quantity W which denotes the length of the fixated window in terms of number of pixels and can be computed as

W = tan 2 • × V × R/D A (7)
where V is the viewing distance in cm., R is the display resolution and D A is the display area. In our case, V = 178 cm, R = 1080 × 1920 pixels and D A ≈ 6100 cm 2 . Plugging these values in to [START_REF] Mather | Foundations of Perception[END_REF] gives W ≈ 115. To reduce the computational effort, HDR-VQM was run on down sampled (by a factor of 2) video frames, and hence the approximate length of the fixated window will be W/2 ≈ 58. Thus, we set x = y = 64 pixels in order to be nearest to a more standard block size.

To determine z, we assumed a fixation duration of 400 ms and with a frame rate of 25 fps, we will have z = 10 frames. The number of scales and orientations used were 5 and 4, respectively i.e. N scale = 5 and N orient = 4.

December 1, 2014 DRAFT

A. Correlation based comparisons

The first set of experimental results are reported in terms of two criteria: Pearson linear correlation coefficient C p (for prediction accuracy) and Spearman rank order correlation coefficient C s (for monotonicity), between the subjective score and the objective prediction. The former depends on the non-linear mapping between objective and subjective scores (we therefore employed a four-parameter monotonic logistic mapping between the objective outputs and the subjective quality ratings [START_REF]Final report from the video quality experts group on the validation of objective quality metrics for video quality assessment[END_REF]) while the latter is independent of any such non-linearity. We compared the performance of HDR-VQM with a few popular LDR methods including PSNR and multi-scale SSIM [START_REF] Wang | Multiscale structural similarity for image quality assessment[END_REF]. The input to all these methods were the perceived luminance values P src and P hrc and hence we refer to them as P-PSNR and P-SSIM. In addition, we considered two other methods which take as input the emitted luminance values E src and E hrc . The first one is the HDR-VDP-2 originally proposed in [START_REF] Mantiuk | HDR-VDP-2: A calibrated visual metric for visibility and quality predictions in all luminance conditions[END_REF], and we employed its re-calibrated version reported in [START_REF] Narwaria | Calibrated HDR-VDP-2 for objective quality assessment of high dynamic range and standard images[END_REF]. The second method is the relative PSNR (RPSNR) which employs a variant of the traditional mean squared error, MSE, in that it normalizes the error by the magnitude of luminance at each point in order to account for reduced sensitivity at high luminance. It can be defined as

RP SN R = -10 log 10 1 N pixels i,j (E src i,j -E hrc i,j ) 2 E 2 src i,j + E 2 hrc i,j (8)
where i, j and N pixels respectively denote the pixel index and the total number of pixels in the source and distorted frames.

Since we are dealing with full-reference video quality estimation, we computed the correlations using only the 80 distorted sequences (i.e. 80 test conditions), and these are shown in Figure 5. The results for across sequences (i.e. with all the 80 sequences) are shown in Figure 5(a).

One can observe the HDR-VQM achieves relatively higher prediction accuracy in comparison to the other methods. It is also interesting to point out the proposed HDR-VQM, P-PSNR, and P-SSIM compute quality based on perceived luminance. The better performance of HDR-VQM relative to these methods therefore indicates the added value of taking into account frequency and orientation information. We also carried out analysis based on an F-test to investigate the significance of the obtained results from a statistical view point, and those results are represented graphically in Figure 5(b). In this, the F values were computed for the different methods with respect to HDR-VQM (the residuals were verified to be approximately Gaussian which is an December 1, 2014 DRAFT points to be fitted is small), for per source sequence are indicated in Figure 6 from which we note that simpler methods like P-PSNR and MRSE tend to perform better (although the performance is still not consistent for each source) as compared to across sequence. But, in general, HDR-VQM is competitive or better in majority of cases.

To further explain why simpler methods like RPSNR and P-PSNR achieve relatively lower correlations in case of across sequence in comparison to the case of per sequence, the scatter plots for different methods are shown in Figure 7. In this, the x-axis denotes the objective scores while the y-axis indicates the MOS. We can see for instance in Figure 7(a) that while the RPSNR values per source are more linearly related to the MOS, they exhibit a large scatter due to the curves being shifted for each source. As a result, for similar MOS values across sequences, the corresponding RPSNR values can be quite different. This decreases the overall correlations.

On the other hand, the HDR-VQM, while not perfect, exhibits less scatter across sequences indicating its ability to better distinguish between quality levels of video sequences from across different sources. To illustrate this further, we take two specific conditions for src1 and src6.

One can see that for RPSNR achieves quite high correlations (in both these cases it is higher than 0.96) for both these source sequences. Consider the conditions: (a) src1 encoded at the lowest bit-rate (highest QP), (b) src6 encoded at the highest bit-rate (lowest QP). The RPSNR value for the first condition was 32.70 dB while the corresponding subjective score was 1.04.

On the other hand, for the second condition, the RPSNR was 28.54 dB with the subjective score for this condition being 3.92. Thus, just looking at RPSNR values can lead to the conclusion that the HDR video in first condition has higher quality than the one in the second condition, which is not the case according to subjective opinion. On the other hand, the HDR-VQM values for the two conditions (respectively 0.1795 and 0.01, recall smaller HDR-VQM implies higher quality) are more in line with subjective opinion. We also wish to stress that this example is only

B. Outlier ratio analysis

Outlier ratio analysis is another approach to evaluate objective methods for their prediction accuracy. It is different from the usual correlation based comparisons in that it does not penalize if the prediction error is within the limit of uncertainty in the subjective rating process. Particularly, it can be very useful in applications such as video compression where one is generally interested in the rate distortion (RD) behavior of objective methods i.e. how the objective visual quality varies with bit rates for different source sequences and to what extent that compares with the subjective video quality. To carry out the outlier ratio analysis, we computed the number of outliers from different objective methods for the 80 conditions used in our HDR video dataset.

To define an outlier, we use the fact that the subjective rating process is always associated with uncertainty due to inter-observer differences between the perceived quality of the same stimuli.

Consequently, the actual subjective video quality can vary between two limits which can be, for instance, determined based on confidence intervals. Therefore, we first computed the absolute prediction error between the subjective MOS and logistically transformed objective scores for each of the 80 test conditions. For each objective method, if the said error was greater than twice the 95% confidence interval associated with the MOS, then that objective method was deemed as an outlier for the given condition. Formally, if |M OS c -OM (logistic) c | > 2CI c then the objective prediction from the given objective method OM will be deemed as an outlier for condition c (c = 1, 2, ...80). Here M OS c , OM (logistic) c and CI c respectively denote the subjective score, the logistically transformed value from the method OM and the associated 95% confidence interval, for condition c. The resulting number of outliers for each objective method is shown in Table I along the percentage of outliers for the 80 test conditions.

We find that HDR-VQM has the least number of outliers (22%). Also notice that P-SSIM, which was second in terms of correlation results in Figure 5(a), has about 43% outliers which is almost double that of HDR-VQM. Thus, such outlier analysis provides additional insights

VI. DISCUSSION

The previous sections proposed and verified the performance of an objective HDR video quality estimator HDR-VQM. An important point worth re-iterating is that in light of limitations imposed in HDR display technologies, the HDR video signal must be pre-processed. This, in turn implies that HDR video quality can be affected by the type of pre-processing used as well as the maximum displayable luminance since these can affect distortion visibility. Thus, the role of a display model is more prominent in HDR, and objective quality assessment should consider this aspect. As opposed to this, quality measurement for the traditional LDR video signals does not usually require any specific display based pre-processing. By this, we do not imply that the display does not affect quality judgment in LDR domain, merely its effect is perhaps less prominent.

While the proposed HDR-VQM is reasonably accurate, it is certainly not without its limitations as is the case with any objective method. The reader will notice that HDR-VQM does not explicitly account for spatio-temporal masking that could play a role in quality judgment.

Therefore, in the current form, it is assumed that the employed measure of similarity is directly related to the change in video quality. We note that such an assumption is more reasonable for supra-threshold distortions (i.e. distortions clearly visible to the human eye) but may not always hold in case of near-threshold distortion levels where the impact of spatio-temporal masking may be more prominent. Also recall that in (3) we did not employ a more sophisticated weighting such as one based on CSF. Thus, in the current formulation, HDR-VQM may be more effective in case of supra-threshold distortions and we believe that it is important to make this distinction in order to define the scope of application. low computational complexity due to the fact that it does not explicitly extract motion information from the video. Rather, the focus is on exploiting basic video signal characteristics by resorting to spatio-temporal analysis which, in turn, is based on the idea that humans tend to judge video quality in local context, both from spatial and temporal view points. As a consequence, HDR-VQM also provides certain local spatio-temporal quality information that can be for instance useful as feedback for video codec optimization. While a formal computational complexity analysis of HDR-VQM is not the focus of this work, recall that in HDR-VQM we performed the filtering in the frequency domain. This allows us to exploit the efficiency of the Fast Fourier Transform (FFT) and inverse FFT whose complexity is O(M 2 logM ) where M is the frame size.

Further, Figure 8 provides the percentage of outliers and the relative computational complexity (expressed as the execution time realtive to RPSNR). Obviously, lower values for an objective method along both axes implies that it is better. We find that the relative execution time for HDR-VQM is reasonable considering the improvements (i.e. smallest % of outliers) in performance over other methods. The reader will also appreciate the fact that video quality judgment, in general, can depend on several extraneous factors (such as display type, viewing distance, ambient lighting conditions etc.) apart from the distortions themselves. In that regard, a notable feature of HDR-VQM is that it takes into account some of the mentioned factors such as the viewing distance, fixation duration and display resolution in computing the different parameters. This allows HDR-VQM to adapt to some of the physical factors that may affect subjective quality December 1, 2014 DRAFT judgment. Finally, HDR-VQM does not have any parameter that needs to be tuned/trained and hence does not require a priori information about the content or distortion.

VII. CONCLUDING THOUGHTS

HDR imaging is increasingly becoming popular in the multimedia signal processing community primarily as a tool towards enhancing the immersive video experience of the user. However, there are very few works that address the issue of assessing the impact of HDR video processing algorithms on the perceptual video quality both from subjective and objective angles. The study in this paper seeks to outline the first steps towards the design and verification of an objective HDR video quality estimator HDR-VQM. While objective video quality measurements cannot always replace subjective opinion, they can still be useful in specific HDR video processing applications where subjective studies may be infeasible (eg. real-time video streaming, video encoding etc.).

To that extent and within the scope of its application, HDR-VQM is a reasonable objective tool for HDR video quality measurement. To enable others to use the proposed method as well as validate it independently, a software implementation will soon be made available online for free download and use. The immediate future work will ensue further refinement of the presented method in view of some of the mentioned limitations as well as further validation with larger HDR video datasets.

Fig. 1 :

 1 Fig. 1: Block diagram of the proposed HDR-VQM.

Fig. 2 :

 2 Fig. 2: Comparison of responses for two transformation functions in two different ranges of luminance, (a) 1 -200 cd/m 2 , (b) 1000 -10000 cd/m 2 . Figure best viewed in color.

  where H s,o is the filter denoted by spatial scale index s and orientation index o, f s denotes the normalized center frequency of the scale, θ is the orientation, σ s defines the radial bandwidth B in octaves with B = 2 2/log(2) * |log(σ s /f s )|, θ o represents the center orientation of the filter, and σ o defines the angular bandwidth ∆Ω = 2σ o 2log(2).

D

  . From spatio-temporal subband errors to overall video quality: The Pooling step Video signals propagate information along both spatial and temporal dimensions. However, due to visual acuity limitations of the eye, humans fixate their attention to local regions when viewing a video because only a small area of the eye retina, generally referred to as fovea, has a high visual acuity. As mentioned in Section II, this is due to higher density of photo receptor cells cones present in the fovea. Consequently, human eyes have to rapidly shift their gaze (the time between such movements is the fixation duration) to bring localized regions of the visual signal into the fovea field. Thus, humans tend to judge video quality in local context both spatially and temporally, and determine the overall video quality based on those assessments.

Fig. 4 :

 4 Fig. 4: Spatial and temporal information plot.

Fig. 5 :

 5 Fig. 5: Numerical results, (a) C p and C s for all 80 distorted sequences, (b) F-test results.

Figure

  Figure best viewed in color.

Fig. 6 :

 6 Fig. 6: C p values for per source (src) sequence (these values are computed without the logistic fitting function). Figure best viewed in color.

  meant to highlight specific potential problems with simpler methods like RPSNR. Of course, one should rely on correlation based comparisons and outlier ratio analysis (presented in the next subsection) to draw more general conclusions about the performance of different objective methods. December 1, 2014 DRAFT

Fig. 7 :

 7 Fig. 7: Scatter plots for different objective methods, (a) RPSNR, (b) P-PSNR, (c) P-SSIM, (d) HDR-VDP-2 and (e) HDR-VQM. Figure best viewed in color.

Fig. 8 :

 8 Fig. 8: % of outliers and the relative computational complexity (expressed as relative execution time with respect to RPSNR) for different methods. Figure best viewed in color.

  Since the typical frequency in video signals does not allow sufficient adaptation time, the dynamic vision range (5 orders of magnitude) is more relevant in the context of this paper as well as HDR video processing in general. However, typical digital imaging sensors (assuming the typical single exposure setting) and LDR displays are not capable of dealing with such large dynamic range present in the real world, and most of them (both capturing sensors and displays) can handle upto 3 orders of magnitude. Due to this limitation, the scenes captured and viewed via LDR technologies will have lower contrast (visual details are either saturated or noisy) and smaller color gamut than what the eyes can perceive. This in turn can decrease the immersive experience quotient of the end-user.

December 1, 2014 DRAFT entire range.

1

  Even with calibration, the HDR values represent real physical luminance with certain error. This is because the camera spectral sensitivity functions which relate scene radiance with captured RGB triplets cannot match the luminous efficiency function of the human visual system.

	N N	src hrc	Transformation into emitted luminance	src hrc E E	Transformation into perceived luminance	src P hrc P	Gabor filtering
							( , hrc , o s t l	)	l	) o src , , ( s t
	HDR				Short term temporal	Subband errors	Subband comparison, pooling across scale,
					pooling			orientation

-VQM src hrc Error pooling

	Long term temporal pooling	Spatial pooling

TABLE I :

 I Outlier ratio analysis for the 80 test conditions in the HDR video dataset.

		R-PSNR	P-PSNR	P-SSIM	HDR-VDP-2	HDR-VQM
	Number of Outliers	42	46	35	38	18
	% of Outliers	52%	57%	43%	47%	22%

  December 1, 2014 DRAFT into the behavior of different objective methods which is probably less apparent looking at just the correlation values. The main advantage of outlier analysis is that it helps to evaluate metric accuracy by taking into account the variability or uncertainty (expressed via 95% confidence intervals in our dataset) in subjective opinions, which are ignored in correlation based comparisons. Overall we find that HDR-VQM is reasonably accurate and more consistent for both across and per sequence cases as indicated by different tests (including correlation coefficients, statistical test and outlier analysis).

The authors are with IRCCyN/IVC group, University of Nantes, 44306, France e-mail: (manish.narwaria@univ-nantes.fr, matthieu.perreiradasilva@univ-nantes.fr, patrick.lecallet@univ-nantes.fr).December 1, 2014 DRAFT

The terms LDR and HDR are also sometimes respectively referred to as lower or standard dynamic range (SDR) and Higher Dynamic Range (to explicitly indicate that the range captured is only relatively higher than LDR but not the entire dynamic range present in a real scene). We, however, do away with such precise distinctions and always assume that the terms HDR and LDR are used in a relative context throughout this paper. December 1, 2014 DRAFT

December 1, 2014 DRAFT

These HDR video sequences were shot and made available as part of the NEVEx project FUI11, related to HDR video chain study. December 1, 2014 DRAFT

With regard to the strengths of the proposed method, one of the most prominent is its relatively December 1, 2014 DRAFT

ACKNOWLEDGMENT

The authors wish to thank Romuald Pepion for his help in generating the subjective test results used in this paper. This work has been supported by the NEVEx project FUI11 financed by the French government.


F Mazza

M P Da Silva

P Le Callet

I E J Heynderickx

What do you think of my picture?: Investigating factors of influence in profile images context perception

Keywords: portrait images, content perception, high level features, social bias, social networks, crowdsourcing HVEI XX

Multimedia quality assessment has been an important research topic during the last decades. The original focus on artifact visibility has been extended during the years to aspects as image aesthetics, interestingness and memorability. More recently, Fedorovskaya proposed the concept of 'image psychology': this concept focuses on additional quality dimensions related to human content processing. While these additional dimensions are very valuable in understanding preferences, it is very hard to define, isolate and measure their effect on quality. In this paper we continue our research on face pictures investigating which image factors influence context perception. We collected perceived fit of a set of images to various content categories. These categories were selected based on current typologies in social networks. Logistic regression was adopted to model category fit based on images features. In this model we used both low level and high level features, the latter focusing on complex features related to image content. In order to extract these high level features, we relied on crowdsourcing, since computer vision algorithms are not yet sufficiently accurate for the features we needed. Our results underline the importance of some high level content features, e.g. the dress of the portrayed person and scene setting, in categorizing image.

INTRODUCTION

Social networks are filled with extremely different pictures, both in terms of objective quality and content. Some of them are high quality shots, but many of them are simpler consumer produced ones. The impact that these pictures can produce is also very different. Even low quality shots may have a huge impact, as the message they convey may be sometimes more important than their inherent quality. For example, family photo galleries or shoots from photo reporters can be invaluable, no matter their technical quality. The latter is probably even more the case with portraits, where different photos of the same person can deliver very different messages. The latter is often overlooked by people: our first impressions do not only influence online interactions, but also real life communications. For example job recruiters may look for online profiles to complement their opinions, as demonstrated by Manant et Al. [START_REF] Manant | Do recruiters 'like' it? Online social networks and privacy in hiring: a pseudo-randomized experiment[END_REF] As stated by authors of, [START_REF] Joshi | Aesthetics and emotions in images[END_REF] it is important to consider image semantics where "human subjectivity" plays an important role. In this respect, current research related to image quality assessment seems to agree that considering only low level technical features is simply not enough, and so, we have to shift the attention towards high level features, more focused on "the domain of psychology". The latter concept is still broad and vague, but first attempts to outline it have been done by Fedorovskaya. [START_REF] Fedorovskaya | Subjective matters: from image quality to image psychology[END_REF] Following our previous work on portrait typologies, [START_REF] Mazza | Would you hire me? Selfie portrait images perception in a recruitment context[END_REF] in this paper we investigate which image features influence portraits' perception, where we more particularly assess the context to which the portrait is perceived to belong to. Portraits can suit different contexts and needs; for example, a portrait can fit well as a social network profile picture, but then may not fit a resume picture at all. Given previous considerations, we consider both low level and high level features, since we believe that the latter category greatly influences the evaluation of a portrait. Portrait images have been studied in different fields. Computer vision research focused on face features as input in machine learning algorithms to predict aesthetic assessment (as done by Li, 5 or more recently by Khan 6 ). Research in cognitive sciences tried to understand and modify image memorability. [START_REF] Khosla | Modifying the Memorability of Face Photographs[END_REF] Many of these approaches, however, adopted black box methods (i.e. ANN, SVM) and/or mathematical descriptors (i.e. HOG, GIST), losing interpretability of the results. [START_REF] Marchesotti | Discovering Beautiful Attributes for Aesthetic Image Analysis[END_REF] As our aim is to understand which interpretable features are influential, we preferred a white box approach. Hence, logistic regression is used to build a predictive model between portrait typology and image features, i.e., the final aim of our research.

METHODS

To evaluate which features influence portrait perception, we collected real online portraits related to three different contexts; namely to friends, work or dating purposes. We based this choice on current trends in social networks, nowadays focused on these three kinds of interactions (e.g., Facebook, Linkedin and Meetic). We then collected subjective assessments of the perceived context of each portrait. Successively we extracted both low and high level features from these portraits. The former ones were directly computed from pixel intensities (e.g., contrast), whereas the latter related to content interpretation were assessed subjectively. To have enough subjective evaluations of both the content category and the high level features, we opted for a large scale subjective campaign via crowdsourcing.

Portrait images

Many portrait databases exist online, but they are mainly dedicated to face detection-recognition, [START_REF] Huang | Labeled faces in the wild: A database forstudying face recognition in unconstrained environments[END_REF] or pose and expression estimation. [START_REF] Sim | The CMU Pose, Illumination, and Expression (PIE) database[END_REF] As such, they mainly focus on the face only (e.g., a neutral facial expression against a white background), or on full body portraits. In our research we were interested in face pictures, including a part of a person's torso and partly showing a background, as such portraits convey more complementary information regarding the context. Hence, we looked for amateur or semi-professional pictures, reflecting less formal and "posed" portraits -a characteristic that we suppose influence subjective context perception. For those reasons, we preferred to collect real online portraits from online networks and image sharing sites, collecting only publicly accessible images and taking care about licenses' restrictions * . We tried to select pictures related to the three chosen context categories: friends, work and dating purposes. While a huge number of portraits can be collected online, many problems arise, since many social networks do not allow -or strongly limit -pictures' disclosure. Facebook and Linkedin forbid using pictures without explicit permission of profile owners, and so, portraits of these databases weren't used in our experiment. Instead Twitter and Flickr offer APIs to access data. In the Flickr database we found portraits that we believe fit the categories friends and dating purposes. To gather work related portraits we adopted the website Elance.com, which is a work related social network for freelancers. In addition, we adopted 35 pictures from the LFW dataset, 9 suitable for the work related category. We avoided portraits of world famous people (e.g., world known politicians), since knowing their profession might influence the assessment of the fit to a category. A careful image selection was required. We manually checked content discarding all non portraits, non-adult subjects or inappropriate content. Extreme close-ups or too small pictures were also not selected, as content information was actually lacking. On the other hand, also pictures showing the context too clearly (e.g.,. showing signing a contract in a working environment) were discarded. To add more pictures to the ones we selected from the databases, we also used the best portraits we created for our previous experiment, [START_REF] Mazza | Would you hire me? Selfie portrait images perception in a recruitment context[END_REF] including both selfies and professional portraits. While it would have been possible to have a huge number of portraits, we limited the actual number for the experiment, since all pictures had to be assessed also on their high level features manually. Thus, as a compromise in terms of accuracy and reasonable time/cost for the experiment, we decided to use 216 collected pictures.

Crowdsourcing portrait evaluations

In order to gather a large amount of subjective evaluations we adopted crowdsourcing as in our previous work. [START_REF] Mazza | Would you hire me? Selfie portrait images perception in a recruitment context[END_REF] Crowdsourcing exploits the power of the web to outsource small tasks to people gathered online; it has already been investigated intensively and positively exploited in multimedia quality assessments. It is not the purpose of this work to dig into this technique; we refer the reader to our previous work, from which we adopted the same platform and framework. In the current study, participants were asked to express for each portrait to which context it fits best. They were given three options, referring to friends, work and dating purposes, as shown in Figure 1. We then also asked participants to indicate the second best category of their choice. Implicitly, we then obtained their third choice too. This approach allowed us to have a ranking of the three contexts for each image. A fourth category named "without faces" was added for reliability check purposes as explained later. Classification was done through a web browser simply with "drag and drop", as was also explained in the provided instructions. Before starting the actual test we provided participants with a small anonymous questionnaire. We collected the participants' job, nationality, birth year, education level and if they were new to this kind of experiments. This information will be used in future work. At the end of the session we provided participants the possibility to leave a comment, in order to have useful feedback to monitor our experiment. It is well known that crowdsourcing participants are much less committed than participants in laboratory environments. Thus, particular attention on experiment duration and price paid is required, otherwise people may withdraw prematurely the test. Preliminary experiments showed that a good compromise to maximize efficiency while avoiding participants' withdrawal is providing 25 images per session. This number corresponds approximately to a test of ten minutes. With our previous experience in crowdsourcing and considering current prices paid for similar work, we decided to pay each participation 0.50$. Still participants can provide unreliable evaluations, both in good or bad faith (in the latter case, for example, to collect easy money). To have some control on that, we included two reliability checks -a.k.a. honeypots. In case of failure in any of the two honeypots participants were excluded from analysis and not paid. The first honeypot was a demographic question; the birth year was set to 1880 by default. Users that did not pay attention to the questions, then reported an impossible age. The second honeypot was part of the picture categorization process. Two images of the Toyama database, [START_REF]Toyama MICT Image Quality Evaluation Database[END_REF] not showing any person, were included in each session. The instructions clearly stated to mark such pictures as 'non faces', but many participants instead labelled them as portraits. While there might be multiple causes for such errors (e.g., misunderstanding the instructions, poor English comprehension or poor attention) we considered participants falling in one of the honeypots as outliers.

High level features evaluation

Different research addresses the analysis of features to describe image content. In particular, the authors of 12 investigate semantic features, mainly related to the setting of the scene (i.e., indoor/outdoor and which scene). Particular focus regarding features of humans is given in, [START_REF] Isola | What makes an image memorable?[END_REF] where visibility, clothing and appearance are considered. Regarding low level features and image quality assessment, a huge amount of research is reported in literature, and reviewed in. [START_REF] Khan | Evaluating visual aesthetics in photographic portraiture[END_REF] The authors of 6 also adopted some of the proposed features to assess human portraits. Based on this literature we chose a subset of those features that we believed to be important in portrait context evaluation. We also added some high level features focused on the depicted context; in particular we included the depicted person's gender, the presence of glasses, his/her gaze direction and whether he/she was smiling in the picture. We didn't add emotion as a feature because we considered that smiling was a sufficient predictor to discriminate between emotions as in. [START_REF] Xue | Feature design for aesthetic inference on photos with faces[END_REF] 1. Many of our features are categorical variables, as head tilt and orientation (left,center,right) or scene setting (don't know/indoor/outdoor), and some of these are ordinal as subject size (from small to big). Computer vision based high level features extraction can be time consuming and error prone. As first step, we prefer to focus on features importance and therefore, we adopted crowdsourcing to manually label them. The advantage of this approach was twofold: (1) it greatly speeded up the process and avoided errors, and (2) it offered a subjective opinion for some cognitive features that might be perceived differently between people (e.g., where a portrait has been shot). For this purpose, we followed the same crowdsourcing strategy, changing only the task for the participants. They now were provided with a web interface to evaluate each feature for each picture (as shown in Figure 1(b)). For some features (e.g., subject profile side) we gave guidelines in the form of icons near the answer options or the possibility to answer 'don't know' when in doubt. Some features were used jointly as honeypots to detect outliers -notably depicted person's gender and beard.

DATA ANALYSIS AND RESULTS

Thanks to crowdsourcing we quickly collected many subjective evaluations. More than 17000 subjective evaluations were collected from 440 participants, spread worldwide over 41 countries. More than 1000 people instead participated in the evaluation of the high level features. Despite these numbers, many participants withdrew the experiment before the end. We cannot say whether they considered their participation not worth the price or whether they experienced technical problems. Investigating experimental timings with server logs, we found that many users in remote regions, notably Eastern Asia, reloaded the test web page more than once in the first crowdsourcing campaign. This fact might indicate poor network connections, and as such, being unable to rapidly load images, even if scaled. However, most evaluations were correctly provided and useful for our analysis.

Comments provided at the end of the test were dominantly positive; users noted that the experiment was clear and asked to be informed of future tests. Evaluations were checked for reliability using the honeypots. Around 20% of the participants failed to provide a reasonable birth year, and another 20% failed to properly indicate the non-portrait images. The corresponding submitted jobs were discarded and participants were notified. Finally, we obtained more than 8000 valid context rankings for further analysis. For the analysis of influential factors, we adopted a Logistic Regression, using our features as regressors and the context ranks as observations to fit. Each portrait picture was represented with its most often selected context ranking. Since the dependent variable had three possible discrete outcomes, we used a Multivariate Logistic Regression. The model, in case of a single observation can be written as:

y n = β 0 + K k=1 x nk β k + n ( 1
)
where y is the dependent variable -the context rank for a particular category -x are our predictor values, β are the coefficients to be estimated and indicates the error term. Even if we expect our model to be more complex than linear, we adopted this method to have interpretable outputs for our features. We fitted three independent models, one for each context, adopting the ranks of that context for all portrait pictures as responses. We used a majority strategy to define the value of the high level features for each portrait picture. So, if a picture was reported to be shot outdoor by 90% of the participants, it was considered as such for the labelling of the high level features. While this subjectivity may be valuable for our study at this stage, we also consider adopting the raw data for the high level features in future work. All features were normalized (especially the low level ones) to the same mean and range, so that the computed coefficients could reflect actual relevance weights. The results of the logistic regression fit are shown in Figure 2. The Friends context was selected as reference in our model. This means that each computed coefficient expresses the influence of a feature on the relative chance that a portrait picture is perceived in another context (i.e., Work or Dating) than the reference, where this chance is expressed in log odds. So for example, an increment of one unit in the feature "Dress" increases β k times the relative log odds of a portrait picture being perceived as Work context, where β k is the coefficient related to the feature "Dress" in the model of the Work context -assuming everything else being equal. The adopted regression method also provides a measure of the statistical influence of each feature in the model via their p-value. These p-values are shown in table 2. They illustrate that the prediction model for a portrait picture having a Work context is significantly affected by the dress (N) that the person in the picture wears, as well as by the portrait setting (L) and by the low level feature of mean saturation (E) in the picture. As expected, a formal dress increases the appropriateness of the portrait for working purposes, while instead an increase in saturation decreases it. For predicting the appropriateness of a portrait for dating purposes instead the gender of the portrayed person, and his/her face orientation are statistically significant contributors. In particular portraits depicting female persons are reported as more appropriate for dating purposes. In this respect, it is interesting to check if the gender of the participant generates a bias to the influence of the gender of the portrayed person. To this extent we adopted permutation test as in our previous work. [START_REF] Mazza | Would you hire me? Selfie portrait images perception in a recruitment context[END_REF] The factor investigated with a chi-square test was the gender of the participant, as obtained from the demographic questionnaire , while the dependent variable was the context evaluation. Note that this analysis considered all the raw evaluations before the majority strategy. Permutation tests underlined that an effect is present (p < 0.05). To analyse if the effect is present especially on one context evaluation, we repeated permutation test considering one context (i.e. work) against the other two (i.e. friends+dating). Gender was found statistically influential only for the appropriateness of portraits for dating purposes, underlining that portraits were evaluated differently between men and women only in the context of dating. This finding pointed out that gender should be more explicitly considered in future research, for example, by only considering evaluations, for which the gender of the portrayed person and the gender of the participant are the same.

DISCUSSION

In this work we addressed the problem of determining influential factors for perceived context of portrait pictures. Our analysis considered some classical low level features as well as higher level features related to image interpretation. It is clear that considering all possible factors of influence in only one analysis is a challenging task. However, isolating them to determine each feature's separate impact is at least as hard and time consuming. We approached the problem considering features we supposed mostly important and we showed how multiple features can be addressed simultaneously. To this extent we gathered more data for a statistical analysis, and so, adopted crowdsourcing not only to determine the appropriateness of a portrait picture for a given context, but also to evaluate the high level features. In fact, extracting these only with computer vision tools can be error prone. We used a white box approach for the statistical analysis that even if less accurate than a black box approach, yet allows easier interpretation of the results. While the proposed analysis is not able to explain all variability in the subjective assessments, some statistically relevant features have been underlined and greatly helped to discriminate between portrait contexts. Our first results are consistent with expectations from empirical experience. In particular the dress of the portrayed person is shown to be discriminative for the likelihood of a portrait to be perceived as work related. Also the gender of the portrayed person appeared to be influential, more particularly for the likelihood of a portrait to be perceived as dating related. The latter, however, was also dependent on the gender of the participant; this element should be taken into account in future works. Interestingly the background interpretation was not as influential as we expected. Instead background interpretation only contributed very little to our model. Future research will deal with online portraits retrieval to adopt a broader scale analysis. With these results in mind, we will focus on computer vision efforts on features underlined as influential.

Figure 1 :

 1 Figure 1: Interfaces adopted for evaluating context (a) and high level features (b) of portraits.

Figure 2 : 2 :

 22 Figure 2: Features regression coefficients for first choice. Friend context has been taken as reference.

Table 1 :

 1 All features adopted in this research are summarized in table LOW LEVEL Aspect ratio, resolution, mean and standard deviation for hue, saturation and value, image contrast. HIGH LEVEL Face size [0-4], orientation [frontal,profile,half profile] and tilt [no,L,R]. Adopted features, with possible values in brackets. Dash represents 'unknown value'.

	Subject gender

* CC attribution licensed images have been taken, provided as found, citing sources. No information about depicted subject was given in order to preserve anonymity. Where no API was available and crawlers were forbidden, we gathered images manually


Luigi Liquori

Simona Ronchi

Della Rocca

ITRS 2004

In this paper, we presents a comfortable fully typed lambda calculus based on the well-known intersection type system discipline where proof are not only feasible but easy; the present system is the counterpart à la Church of the type assignment system as invented by Coppo and Dezani.

Introduction

The Intersection Type Assignment System (Λ u ∧) is a set of inference rules for assigning Intersection types to terms of the untyped λ-calculus. Intersection types are formulae of the implicational and conjunctive fragment of the predicate logic. The syntax and the typing rules are presented in Figure 1. Intersection types were introduced by Coppo and Dezani at the end of '70s, to increase the typability power of Curry's type assignment system for the λ-calculus [START_REF] Coppo | An extension of the basic functionality theory for the λ-calculus[END_REF]. Since then, intersection types have been fruitfully used for designing static semantics of programming languages (e.g. Algol-like [START_REF] Reynolds | Design of the programming language Forsythe[END_REF], and object-oriented [START_REF] Pierce | Simple Type-theoretic foundations for object-oriented programming[END_REF]), for characterizing interesting classes of λ-terms (e.g. the strongly normalizing ones [START_REF] Pottinger | A type assignment for the strongly normalizable λ-terms[END_REF]), and for studying denotational semantics of various untyped λ-calculi [START_REF] Barendregt | A Filter Lambda Model and the Completeness of Type Assignment[END_REF][START_REF] Coppo | Extended Type Structures and Filter Lambda Models[END_REF].

There are many versions in the literature of intersection type assignment systems. Here we choses that one presented as "System D" by Krivine [START_REF] Krivine | Lambda-calcul, types et modèles[END_REF], characterized by the presence of explicit rules for dealing with the introduction and elimination of the intersection. Note that, differently from the big part of the systems presented in the literature, as for example [START_REF] Dezani-Ciancaglini | Intersection types, lambda-models and Böhm trees[END_REF], in this system the connective ∧ is neither commutative nor associative nor idempotent, This last choice has been done since we are looking for a typed version of the calculus, and in this setting it is natural to consider types as syntactical entities. In

Γ ∧ M : σ 1 ∧ σ 2 Γ ∧ M : σ 1 (∧E L ) Γ ∧ M : σ 1 ∧ σ 2 Γ ∧ M : σ 2 (∧E R ) Figure 1. The Intersection Type Assignment System Λ u ∧
any case this choice does not have any consequence on the typability power of the system, which is well known to characterize all and only the strongly normalizing terms [START_REF] Krivine | Lambda-calcul, types et modèles[END_REF].

Following a standard terminology, let us call à la Curry a system assigning types to untyped terms, and à la Church a system assigning types to typed terms, i.e. where types are part of the syntax of terms. Differently from other type assignment systems à la Curry, Λ u ∧ has no natural counterpart à la Church. The classical example is the polymorphic identity in Λ u ∧ that has the following type-derivation:

x:σ 1 ∧ x : σ 1 ∧ λx.x : σ 1 →σ 1 (→I) x:σ 2 ∧ x : σ 2 ∧ λx.x : σ 2 →σ 2 (→I) ∧ λx.x : (σ 1 →σ 1 ) ∧ (σ 2 →σ 2 ) (∧I)
but is untypable using a naïve corresponding rule à la Church for the introduction of intersection types [START_REF] Hindley | Coppo Dezani types do not correspond to propositional logic[END_REF].

x:σ 1 ∧ x : σ 1 ∧ λx:σ 1 .x : σ 1 →σ 1 (→I) x:σ 2 ∧ x : σ 2 ∧ λx:σ 2 .x : σ 2 →σ 2 (→I) ∧ λx: ? .x : (σ 1 →σ 1 ) ∧ (σ 2 →σ 2 ) (∧I)
By the Curry-Howard isomorphism, the λ-term must record the shape of its type-derivation. Naïve solutions of λ-calculi à la Church lead to incompleteness, in the sense that the resulting typed system has less typability power of the type assignment one (see for example [START_REF] Reynolds | Design of the programming language Forsythe[END_REF]). The problem is, as the skilled reader can understand, the presence of non syntax-directed rules that disconnect the λ-term with its type-derivation (hence losing Curry-Howard correspondence).

It is important to point out that this problem does not depend on the chosen intersection type assignment system; indeed no one of the type assignment systems presented in the literature is completely syntax directed (and not-even it cannot be!) .

Our goal is to build a typed λ-calculus à la Church with related typing system, such that the underlying untyped calculus is exactly the λ-calculus à la Curry, and its relation with the type assignment system follows the standard path designed in [START_REF] Van Bakel | Comparing Cubes of Typed and Type Assignment systems[END_REF]. Namely the following requirements must be satisfied: (i) there exists an erasing function J , erasing type informations from terms, such that, if M is a typed term, then J (M ) ∈ Λ;

(ii) typed and type assignment proofs are isomorphic, i.e. both the application of the erasing function J on all terms in a typed proofs produces a correct type assignment proof, and every type assignment proof is obtained from a typed one by erasure.

Moreover, we want that the intersection calculus à la Church inherits all the properties of intersection calculus à la Curry, namely:

(iii) subject reduction;

(iv) strong normalization of typable terms;

plus the following ones:

(v) unicity of typing;

(vi) decidability of type reconstruction and of type checking.

No one of the proposals present in the literature satisfies all the given requirements. The typed languages proposed in [START_REF] Reynolds | Design of the programming language Forsythe[END_REF] and [START_REF] Pierce | Simple Type-theoretic foundations for object-oriented programming[END_REF] are not complete with respect to the type assignment, the ones in [START_REF] Capitani | Hyperformulae, Parallel Deductions and Intersection Types[END_REF], [START_REF] Della Rocca | Intersection Typed Lambda-Calculus[END_REF] and [START_REF] Wells | A Calculus with Polymorphic and Polyvariant Flow Types[END_REF] do not satisfy requirement 1, while the language in [START_REF] Wells | Branching Types[END_REF] does not satisfy requirement 2.

In order to build such a calculus, our attempt has been to design a calculus, where typing depends not only on a new "imperative" formulation of context, now assigning types to term variables at a given location, but also on a new notion of store, that remembers the associations between locations and types. The further task of a store is to record the shape of a proof. Hence a store is a truly typed proof calculus that can be executed by means of suitable reduction rules; reduction in this calculus models cut-elimination. The store-calculus can be defined per se, as decoration of the implicative and conjunctive fragment of intuitionistic logic. So it codifies a set of proofs that is strictly bigger than these corresponding to intersection type-derivations (see [START_REF] Ronchi | Intersection logic[END_REF]).

Finally the desired intersection typed calculus can be built, where stores can be seen as modalities for terms. Very roughly speaking, a modality is a unary operator that can be used for decorating a logical formula, saying additional informations about its provability. In particular the information carried out by a modality can be a meta-theoretical information about the structure of the proof, as for example the modality ! in Linear Logic [START_REF] Girard | Linear Logic[END_REF], that denotes a possible not linear use of a premise. In [START_REF] Della Rocca | Lambda calculus and intuitionistic linear logic[END_REF] a typed language has been showed, where a modality on terms is the counterpart of the modality on types, and it is used for characterizing the variables that can occur not linearly. Here the modality is used for describing the structure of the typederivation. In fact, packing together λ-terms and stores as modalities restrict the stores to describe just the intersection type-derivations. So the typed identity with type (σ 1 →σ 1 ) ∧ (σ 2 →σ 2 ) now is the term: λx : 0.x, where 0 is a location, and the modality of this term is: (λ0:σ 1 .0) ∧ (λ0:σ 2 .0). The typed λ-calculus so obtained satisfies all the above requirements. In particular the type reconstruction and type checking are decidable, and the algorithms are pretty easy.

The paper is organized as follows: In Section 2 the calculus of stores is presented, in Section 3 the whole intersection typed λ-calculus is showed, Section 4 lists its properties, and in particular it contain the type checking and the type inference algorithm. The conclusion presents some final considerations.

The Typed Proof-calculus

The syntax of intersection types is that of the formulas of the implicative and conjunctive fragment of the intuitionistic logic (L∧ →,∧ ) , if we think to the connective → as the implication and to the connective ∧ as the conjunction. However the intersection type assignment system is not corresponding, in the Curry-Howard sense, to this logic, because of the "anomalous" decoration of the rules dealing with the conjunction.

In this section we define a typed calculus, decorating the proof of such a logic. The calculus is a typed λ-calculus, but it is built, instead on variables, on locations. In fact it will be used as a (particular notion of) store, for remembering both the association between locations and types and the structure of the type-derivation. (ii) Intersection types are defined as follows: where α range over a denumerable set V of constants.

Syntax of ΛP.

σ ::= α | σ→σ | σ ∧ σ ι:σ ∈ Γ Γ P ι : σ (Var) Γ, ι:σ 1 P ∆ : σ 2 Γ P λι:σ 1 .∆ : σ 1 →σ 2 (→I) Γ P ∆ 1 : σ 1 →σ 2 Γ P ∆ 2 : σ 1 Γ P ∆ 1 ∆ 2 : σ 2 (→E) Γ P ∆ 1 : σ 1 Γ P ∆ 2 : σ 2 Γ P ∆ 1 ∧∆ 2 : σ 1 ∧ σ 2 (∧I) Γ P ∆ : σ 1 ∧ σ 2 Γ P ∆ : σ 1 (∧E L ) Γ P ∆ : σ 1 ∧ σ 2 Γ P ∆ : σ 2 (∧E R )
(iii) Contexts are finite associations between locations and types, and are defined by the following grammar:

Γ ::= | Γ, ι:σ (iv) Tree-stores are labeled unary/binary trees defined as follows:

∆ ::= ι | λι:σ.∆ | ∆ ∆ (for syntax directed rules) ∆∧∆ | ∆ | ∆ (for intersection rules) (v)
The set Fl(∆) of the free locations in a tree-store ∆ is an easy adaptation to free-stores of the notion of the set of free variables in a λ-term.

In what follows, the symbol ≡ denotes the syntactic equality for terms, types, contexts, type-locations and tree-stores, respectively.

Type System of ΛP.

The system proves judgments of the shape:

Γ P ∆ : σ
Intuitively: in the judgment, the type-context Γ assigns intersection types to store-locations of ∆; the tree-store keeps track of the type of the used location together with a written trace of the skeleton of the typing proof, where the skeleton of a proof is the tree obtained from it by erasing all the informations but the name of the applied rules. So the tree-store ∆ plays the role of the "road map" to backtrack (i.e. roll back) the derivation tree. The typing rules are presented in Figure 2. Some comments are in order:

• (Var) gives types to free-locations;

• (→I) the tree-store ∆ evolves in a new tree-store enriched with the binding for the location ι;

• (→E) observes that the two type-stores of the premises become sub treestores in the conclusion (the hidden application operator being the root);

• (∧I) (∧E L ), and (∧E R ) are the three standard rules that introduce/eliminate intersection-types; note that in order to keep track of which branch is chosen in the intersection-elimination (and keep unicity of typing), tree-stores are marked with two place-holders and indicating the correct branch to select.

Reduction Semantics of ΛP.

Being every term in ΛP a decorations of a proof of L∧ →,∧ , the reduction rules of the languages correspond to the cut-elimination steps of the logic. So the →-cut elimination gives rise to the following reduction rule (similar to the standard β-rule) :

(λι:σ.∆ 1 ) ∆ 2 → ι ∆ 1 [∆ 2 /ι]
and the ∧-cut eliminations give rise to the following two reduction rules:

(∆ 1 ∧ ∆ 2 ) → π 1 ∆ 1 (∆ 1 ∧ ∆ 2 ) → π 2 ∆ 2
The reduction relation → ιπ is the contextual closure of the reduction rules → ι , → π 1 , → π 2 . In particular, we denote by → → π the contextual, reflexive and transitive closure of the two rules → π 1 and → π 2 .

We also work modulo α-conversion, which can be rephrased in our ΛP as the symmetric, reflexive, transitive and contextual closure of the following rules:

λι 1 :σ.∆ → αι λι 2 :σ.∆[ι 2 /ι 1 ] if ι 2 ∈ Fl(∆)
Every type-derivation in Λ u ∧, when terms are erased, corresponds to a proof in L∧ →,∧ , but the vice-versa is not true, since the rule (→ I) corresponds to a meta-theoretical condition on the proofs of the two premises. For a complete analysis of the relation between Λ u ∧ and L∧ →,∧ see [START_REF] Ronchi | Intersection logic[END_REF]. Here just note that, for example, the skeleton of the proof encoded by the tree-store (λ0:σ.0) ∧ 1 is the following:

(V ar) (→ I) (V ar) (∧I)
which cannot be the skeleton of any intersection type assignment derivation.

Example 2.2 We show a type-derivation for the tree-store (λ0:σ 1 .0)∧(λ0:σ 2 .0).

0:σ 1 P 0 : σ 1 (Var)

P λ0:σ 1 .0 : σ 1 →σ 1 (→I) 0:σ 2 P 0 : σ 2 (Var) P λ0:σ 2 .0 : σ 2 →σ 2 (→I) P (λ0:σ 1 .0) ∧ (λ0:σ 2 .0) : (σ 1 →σ 1 ) ∧ (σ 2 →σ 2 ) (∧I)
The Intersection Typed System Λ t ∧ is built starting from a particular notion of context. In fact, now a context associates a type to a variable at a given location, i.e., it both associates the type to the variable and takes a free location for storing the variable itself. This trick allows for remembering, in the rule (→I), just the location, being the corresponding type stored in the tree-store, built by the system in parallel with the typed term. In this way the underlying term is a term of the classical untyped λ-calculus. Moreover, since the tree-store describes the structure of the type-derivation, we obtain the decidability property of typing.

Syntax of Λ t ∧. Definition 3.1 (i) Type-locations, intersection types and tree-stores are defined as in Definition 2.1.

(ii) Contexts are finite associations between variables and types at a given location, and they are defined as follows:

Γ ::= | Γ, x@ι:σ
The set Λ t ∧ of intersection typed terms is defined as follows:

M ::= x | λx:ι.M | M M Type System of Λ t ∧.
The intersection typed calculus Λ t ∧ is in some sense a modal calculus, where terms of ΛP represent the modality. The typed system proves statements of the shape:

Γ M @∆ : σ where Γ is a context, M ∈ Λ t ∧, and ∆ ∈ ΛP. Intuitively: in the judgment, the type-context Γ assigns intersection types to the free-variables of M allocated in the free store-locations; the tree-store keeps track of the type of the used location together with a written trace of the skeleton of the derivation tree. The tree-store ∆ plays the role of the road map to backtrack (i.e. roll back) the derivation tree. The typing rules are presented in Figure 3. Some comments are in order:

• (Var) gives types to free-variables at a given location;

• (→I) is a quasi-classical abstraction rule, but it records in the term only the type-location associated to the abstracted variable; the tree-store ∆ evolves in a new tree-store enriched with the binding for the location ι;

• (→E) is a quasi-classical application rule; observe that the two type-stores of the premises become sub tree-stores in the conclusion (the hidden application operator being the root.)

The notion of skeleton of a proof, defined for the system ΛT , can be naturally extended to the system Λ t ∧. (ii) (Subject Reduction) If Γ P @∆ : σ, and

P @∆ → β Q@∆ , then Γ Q@∆ : σ with ∆ → → π ∆ . (iii) (Strong Normalization) Γ
M @∆ : σ if and only if M @∆ is strongly normalizing.

(iv) (Unicity of Typing) If Γ P @∆ : σ, and Γ P @∆ : σ , then σ ≡ σ .

(v) (Type Reconstruction) Given a context Γ, a type-store ∆, and a term M , there is a type σ such that Γ M @∆ : σ if and only if Type ∧ (Γ, M @∆) = σ.

(vi) (Type Checking) Given a context Γ, a tree-store ∆, a term M and a type σ, Γ M @∆ : σ if and only if Typecheck ∧ (Γ, M @∆, σ) = true.

Properties 4, 5 and 6 of this galleria are reached thanks to the notion of tree-store. Figure 4 shows, in ML-style, the type reconstruction and typechecking algorithms.

As far as the properties listed at the points 1,2,3 of the galleria are concerned, the key one is the isomorphism property between the system Λ t ∧ and the system Λ u ∧, which can be easily proved by induction on type-derivations. Both the subject reduction and the strong normalization property are consequences of it.

Conclusions

We studied in this paper the problem of designing a Church version of the intersection type assignment system. In particular we asked for a typed language such that its relationship with the intersection type assignment system enjoys all the standard requirements we posed in [START_REF] Van Bakel | Comparing Cubes of Typed and Type Assignment systems[END_REF]. Examples of such "good" correspondences are respectively the Church and Curry version of the simple typed λ-calculus, the typed and type assignment version of the second order λ-calculus. We succeed in designing a language satisfying the given requirements, which is based essentially on two tools: an imperative notion of typing, when types are assigned to variables "at a given location", and a typed language, describing intersection type-derivations, whose terms are used as modalities for the terms of the target language.

A reader interested in particular in programming applications could object that the used language is far for being "usable", since the user needs to specify

Definition 2. 1 (

 1 i) Type-locations (or type-addresses) range over Nat.

Figure 2 .

 2 Figure 2. The Proof-calculus ΛP.

Theorem 4 . 2 (

 42 Galleria) (i) (Isomorphism) (a) If D : Γ M @∆ : σ, then there exists D , such that D : J (Γ) ∧ J (M @∆) : σ, with D and D having the same skeleton; (b) If : Γ ∧ M : σ, then there exists D , M and ∆, such that D : Γ M @∆ : σ, and J (M @∆) = M , and J (Γ ) = Γ, with D and D having the same skeleton.

(Var) Γ, x:σ 1 ∧ M : σ 2 Γ ∧ λx.M : σ 1 →σ 2 (→I) Γ ∧ M : σ 1 →σ 2 Γ ∧ N : σ 1 Γ ∧ M N : σ 2 (→E) Γ ∧ M : σ 1 Γ ∧ M : σ 2 Γ ∧ M : σ 1 ∧ σ 2 (∧I)

Liquori, Ronchi dells Roccax@ι:σ ∈ Γ Γ x : σ (Var) Γ, x@ι:σ 1 M @∆ : σ 2 Γ (λx:ι.M )@(λι:σ 1 .∆) : σ 1 →σ 2 (→I) Γ M @∆ 1 : σ 1 →σ 2 Γ N @∆ 2 : σ 1 Γ (M N )@(∆ 1 ∆ 2 ) : σ 2 (→E) Γ M @∆ 1 : σ 1 Γ M @∆ 2 : σ 2 Γ M @(∆ 1 ∧∆ 2 ) : σ 1 ∧ σ 2 (∧I)

Acknowledgment. Simona was kindly supported by QSL: Qualité et Sûrété du Logiciel, CPER, Région Lorraine, Nancy, and by INRIA; Luigi was visiting the Department of Informatics, University of Sussex, Brighton; he would like to thank his hosts Matthew Hennessy and Vladimiro Sassone, and the whole Department of Informatics for the ideal working conditions they provided. The two anonymous referees give also useful comments.

Let α range over a denumerable set V of constants, and Γ ≡ {x 1 :σ 1 , . . . , x n :σ n }, where i = j implies x i ≡ x j . The operator "∧" takes precedence over "→".

Typing Rules

• (∧I) is the most important rule; given two judgments for M proving type σ 1 and type σ 2 , (both proved in the same context Γ but with different treestores ∆ 1 , and ∆ 2 ), we can assign the intersection type σ 1 ∧ σ 2 to M in the context Γ but in the new tree-store ∆ 1 ∧ ∆ 2 . At this point the λ-term M loses the one-to-one correspondence with its proof. Luckily, the new tree-store keeps track of the derivation and guarantees unicity of typing;

• (∧E L ), and (∧E R ) are the two standard rules that eliminate intersection types. Also in this case the λ-term M loses the one-to-one correspondence with its (logical) proof, But the proof is memorized by the tree-store, thanks to the two place-holders and , indicating the applied rule.

Reduction Semantics of Λ t ∧.

In order to maintain the correct relation between a term and its modality, the reduction works in parallel both on terms and on tree-stores. Formally, the reduction relation → βι of Λ t ∧ is the contextual closure of the following reduction rules:

We also work modulo α-conversion, which is the symmetric, reflexive, transitive and contextual closure of the following rules:

We show a polymorphic typederivation for the classical polymorphic identity λx:0.x in the tree-store

x@0:σ 1 x@0 : σ 1 (Var)

(λx:0.x)@(λ0:σ 1 .0) : σ 1 →σ 1 (→I)

x@0:σ 2 x@0 : 2 (Var)

(λx:0.x)@(λ0:σ 2 .0) : σ 2 →σ 2 (→I)

(λx:0.x)@((λ0:

We show a polymorphic type-derivation for the classical selfapplication λx:0.x x in the tree-store λ0:σ 2 .( 0) (0 ).

(λx:0.x x)@(λ0:σ 2 .( 0) (0 )) :

Note how the tree-store memorizes exactly the skeleton of the type-derivation.

Sketch of the Proof-theoretical Development

The system Λ t ∧ enjoys all the properties we asked for. In order to list them, we need to define an erasure function, connecting Λ t ∧ with Λ u ∧.

Definition 4.1 [Erasure]

Let J : Λ t ∧ → Λ be inductively defined on terms and point-wise extended to contexts and tree-stores as follows: not only the typed terms, but also their modalities, which are codings of typederivations. The answer can be twofold. From a programming languages point of view, in every typed language the user, in order to write explicitly the type of a term, in some sense needs to "guess" the correct type-derivation assigning that type to the term itself. Here obviously the type-derivations are more difficult than in the simple typed case. But if we think, for example, to the second order typed λ-calculus, in order to write the term Λβ.Λγ.λx:∀α.α.x(β → γ) of type ∀β.∀γ.(∀α.α) → (β → γ)

it is necessary to know exactly how the rules for introducing and eliminating the universal quantifier work. However, we think that the production of an usable language is not the only justification for the problem we studied. The relationship between typed and type assignment systems is an important theoretical issue, that is interesting in itself.