Julien Cegarra
email: julien.cegarra@univ-jfc.fr

Bernat Gacias
email: bgacias@laas.frlopez@laas.fr

Pierre Lopez Clle

Implications of technological changes in vehicle routing interfaces for planners' constraint processing

Keywords: vehicle routing, automation, decision support, planning, interface, domain, constraints, intentional systems

This study sought to assess the consequences of technological changes in vehicle routing interfaces for planners' constraint processing during route selection. We began by developing a model of domain constraints for the generic vehicle routing problem, in order to characterize planners' constraint processing and assess the visibility of constraints on different routing interfaces. An experiment featuring vehicle routing problems was then designed to test interfaces reflecting technological changes, including automation leading to simplified interfaces and the display of multiple routes computed by algorithms. Twelve participants who had worked for a small transport company for nine months were exposed to all these interfaces. Mental workload, performance and decision-making times were measured. Results revealed that automation decreases mental workload and decision times, attributable to the abridged (vs. unabridged) display of constraints on the interface. Results also showed that the perceptual (vs. analytical) display of routes greatly decreases decision times and enhances performances.

Introduction

The vehicle routing problem (VRP) embraces a class of complex problems consisting in determining an optimum route (chiefly by minimizing the total journey cost) for a set of customers who are subject to side constraints such as time windows and vehicle capacity. The VRP applies to the situation faced by postal organizations, which have to route a fleet of vehicles based in multiple depots to a set of customers with specific time windows for delivery (e.g., [START_REF] Hollis | routing and crew scheduling for metropolitan mail distribution at Australia Post[END_REF]. It also refers to intra-city transport companies providing dial-a-ride services using a heterogeneous fleet (e.g., minibuses) when booking is done either in advance or in real time (e.g., [START_REF] Rahimi | A hierarchical task model for dispatching in computerassisted demand-responsive paratransit operation[END_REF].

In field studies, planners appear to play a crucial role, taking the large set of constraints into account and adapting to changes in the domain [START_REF] Jackson | A new model of scheduling in manufacturing: Tasks, roles[END_REF][START_REF] Sanderson | The human planning and scheduling role in advanced manufacturing systems: An emerging human factors domain[END_REF]. At the same time, the integration of transportation technologies is gradually changing the nature of these decision-making processes, in that vehicle routing interfaces now combine human planners and technologies. For instance, the introduction of global positioning systems (GPS), electronic data interchange (EDI) and geographic information systems (GIS) means that planners can now monitor vehicles more easily, on computer-based road maps. Then there are 'intelligent' transportation systems, which are designed to support decisions by means of powerful algorithms [START_REF] Crainic | Intelligent freight-transportation systems: Assessment and the contribution of operations research[END_REF]. These new technologies are changing the way that routes are planned. More specifically, transport companies are shifting their focus away from stand-alone planners to planners supported by multiple technological systems.

We believe that these technological changes have at least two implications for routing interfaces and the allocation of routing tasks to vehicle planners. [START_REF]Breakdown of ambulance dispatch management[END_REF] The handling of the routing problem's physical constraints (e.g., computing distances between depots and vehicles) is now fully automated, leaving planners to concentrate on the functional aspects of the problem instead. However, if the interface only displays the problem's functional constraints, this can lead to poorer performances whenever the planner is called upon to handle a physical constraint that is not processed by the automated system [START_REF] Couclelis | The certainty of uncertainty: GIS and the limits of geographic knowledge[END_REF].

(2) Algorithms now generate multiple solutions, and in state-of-the-art interfaces, planners are allocated the task of selecting the most relevant one. This approach has long been criticized in industrial planning because it involves examining all the solutions in turn, which creates a very high workload [START_REF] Sanderson | The human planning and scheduling role in advanced manufacturing systems: An emerging human factors domain[END_REF][START_REF] Schakel | Process control: Simple and sophisticated display devices as decision aids[END_REF]. This is certainly not without consequences for vehicle routing interfaces.

The present paper seeks to address these two significant implications of technological changes in terms of mental workload, performance and time taken to make decisions. We focus on the routing problem (i.e., selection of an initial solution), where the interface plays an important role, rather than on the real-time re-planning of vehicles, which tends to revolve around communication with drivers (Ng et al., 1995). We begin by discussing constraint processing and the importance of modeling the work domain in order to assess planners' constraint processing. We then describe an experiment that was designed to assess the implications of technological changes for routing. More specifically, we compared an interface providing all the constraints (both physical and functional; "unabridged") with an interface focusing solely on high-level constraints (functional constraints only; "abridged").

We then compared two interfaces allowing for the successive comparison of solutions (analytical processing of constraints) with a third interface enabling users to compare all the solutions at the same time (perceptual processing). Finally, we discuss the importance of taking planners' constraint processing into account when introducing technological changes.

Domain constraints in vehicle routing problems

PLANNERS' CONSTRAINT PROCESSING IN ROUTE SELECTION

Transportation technologies are rapidly moving toward greater automation. At one extreme, decisions related to route selection have now become fully automated. Taxi dispatching is a typical example of such a system. In taxi dispatching, a group of call-takers answer incoming calls and enter customers' locations into a database. A routing algorithm automatically selects the most appropriate vehicle according to different sets of constraints (available capacity, driver's work schedule, distance from the pickup point, and so on).

Optimization criteria are well known and usually consist in minimizing time and distance to the pickup point. The taxi driver then receives a notification and either accepts or declines to pick up the customer.

In most routing situations, however, such fully automated systems are still uncommon because the optimum solutions cannot be determined with any degree of efficiency through automation alone [START_REF] Lenior | Human-factors engineering for smart transport: Decision support for car drivers and train traffic controllers[END_REF]. In goods delivery, for instance, optimization criteria are particularly complex and planners are known to consider various unstated constraints: personal (e.g., how well the driver knows a particular route or foreign language), environmental (e.g., impact of weather conditions, traffic congestion), social (e.g., period of absenteeism), infrastructure (e.g., vehicle maintenance), and so on. The planner has a list of demands and has to prepare a sheet for each driver, on the basis of constraints such as locations, sequences, travel times and time windows for deliveries. This solution, which is also based on optimization criteria, is then given to each driver at the start of his or her shift.

In an ideal world, the planner would design a route considering each constraint as an independent subproblem. However, as these constraints interact, planners cannot define an acceptable route without paying considerable attention to their interactions. In line with [START_REF] Stefik | Planning with constraints (MOLGEN: Part 1)[END_REF], we regard constraints as expressions of partial relationships among variables. They also partially specify the overall solution (route). Planners play a crucial role, taking the large set of routing constraints into account and adapting to changes in the problem constraints [START_REF] Jackson | A new model of scheduling in manufacturing: Tasks, roles[END_REF][START_REF] Sanderson | The human planning and scheduling role in advanced manufacturing systems: An emerging human factors domain[END_REF]. They also make a decisive contribution when problems are over-constrained, as their extensive knowledge allows them to relax constraints in order to arrive at an efficient solution [START_REF] Gacias | Une approche interdisciplinaire pour l'ordonnancement des transports [An interdisciplinary approach for the vehicle routing problem[END_REF][START_REF] Higgins | Interaction in hybrid intelligent scheduling[END_REF][START_REF] Higgins | Interaction in hybrid intelligent scheduling[END_REF]MacCarthy & Wilson, 2001). Planners play such a vital part in routing that full automation of route selection is impossible. If they are to be properly supported, it is important to identity all the constraints they have to process in order to design appropriate routing interfaces.

There have been a number of attempts to define the vehicle routing task structure on the basis of hierarchical task analysis [START_REF] Rahimi | A hierarchical task model for dispatching in computerassisted demand-responsive paratransit operation[END_REF] and cognitive task analysis (Wong & Blandford, 2002). However, when Cegarra and van Wezel (2010) compared the amount of information produced by these two methods, as well as by work domain analysis, they found that the latter was far more exhaustive in identifying constraints, not least because it provides a generic view of constraints and does not focus on usual or known tasks. Work domain analysis (WDA) was developed by Rasmussen and colleagues (Rasmussen, [START_REF] Pejtersen | Cognitive systems engineering[END_REF][START_REF] Vicente | Cognitive work analysis: Towards safe, productive, and healthy computer-based work[END_REF] and emphasizes on the domain constraints. Initially, it was applied to "causal" systems guided by physical laws, as in nuclear power stations [START_REF] Itoh | An ecological interface for supervisory control of BWR nuclear power plants[END_REF], conventional power stations (Burns, 2000) and cement milling plants ( Van Paassen, 1995). In "causal" systems, the objective reality is imposed on the human operator [START_REF] Vicente | Cognitive work analysis: Towards safe, productive, and healthy computer-based work[END_REF], as opposed to "intentional" systems, where the operator is the main agent of the domain and there are fewer references to an external environment. This is the case of routing problems, where it is difficult to enumerate the constraints in a generic fashion because they result partly from conventions, organizational objectives, formal or informal rules and operators' goals.

TOWARD COMPLETENESS OF DOMAIN CONSTRAINTS

At the lowest levels of the routing constraint space, we find physical objects such as vehicles, goods, drivers or depots. These objects are easily identified through interviews or observations. The highest levels, however, may well include human activities, for which work domain analysis is inappropriate. For instance, when [START_REF] Wong | The ecological approach to interface design: Applying the abstraction hierarchy to intentional domains[END_REF] produced a tentative breakdown of ambulance dispatching, they initially conducted a cognitive task analysis and then used their findings to model the work domain. The authors included human tasks in their breakdown (e.g., "Locate nearest available ambulance", "Dispatch in 3 minutes"), meaning that the analysis did not focus solely on domain constraints. [START_REF] Hajdukiewicz | Work domain analysis for intentional systems[END_REF] criticized this approach and undertook a different breakdown, trying to describe the constraints more independently of the decision-maker (see Fig. 1). At the top of their hierarchy is the overall functional purpose of the system, namely taking care of sick or injured people based on acceptable risks and resource constraints. This is done by prioritizing emergencies according to several abstract functions: 'survival/damage' (degree of urgency), 'resource balance', 'time' and 'probability of successful treatment' (related to transportation and care quality). Moving down to the lower levels, the description focuses increasingly on the physical aspects, such as physical functions: capabilities and limitations of resources to handle emergencies (e.g., ambulance speed, vehicle only offering first aid). Finally, physical form describes the appearance, condition and location of the emergencies.

INSERT FIGURE 1 ABOUT HERE

Even so, when we look carefully at their proposed breakdown, we see that it is based on a hypothetical situation featuring two available ambulances and two emergencies (see Fig. 1). [START_REF] Vicente | Cognitive work analysis: Towards safe, productive, and healthy computer-based work[END_REF] stressed that work domain analysis should be performed independently of usual or known tasks, the aim being to provide an exhaustive breakdown that is resistant to changes in the situation. Thus, while their breakdown focuses on constraints, not planners' tasks, it still deals with known cases, which is not compatible with the idea of a detailed and resilient view of constraints. In view of this, we sought to enhance the identification of domain constraints by extending the scope of the domain. More specifically, instead of focusing on currently known or usual cases in one particular situation (which inevitably leads to the inclusion of more details about the current situation), we set out to identify constraints by looking at different situations documented in the literature. Each variant of the VRP would allow us to increase the completeness of the constraint space by considering constraints which might potentially help to identify planners' degrees of freedom. Our search for VRPs in scientific databases yielded more than ten thousand articles. However, only a few of them suggested genuinely new variants of the generic VRP (see [START_REF] Toth | The vehicle routing problem[END_REF]. Instead, researchers tended to develop algorithms to solve known variants or design algorithms for multiple variants (e.g., Pisinger & Ropke, 2007). The variants extended the domain by providing constraints related to a temporal perspective, including customers' time windows (VRPTW) and vehicles with limited capacity (CVRP), as well as more complex ones, such as trucks and trailers (TTRP), pick-up and delivery (VRPPD), or constraints related to multiple depots (MDVRP).

INSERT FIGURE 2 ABOUT HERE

As previously indicated, work domain analysis organizes the planners' constraint space in terms of different concepts that planners can then use for reasoning within a work system. We believe that the classic five levels of the abstraction hierarchy are needed to describe this space, as exemplified in Figure 2. Detailing each level is beyond the scope of this article, but readers can refer to [START_REF] Gacias | Une approche interdisciplinaire pour l'ordonnancement des transports [An interdisciplinary approach for the vehicle routing problem[END_REF] and [START_REF] Gacias | Work domain analysis and ecological interface for the vehicle routing problem[END_REF] for further details about the different variants and the procedure we used to achieve this model. [START_REF] Harper | Human factors in technology replacement: A case study in interface design for a public transport monitoring system[END_REF] performed a task analysis of vehicle planners and noted that it was necessary both to improve positional information about vehicles for correct planning and to reduce tasks requiring the entry of large amounts of data. These recommendations have since been met by the introduction of technological changes, with companies increasingly integrating new systems such as GPS, EDI and GIS into their internal systems, and the development of support systems to aid in routing decisions and reduce time-consuming tasks. This brings us to the two main technological changes under consideration in our study.

Challenges for constraint processing following technological changes

AUTOMATION AND CONSTRAINT ABRIDGMENT

The introduction of new automation devices has brought about a major change in routing procedures. GPS help planners to gather information about vehicles' current routes and automatically compute journey times to customers. EDI systems, such as on-board computers, allow locations and other information to be automatically transferred between planners and drivers. GIS, meanwhile, are gradually being integrated with GPS and EDI, and allow planners to easily monitor vehicles on computer-based road maps. [START_REF] Keenan | Spatial decision support systems for vehicle routing[END_REF] noted that planners can greatly improve the quality of routes produced by automated systems. Furthermore, because planners' decisions are partly based on positional information, he argued that routing interfaces should be supplemented with GIS technology. However, with this increasing automation and the introduction of hardware devices, the work situation of planners will inevitably start to resemble supervisory control in process industries [START_REF] Lenior | Human-factors engineering for smart transport: Decision support for car drivers and train traffic controllers[END_REF]. As such, to select routes, planners will no longer need to have extensive knowledge about physical constraints, especially spatial ones (e.g., location of vehicles or customers). In addition, with GPS and EDI automatically computing distances, planners will find it easier to combine these constraints with basic information about road networks. They will simply have to choose the most relevant solution according to optimization criteria such as the overall cost of the solution. If the physical levels of the abstraction hierarchy are automated, planners will naturally focus their attention on the functional levels (optimization criteria). Moreover, it is often recommended to design interfaces that favor direct perception of higher-level constraints (Vicente, 2002). In the present study, an interface showing only the functional constraints was referred to as "abridged" and an interface showing both physical and functional constraints was referred to as "unabridged". We hypothesized that participants using an abridged interface rather than an unabridged one would require less time and mental workload to select routes and would perform better (Hypothesis 1).

DECISION SUPPORT AND ROUTE SELECTION

More recently, transportation systems have started to focus on software issues, especially the use of powerful algorithms to support decision-making [START_REF] Crainic | Intelligent freight-transportation systems: Assessment and the contribution of operations research[END_REF]. Algorithms form the basis of 'intelligent' transportation systems and are based on either mathematical models (operational research; OR) or knowledge representation formalisms (artificial intelligence; AI). They are needed to deal with problem complexity and to supply complex data, for instance by anticipating peak demands [START_REF] Linton | decision Support system for planning remanufacturing at Nortel Networks[END_REF], or providing values for shift optimization [START_REF] Taylor | A break from tradition for the San Francisco Police: Patrol officer scheduling using an optimization-based decision support tool[END_REF]. A second purpose of these algorithms is generally to reduce the time-consuming task of manually designing repetitive plans for the vehicle fleet (e.g., [START_REF] Avramovich | A decision support system for fleet management: A linear programming approach[END_REF].

As previously noted, planners have to choose the most appropriate solution according to the current goal. To this end, powerful algorithms provide the capability to compute all the possible solutions. The planners are then shown all these possible solutions, displayed on a computer screen one at a time. However, this approach involving the analytical processing of solutions has long been criticized in industrial planning for generating a very high mental workload and sometimes leading to poor decision-making [START_REF] Sanderson | The human planning and scheduling role in advanced manufacturing systems: An emerging human factors domain[END_REF][START_REF] Schakel | Process control: Simple and sophisticated display devices as decision aids[END_REF]. A real-world example is described by [START_REF] Mietus | Understanding planning for effective decision support[END_REF], who noted that planners who were offered multiple solutions often finally focused on only one of them. [START_REF] Cegarra | The role of algorithm and result comprehensibility of automated scheduling on complacency[END_REF] demonstrated that planners sometimes accept a level of performance that is lower than the level they are capable of achieving, due to the very high mental workload of solution analysis.

According to [START_REF] Vicente | Cognitive work analysis: Towards safe, productive, and healthy computer-based work[END_REF], interfaces should favor direct perception of visual patterns, as planners' powerful visual perception of patterns has frequently been noted (Dessouky et al., 1995;[START_REF] Sanderson | The human planning and scheduling role in advanced manufacturing systems: An emerging human factors domain[END_REF][START_REF] Trentesaux | Integration of the human operator into responsive discrete production management systems[END_REF]. Ormerod and [START_REF] Chronicle | Global perceptual processing in problem solving: The case of the travelling salesperson[END_REF], for instance, showed that visual perception allows planners to find close approximations to optimum solutions for simple routing problems at low computational costs.

An effective approach to supporting decisions would thus consist in collating and integrating multiple routing solutions into a single visual form (see [START_REF] Bennett | Graphical displays: Implications for divided attention, focused attention, and problem solving[END_REF]. This way, planners would be guided in their use of perceptual rather than analytical processing of the constraints. An interface displaying the solutions separately (requiring analytical processing) would therefore result in poorer performances, longer decision times and a higher mental workload than an interface presenting all the solutions simultaneously (and allowing for perceptual processing) (Hypothesis 2).

These two types of interfaces focus solely on functional constraints (both are "abridged interfaces") and require algorithms to produce adequate routes on the basis of information from GIS, EDI and GPS. However, there are always data that escape automation [START_REF] Couclelis | The certainty of uncertainty: GIS and the limits of geographic knowledge[END_REF]. For instance, congestion black spots are not always taken into account by automated systems, whereas this is precisely the kind of supplementary knowledge needed for route selection that human operators possess. When [START_REF] Golob | Traffic congestion and trucking managers' use of automated routing and scheduling[END_REF] conducted a survey of 700 trucking companies operating in California, 85% of managers said that traffic congestion caused missed schedules and 36% regarded congestion as a serious problem for their businesses. The interface should therefore display not just functional information but also information about crucial physical constraints (e.g., traffic status in a particular location), which is not the case in "abridged" interfaces. When the planner interacts with an "abridged" interface, we can thus deduce that solving a problem with a physical constraint will require more time and a higher mental workload, and result in poorer performances, than solving a similar problem with a functional constraint (Hypothesis 3)

Constraint processing: an empirical assessment

PARTICIPANTS

In most companies, routing problems are solved by just a single planner or a very small group of individuals. Moreover, due to the extreme diversity of routing situations, it is often difficult to generalize results [START_REF] Cegarra | A cognitive typology of scheduling situations: A contribution to laboratory and field studies[END_REF]. For this reason, most routing and scheduling experiments have been carried out with students. However, it can be difficult to reach conclusions about interface design, as students do not have the experience needed to solve routing problems. For this study, we therefore gave participants extensive training beforehand.

Twelve participants (mean age: 23.8; six men, six women) spent nine months working for a small firm of consultants who mainly provide fleet management analyses for the private and public sectors. More specifically, they carried out a variety of tasks related to transportation and routing. These included analyses of customers' sites in order to assess distribution costs, analyses of companies' transport costs (multiple transport modes), and fleet utilization assessments. In particular, they worked on a case in the same geographical area as the one used as the context for this study. At the end of these nine months, we deemed that they had all acquired sufficient experience of the transportation domain and reached approximately the same level of practice in transportation cost assessment and route selection.

EXPERIMENTAL DESIGN

The experiment used a 2 x 3 within-participants design. The independent variables were scenario type (physical vs. functional constraint) and interface (analytical + abridged vs. analytical + unabridged vs. perceptual + abridged). All six conditions required participants to select the best solution from a set of thirty computer-generated solutions.

Participants were individually invited to take part in the experiment. They were first given a document introducing them to the context of the routing problem. They then familiarized themselves with the three interfaces by using them to solve a number of training problems. This training phase was repeated until they had correctly solved all the problems.

Participants were then administered one problem in each of the six conditions, in a pseudorandom order. Each time they embarked on a fresh problem, participants were instructed to find the least costly solution (performance criterion) that satisfied one particular constraint (either functional or physical). Unlike the training phase, no performance feedback was provided after the completion of each problem.

Each problem was designed in such a way as to produce thirty solutions, five of which satisfied the relevant constraint. One of the five was calculated using the classic Bellman-Ford algorithm [START_REF] Bellman | On a routing problem[END_REF], which finds the shortest path in polynomial time with a minimum cost in a graph. The four others were all acceptable routes, but with different modes of transport and higher transportation costs. Therefore, the computational nature of each problem was the same, meaning that any significant difference in the variables we measured related solely to the experimental condition (scenario or interface).

CONTEXT AND SCENARIOS

A real-life problem of waste collection was taken as the context for this study. Each year, a producers' organization in the French department of Seine-et-Marne grows several hundred thousand tons of beet. Harvesting starts in July and ends in October, before surface temperatures fall below freezing. The beets are cleaned in order to remove sand, soil and stones. The sand is then either transported by the producers to an expensive waste collection site or sold at a low price to construction companies. Overall, the producers' organization has to plan the transportation of the sand with a view to minimizing the total costs (transportation costs and unloading costs for the unsold sand) and (a secondary concern) the number of days required for transportation. This context allowed us to design several problems.

INSERT FIGURE 3 ABOUT HERE

In our experiment, 4,550 tons of sand had to be routed from the producers' depot ("La Chapelle Rablais" in Fig. 3). The planner had to deliver as many tons as possible to construction companies ("Poincy", "St-Rémy-la-Vanne", "Rouilly", "Rozay-en-Brie" and "Episy" in Fig. 3) in order to minimize the quantity of sand that would have to be unloaded at the waste collection site ("Claye-Souilly"). Multiple constraints had to be taken into account.

First, unloading at the waste collection site cost about €100/ton, while the construction companies would take the sand for free and sometimes even pay a small amount of money for it (see Table 1). Furthermore, the waste collection site was large enough to take all the producer's sand, whereas the construction companies differed in the amount they could take, according to their construction needs.

INSERT TABLE 1 ABOUT HERE

Second, a number of different transportation modes were available: trucks, barges, and trains. For each mode of transport, capacity, transportation cost (cost/ton/km), and average speed constraints had to be considered (see Table 2). With road transport (trucks), the costs of traveling back and forth also had to be included. Two of the modes (barges and trains) were only possible from one fixed point to another, along fixed routes: the barge docks were located in "Dammarie-les-Lys" and "Meaux", while there were train depots in "Melun", "Nangis" and "Provins".

INSERT TABLE 2 ABOUT HERE

The abstraction hierarchy presented in Figure 2 was used to determine the relevant physical and functional constraints in this waste collection context. It indicated that not all the constraints of the work domain analysis were needed to produce a solution.

The system's functional purpose is twofold: find a solution that both minimizes costs and ensures adequate customer service. In our experiment, the company was both the planner and the customer of the solution, and the most important constraints therefore related to costs.

Regarding the values and priority measures (second level of the hierarchy), the planner needed to consider global capacity first (total cost of transport), followed by the number of days needed to implement the solution. At the lowest level of the abstraction hierarchy, the planner needed to take into account the types of vehicles available, the volume that had to be routed, and the location of the depots. These constraints determined the number and type of vehicles needed to handle the volume, the routes they took, and their travel times (different speeds for different modes).

Before each condition of the experiment, participants were told that they would have to satisfy one of two types of constraints:

A high-level, functional constraint. This involved looking for solutions whereby all the sand could be routed in the space of a set number of days (e.g., "You have to determine the least costly route for dispatching the sand in less than 5 days");

A low-level, physical constraint. Here, they had to avoid a particular route due to congestion (e.g., "You have to determine the least costly route for dispatching sand, avoiding the 'La Chapelle Rablais'-'Meaux' road due to extensive roadworks").

INTERFACES

We designed three different interfaces for selecting the solutions (see Fig. 4).

INSERT FIGURE 4 ABOUT HERE

The first interface (a) provided only functional information about the thirty solutions, which were displayed one at a time. The user had to click on arrows to browse through the solutions, which implied analytical processing of these solutions. Each screen consisted of performance measures (transportation cost, number of vehicles used, time required for the collection). As only functional information was shown on the screen, this was dubbed the "abridged interface". In this interface, physical constraints such as the route used by vehicles or the locations were not displayed.

The second (analytical) interface (b) had the same structure, but this time physical information was added to each solution. More specifically, a map was displayed, highlighting the routes used by the different modes of transport for a given solution. This allowed both the problem's physical and functional constraints to be visualized ("unabridged interface").

The third interface (c) was regarded as a 'perceptual' interface, in that it presented all the solutions simultaneously on the screen. Participants therefore did not need to browse through the solutions because they were all presented on the screen. Instead, they had to circle the selected solution with the mouse. Only functional information was provided on this (abridged) interface. It therefore differed from the first one not in the information being displayed but in the way the solutions were presented (simultaneously vs. successively).

For the purpose of our analyses, the first, abridged, interface (a) constituted the control condition.

PERFORMANCE MEASURES

In order to assess the participants' behavior and compare their performances in relation to the scenarios and the interfaces with which they had to interact, we selected three measures:

-Routing performance: This performance measure referred to the instructions given to participants, namely to minimize costs whilst satisfying the prescribed constraint. We deemed that the participant had successfully solved the problem if he or she selected the solution with the best performance.

-Time performance: unlike the measure of routing performance, time performance was a measure not of the outcome but of the cognitive process. Participants needed time to compare the solutions and select the most appropriate one. Longer times could be assumed to reflect more demanding cognitive processes.

-Mental workload: We reviewed various workload analysis methods in terms of their invasiveness and opted for measures that were directly obtained from participants.

Accordingly, workload was assessed with the NASA-TLX [START_REF] Hart | Development of NASA-TLX (Task Load Index): Reof empirical and theoretical research[END_REF]. The NASA-TLX is a multidimensional rating scale procedure. It probes six dimensions of workload: cognitive demand, physical demand, temporal demand, effort, performance, and frustration. It is often considered to be not only the most sensitive subjective measure, but also the most reliable one [START_REF] Cegarra | The use of Tholos software for combining measures of workload: Towards theoretical and methodological improvements[END_REF]Hill et al., 1992). The Frenchlanguage version was validated prior to this study [START_REF] Cegarra | Etude des propriétés de la version francophone du NASA-TLX[END_REF].

RESULTS

In order to test statistical significance, we performed repeated-measures ANOVAs.

We controlled the overall Type I error rate of the planned comparison by adjusting the p value downward for declaring statistical significance (p = .0125). Moreover, a priori power analyses performed with G*Power software [START_REF] Faul | Statistical power analyses using G*Power 3.1: Tests for correlation and regression analyses[END_REF] showed that an optimum sample size would be N = 52. This was far higher than the number of available participants in our study and directly affected the probability of the Type II error-retaining a false null hypothesis. Because it would not have been possible to distinguish between the absence of an effect and the lack of statistical power needed to detect an effect, nonsignificant results were regarded as inconclusive and are not discussed here.

Abridged vs. unabridged interface

4.6.1.1.
Time taken to select a solution

INSERT FIGURE 5 ABOUT HERE

The comparison of interfaces, illustrated in Figure 5, showed that the task took longer to perform with the unabridged interface than with the abridged one. There was therefore an overall significant effect of interface type across all the scenarios, F(1, 11) = 27.212, p = .000, η p ² = .546. In terms of behavioral performance, it took participants longer to make decisions when all the constraints were visible on the interface.

Concerning scenario type (physical vs. functional constraint), we failed to observe any clear difference in total times between the two interfaces and our statistical analyses failed to reveal any overall significant effect of scenario type across the interfaces, F(1, 11) = .486, p = .493, η p ² = .021.

Mental workload

INSERT FIGURE 6 ABOUT HERE

Concerning the effect of interface type (Fig. 6) we observed small but consistent differences in workload between the unabridged and abridged interfaces. Statistical analyses highlighted an overall significant difference between the two interfaces, F(1, 11) = 11.317, 4.6.2. Analytical vs. perceptual interface 4.6.2.1. Time taken to select a solution

INSERT FIGURE 8 ABOUT HERE

Looking at the results from a descriptive point of view, we observed that decisions took less time to make with the perceptual interface than with the analytical interface (Fig. 8).

More specifically, results showed that there was an overall significant effect of interface type across all conditions, F(1, 11) = 13.104, p = .001, η p ² =.363, with participants making decisions faster with the perceptual interface than with the analytical ones.

Furthermore, there was an overall significant effect of type of scenario across the interfaces, F(1, 11) = 36.109, p = .000, η p ² = .611. This indicated that participants worked faster when they had to consider a functional constraint rather than a physical one.

Mental workload

INSERT FIGURE 9 ABOUT HERE

When we looked at mental workload, there did not appear to be any difference between the interfaces. Statistical analysis also showed that there was no significant overall effect of interface on mental workload, F(1, 11) = .202, p = .657, η p ² = .009. However, due to the small sample size, it was not possible to conclude as to the absence of effect or the lack of statistical power.

There appeared to be a small difference between the physical and functional constraint scenarios (Fig. 9). A descriptive analysis allowed us to determine that there was a greater mental workload for physical constraint scenarios than for functional constraint ones. This finding was strengthened by a statistical analysis, which revealed a significant effect of scenario on mental workload, F(1, 11) = 19.125, p = .000, η p ² = .454.

INSERT FIGURE 10 ABOUT HERE

During the experiment, virtually no errors were committed whilst using the perceptual interface (see Fig. 10). Only one of the participants using this interface missed the correct solution, relaxing the functional constraint that had been given. Two of the participants using Results indicated that an abridged interface requires less time and mental workload to select a solution, all the while ensuring a high level of performance. More generally, our results confirmed our first hypothesis and showed that participants did not have to see the lower levels of the abstraction hierarchy to make decisions when these levels were only by the system (GPS, GIS, EDI) to calculate solutions. [START_REF] Keenan | Spatial decision support systems for vehicle routing[END_REF] had previously argued that routing interfaces should be supplemented maps and spatial data (e.g., administrative boundaries). However, our results indicated that this lower-level information was superfluous to requirements. In all probability, when an interface contains supplementary information about the solution, planners laboriously take all this excessive data into account, resulting in an increase in decision time and mental workload.

This does not mean to that physical constraints such as spatial information are not crucial for resolving routing problems. If planners are in frequent communication with drivers during route execution, they are more likely to require route and navigation information to carry out real-time monitoring. Thus, planners who currently use GIS regard these features as for communicating with drivers (Ng et al., 1995). This is mainly because they need to view the situation from the drivers' perspective. Accordingly, while computer-based maps are useful for supporting communication with drivers, we can conclude that they are of little assistance to experienced planners when they are selecting the initial routes.

A similar conclusion has been reached in the industrial scheduling domain. In this domain, the Gantt chart, which displays the use of resources on the y-axis and time on the xis the most popular way of representing solutions. For this reason, various authors have that humans should be supported by Gantt charts (e.g., [START_REF] Adelsberger | The Leitstand -A new tool for computer-integrated manufacturing[END_REF][START_REF] Kurbel | Integrating intelligent job-scheduling into a real-world production-scheduling system[END_REF]. However, these have also been criticized, for helping humans to communicate the plan to other individuals but not necessarily to reach planning decisions [START_REF] Higgins | Interaction in hybrid intelligent scheduling[END_REF]. Therefore, as Trenteseaux, [START_REF] Trentesaux | Integration of the human operator into responsive discrete production management systems[END_REF] suggested in the industrial domain, and as demonstrated by our results, new graphical forms need to be developed for route selection.

ANALYTICAL VS. PERCEPTUAL INTERFACE

Results showed that an interface facilitating perceptual rather than analytical processing requires less time for decision-making. While the results on mental workload are inconclusive, the decision time finding partly confirms our second hypothesis. This result is also in line with other studies showing that planners who have to undertake pairwise comparisons are impacted in their decision-making [START_REF] Sanderson | The human planning and scheduling role in advanced manufacturing systems: An emerging human factors domain[END_REF]. Similarly, there is now a large body of literature arguing for integrated rather than separate displays [START_REF] Bennett | Graphical displays: Implications for divided attention, focused attention, and problem solving[END_REF]. Integrated displays collate and integrate data from multiple sources ("sensors") into a single visual form, unlike separate displays which map each source to a different display. Our results stress the importance of facilitating the perceptual of constraints in order to facilitate the decision process. A secondary benefit of having all the information available in computers is the possibility of sharing this information among the company's different departments (shipping, planning, drivers), thus facilitating the overall routing process [START_REF] Scapinakis | Communications and Positioning Systems in the Motor Carrier Industry[END_REF].

Nonetheless, one of our study relates to the reliability of the data. In our experiment, participants consistently performed well across all the conditions, selecting that satisfied the prescribed constraints. Implicitly, the solutions were designed as the computer had access to the physical constraint congestion) when it designed the routes. In practice, however, this constraint is not available to computers and they sometime generate solutions on the wrong basis. Moreover, unreliable data can considerably affect the performance and usefulness of integrated displays, as [START_REF] Reising | Minimally adequate instrumentation in an ecological interface may compromise failure diagnosis[END_REF] demonstrated in their study of the Pasteurizer microworld. This limitation highlights the need for a follow-up study of how planners react to imperfect solutions. For Reddy et al. (1995) analyzed the route selection behavior of students using simplistic routing software. They noted that acceptance of the single solution proposed by the computer was related to its accuracy. More specifically, if they had been given poor advice, participants chose not follow the computer's advice for subsequent trips, although they did sometimes start following it again if the accuracy of the computer-generated routes increased.

When they looked at experienced planners, Ng et al. (1995) found that they set little store by the route selection features of automated systems because they trusted in their own ability to find an appropriate route. These results are in line with research on trust and self-confidence (Lee & See, 2004) and highlight the need to explore the design of trustable routing systems, for instance on the basis "sensor abstraction hierarchies" [START_REF] Reising | Minimally adequate instrumentation in an ecological interface may compromise failure diagnosis[END_REF] to determine potential automation inadequacies and their consequences for routing interfaces.

Another important result of our study is the increase in workload and decision-making time for physical as opposed to functional constraints for both interfaces. At first sight, this would appear to confirm our third hypothesis. However, these results need to be set against performance, as the perceptual interface allowed participants to achieve perfect performance on physical constraint scenarios, which seems incompatible with our hypothesis. Moreover, in the comparison of abridged vs. unabridged interfaces, we noted that mental workload was higher for the physical constraint than for the functional one for both interfaces. Overall, these results emphasize that finding an adequate route with a physical (spatial) constraint is a demanding task even in the presence of a computer map. One possible explanation is that these maps are inadequate support physical constraint processing.

and [START_REF] Golob | The perceived usefulness of different sources of traffic information to trucking operations[END_REF] showed in a survey that planners regard computer maps as one of the least useful means of reporting traffic congestion. At the same time, they noted that traffic maps were deemed to be helpful for carriers with long load moves (>800 km) but not for private carriers (transporting only their own goods) and carriers with short load moves.

This directly relates to previous experience of the road network. Planners who are not familiar with the road network (as is the case for long moves) probably need maps to visualize the routes, whereas well-informed planners (e.g., those repeating short moves) do not. For experienced planners, like our participants, alternative routes may not necessarily be best supported by maps, as these routes are already known to them. This idea is also supported by different investigations of planners' practice, showing that information about traffic conditions is mainly obtained from radio reports and direct communication with drivers and is not necessarily based on maps (Hall & Intihar, 1997). This underscores the need to design innovative interfaces for visualizing spatial constraints in an efficient manner, rather than providing planners with information they already have in their heads. More generally, our listing of constraints in the form of an abstraction hierarchy (see Fig. 2) could serve in followup empirical studies to identify the constraints (time, capacity, etc.) that planners already handle well and those that really deserve to be supported.

Conclusion

are many obstacles to the design of empirical studies in the routing domain. The presence of only a few planners in each company, the complexity of domain modeling and the interdisciplinary nature of these issues all make it difficult for researchers to analyze routing interfaces. This probably explains why the latest peer-reviewed article empirically assessing the perception of constraints in planning problems was published so long ago [START_REF] Gibson | The presentation of information to the job-shop scheduler[END_REF]. Since then, many authors have expressed concern at the dearth of empirical studies of planning/routing [START_REF] Hoc | L'assistance à l'opérateur humain pour l'ordonnancement dans les ateliers manufacturiers [Human operator support of scheduling in manufacturing workshops[END_REF][START_REF] Moray | Trust and human intervention in automated systems[END_REF][START_REF] Sanderson | The human planning and scheduling role in advanced manufacturing systems: An emerging human factors domain[END_REF].

changes have implications for the way planners solve vehicle routing problems. Our results on route selection have direct consequences for the design of routing interfaces. More specifically, they validate the inclusion of automation and decision support in interfaces. However, they also stress the need to evaluate routing interfaces in terms of information reliance (abridgment), automation accuracy (trust) and graphical forms tailored to meet genuine support needs. At the end of the day, our results reinforce the idea that it is not the technology itself that is the key to its application in routing, but rather the way in which it is merged with planners' decision-making processes. Overall mental workload (NASA-TLX).

  the analytical interface failed to find the best solution with functional constraints and three of them failed to find the best solution with physical constraints. Chi-square tests did not reveal a significant effect of interface on performance [χ(1) = .381, ns]. No significant effect was observed for scenario [χ(1) = .000, ns]. Nonetheless, it is worth noting that only participants handling physical constraints with the perceptual interface achieved perfect route selection performances. Discussion 5.1. ABRIDGED VS. UNABRIDGED INTERFACE

Figure 2 .

 2 Figure 2. Work domain analysis the generic vehicle routing problem.

Figure 3 .

 3 Figure 3. Schematic view of the different locations and distances featured in the experiment.

Figure 4 .

 4 Figure 4. Illustrations of interfaces used in the experiment. Highlighted routes on the

Figure 8 .

 8 Figure 8. Total taken to select a solution according to interface type and

Table 2 .

 2 each transport mode.

	Transport Maximum capacity Transportation cost for	Average speed
			maximum capacity
	Truck	25 tons	€ 2.50/km	55km/h
	Train	500 tons	€ 250/km	18km/h
	Barge	400 tons	€ 80/km	8km/h

Acknowledgments

We are very grateful to Elizabeth Portier for proof-reading this article.

p = .003, η p ² = .330. Thus, a smaller mental workload was involved in finding solutions with the abridged interface than with the unabridged one.

There was a comparable difference in workload according to type of constraint (Fig. 6). We were thus able to identify a significant overall effect of scenario, F(1, 11) = 8.769, p = .007, η p ² = .276. Participants experienced a higher workload when they considered physical versus functional constraints. 4.6.1.3.

Routing performance

INSERT FIGURE 7 ABOUT HERE

Regarding the percentage of participants who successfully solved the problem, there was no clear difference between either the interfaces or the scenarios (Fig. 7). In every condition, two or three participants systematically failed to find the best solutions. A detailed scrutiny of the solutions they selected showed that these were almost always the second or third best. Only one participant selected a solution that did not satisfy the physical/functional constraint.

Using performance (success/failure) as a dichotomous variable raises concerns as to the applicability of analyses of variance. A variable taking the value of zero or one to count the number of correct answers is not normally distributed. Lunney (1970) argued that analyses of variances are robust for dichotomous variables if the response proportions are less extreme than 20%-80%. This was not, however, the case for these results. We therefore proceeded to conduct nonparametric chi-square tests. Results failed to reveal a significant effect of either interface [χ(1) = .000, ns] or scenario [χ(1)=.000, ns] on successful outcome.

In terms of behavioral performance, scores confirmed the fact that participants generally found the correct solution (≥ 75% success).

Figure 10. Percentage successfully solved the problem.

Capacity and price constraints for the sites used in the scenarios.

Site


Alberto Carraro
email: acarraro@dsi.unive.it

Antonino Salibra
email: salibra@dsi.unive.it

Antonio Bucciarelli

Minimal lambda-theories by ultraproducts

A longstanding open problem in lambda calculus is whether there exist continuous models of the untyped lambda calculus whose theory is exactly the λ β or the least sensible lambda-theory H (generated by equating all the unsolvable terms). A related question is whether, given a class of lambda models, there is a minimal lambda-theory represented by it. In this paper, we give a general tool to answer positively to this question and we apply it to a wide class of webbed models: the i-models. The method then applies also to graph models, Krivine models, coherent models and filter models. In particular, we build an i-model whose theory is the set of equations satisfied in all i-models.

If x is added by clause

Introduction

Lambda-theories are congruences on the set of λ -terms which contain β -conversion, providing (sound) notions of program equivalence. Models of the λ -calculus are one of the main tools used to study the lattice of λ -theories. Some of them, called webbed models, are built from lower level structures called "webs" (see Berline [START_REF] Berline | From computation to foundations via functions and application: the λ -calculus and its webbed models[END_REF] for an extensive survey). The simplest class of webbed models is the class of graph models, which was isolated in the seventies by Plotkin, Scott and Engeler [START_REF] Engeler | Algebras and combinators[END_REF][START_REF] Plotkin | Set-Theoretical and Other Elementary Models of the lambda-Calculus[END_REF][START_REF] Scott | Data types as lattices[END_REF] within the continuous semantics. The class of graph models contains the simplest models of λ -calculus, is itself the easiest describable class, and represents nevertheless a continuum of (non-extensional) lambdatheories. Another example of a class of webbed models, and the most established one, is the class of filter models. It was isolated at the beginning of the eighties by Barendregt, Coppo and Dezani [START_REF] Barendregt | A filter lambda model and the completeness of type assignment[END_REF], after the introduction of the intersection type discipline by Coppo and Dezani [START_REF] Coppo | An Extension of the Basic Functionality Theory for the λ -Calculus[END_REF]. Not all filter models live in Scott continuous semantics: for example some of them lack the property of representing all continuous functions, and others were introduced for the stable semantics (see Honsell-Ronchi [START_REF] Honsell | Reasoning about interpretations in qualitative lambda models[END_REF], Bastonero et al. [START_REF] Bastonero | Structures for lazy semantics[END_REF]).

In general, given a class C of models, a natural completeness problem arises for it: whether the class is complete, i.e., for any lambda-theory T there exists a member of C whose equational theory is T . A related question, raised in [START_REF] Berline | From computation to foundations via functions and application: the λ -calculus and its webbed models[END_REF] is the following: given a class C of models of the λ -calculus, is there a minimal lambda-theory represented by C ? If this is the case, we say that C enjoys the minimality property. In [START_REF] Di Gianantonio | Uncountable limits and the lambda calculus[END_REF] it was shown that the above question admits a positive answer for Scott's continuous semantics, at least if we restrict to extensional relexive CPO-models. Another result, in the same spirit, is the construction of a model whose theory is λ β η, a fortiori minimal, in the ω 1 -semantics. However, the proofs of [START_REF] Di Gianantonio | Uncountable limits and the lambda calculus[END_REF] use logical relations, and since logical relations do not allow to distinguish terms with the same applicative behavior, the proofs do not carry out to non-extensional models. Similarly, in [START_REF] Bucciarelli | Graph lambda theories[END_REF], it is shown that the class of graph models enjoys the minimality property.

In this paper, we propose a method to prove that a given class of models enjoys the minimality property, based on two main ingredients: the finite intersection property (fip) and the ultraproduct property (upp). The finite intersection property is satisfied by a class C of models if for all models M 1 , M 2 in C there exists a model M in C whose theory is included in T h(M 1 ) ∩ T h(M 2 . The ultraproduct property is satisfied in C if for every non-empty family {M i } i∈I of members of C and for every proper ultrafilter U of sets on P(I) the ultraproduct (∏ i∈I M i )/U can be embedded into a member of C . We show in Theorem 3.1 that if these conditions are satisfied, then C has the minimality property. An important technical device used in the proof of Theorem 3.1 is Lös Theorem: the ultraproduct of a family of models satisfies an (in)equation beetwen λ -terms if and only if the set of indexes of the component models satisfying it belongs to the ultrafilter. Hence, proving the minimality property boils down to exhibiting an appropriate ultrafilter.

As an application of this general method, we prove that the class of i-models introduced in [10] enjoys the minimality property. First of all, for every pair of i-models A, B we construct an i-model C such that T h(C) ⊆ T h(A) ∩ T h(B). This result is obtained via a sophisticated completion process applied to the categorical product of A and B, adapted from [START_REF] Carraro | Reflexive Scott domains are not complete for the extensional lambdacalculus[END_REF]. In order to prove that the class of i-models enjoys the ultraproduct property, we exploit the fact that i-models are webbed models. Given an ultraproduct of i-models, P, we construct the ultraproduct of the corrisponding webs, P ′ , which turns out to be a well defined web, and show that there exists an embedding of combinatory algebra from P to the i-model associated to P ′ . We also show how our proof applies to smaller classes of webbed models, like graph models, Krivine models, coherent models, and filter models.

The paper is organized as follows. In Section 2 we provide the preliminary notions and results needed in the rest of the paper, in section 3 we present the general method for showing that a given class of models of the λ -calculus has the minimality propery, and a couple of interesting corollaries of upp, and in section 4 we apply this method to the class of the i-models.

Preliminaries

Lambda-theories and models of λ -calculus

With regard to the λ -calculus we follow the notation and terminology of [START_REF] Barendregt | The Lambda calculus: Its syntax and semantics[END_REF]. By Λ and Λ o , respectively, we indicate the set of λ -terms and of closed λ -terms. We denote αβ -conversion by λ β . A λ -theory is a congruence on Λ (with respect to the operators of abstraction and application) which contains λ β . A lambda-theory is consistent if it does not equate all λ -terms, inconsistent otherwise. The set of lambdatheories constitutes a complete lattice w.r.t. inclusion, whose top is the inconsistent lambda-theory and whose bottom is the theory λ β . The lambda-theory generated by a set X of identities is the intersection of all lambda-theories containing X.

It took some time, after Scott gave his model construction, for consensus to arise on the general notion of a model of the λ -calculus. There are mainly two descriptions that one can give: the categorytheoretical and the algebraic one. Besides the different languages in which they are formulated, the two approaches are intimately connected (see Koymans [START_REF] Koymans | Models of the Lambda Calculus[END_REF]). The categorical notion of model is well-suited for constructing concrete models, while the algebraic one is rather used to understand global properties of models (constructions of new models out of existing ones, closure properties, etc.) and to obtain results about the structure of the lattice of lambda-theories.

Ultraproducts of λ -models

Reduced products result from a certain combination of the direct product and quotient constructions. They were introduced in the 1950's by Loś and the special case of ultraproducts has been a subject worthy of at least one book.

Let I be a non-empty set and let {A i } i∈I be a family of combinatory algebras. Let U be a proper ultrafilter of the boolean algebra P(I) and define a relation ∼ U given by a ∼ U b ⇔ {i ∈ I : a(i) = b(i)} ∈ U. Then θ is a congruence on the combinatory algebra ∏ i∈I A i . The ultraproduct of the family {A i } i∈I , noted (∏ i∈I A i )/U is defined as the quotient of the product ∏ i∈I A i by the congruence ∼ U . Now if all members of {A i } i∈I are λ -models, by a celebrated theorem of Loś we have that (∏ i∈I A i )/U is a λ -model too, because λ -models are axiomatized by first-order sentences. The basic combinators of the λ -model (∏ i∈I A i )/U are k ∏ i∈I A i /U and s ∏ i∈I A i /U and application is given by x/U • y/U = (x • y)/U, where the application x • y is defined pointwise.

We now recall the famous theorem Loś that we will use throughout this paper.

Theorem 2.1 (Loś). Let {A i } i∈I be a family of first-order structures indexed by a non-empty set I an let U be a proper ultrafilter of P(I). Then for every first-order L -formula ϕ(x 1 , . . . , x n ) and for every tuple (a 1 , . . . , a n ) ∈ ∏ i∈I A i we have that

( ∏ i∈I A i )/U |= ϕ(a 1 /U, . . . , a n /U) ⇔ {i ∈ I : A i |= ϕ(a 1 (i), . . . , a n (i))} ∈ U

Information systems

Information systems were introduced by Dana Scott in [START_REF] Scott | Domains for Denotational Semantics[END_REF] to give a handy representation of Scott domains. An information system is a tuple A = (A, Con A , ⊢ A , ν A ), where A is a set and ν A ∈ A, Con A ⊆ P f (A) is a downward closed family containing all singleton subsets of A, and ⊢ A ⊆ Con A × A satisfies the four axioms listed below:

(I1) if a ∈ Con A and a ⊢ A b, then a ∪ b ∈ Con A (where a ⊢ A b def = ∀β ∈ b. a ⊢ A β ) (I2) if α ∈ a, then a ⊢ A α (I3) if a ⊢ A b and b ⊢ A γ, then a ⊢ A γ (I4) / 0 ⊢ A ν A
We adopt the following notational conventions: letters α, β , γ, . . . are used for elements of A (also called tokens); letters a, b, c, . . . are used for elements of Con A , usually called consistent sets; letters x, y, z, . . . are used for arbitrary elements of P(A). We usually drop the subscripts from Con A and ⊢ A when there is no danger of confusion.

Scott proposed information systems as structures where the "backbone" of a domain is introduced by just a few axioms. Then the domain itself is defined as a certain construction from the backbone in order to define the appropriate notion of element. Scott's idea was not only to offer a simple alternative to domains, but also to continuous functions: in fact his purpose was to describe at a "lower lever" the entire category SD. For this reason he also defined an appropriate notion of morphism between information systems.

An approximable relation between two information systems A , B is a relation R ⊆ Con A × B satisfying the following properties:

(AR1) if a ∈ Con A and a R b, then b ∈ Con B (where a R b def = ∀β ∈ b. a R β ) (AR2) if a ′ ⊢ A a, a R b, and b ⊢ B β ′ , then a ′ R β ′
We will call Inf the category which has information systems as objects and approximable relations as arrows. The composition of two morphisms R ∈ Inf(A , B) and S ∈ Inf(B, C ) is (using the meta-notation) their usual relational composition:

S • R = {(a, γ) ∈ Con A × C : ∃b ∈ Con B . (a, b) ∈ R and (b, γ) ∈ S}.
The identity morphism of an information system A is ⊢ A .

The ccc structure of Inf is described in [START_REF] Scott | Domains for Denotational Semantics[END_REF], and we recall it here for the sake of self-containment. In what follows we use the projection functions fst and snd of a set-theoretic Cartesian product over the first and second component, respectively.

Definition 2.1. The Cartesian product of A and B is given by

A B = (A ⊎ B, Con, ⊢, ν) where A ⊎ B = ({ν A } × B) ∪ (A × {ν B }) ν = (ν A , ν B ) a ∈ Con iff fst * (a) ∈ Con A and snd * (a) ∈ Con B a ⊢ α iff fst * (a) ⊢ A fst(α) and snd * (a) ⊢ B snd(α)
The terminal object is the information system ⊤ whose underlying set contains only one token.

Definition 2.2. The exponentiation of B to A is given by

A ⇒ B = (A ⇒ B, Con, ⊢, ν) where A ⇒ B = Con A × B ν = ( / 0, ν B ) {(a 1 , β 1 ), . . . , (a k , β k )} ∈ Con iff ∀I ⊆ [1, k]. (∪ i∈I a i ∈ Con A ⇒ {β i : i ∈ I} ∈ Con B {(a 1 , β 1 ), . . . , (a k , β k )} ⊢ (c, γ) iff {β i : c ⊢ A a i , i ∈ [1, k]} ⊢ B γ
The categories SD and Inf are isomorphic, via a pair of mutually inverse ccc-functors (•) + : Inf → SD and (•) -: SD → Inf. In particular for an information system A , we have that A + = Inf(⊤, A ), i.e., the set of points of an information system, ordered by inclusion, is a Scott domain. Moreover the domains [A + → B + ] and A + × B + are ismorphic (in the category SD) to the domains (A ⇒ B) + and (A B) + , respectively.

Webbed models of λ -calculus

Some of the models of λ -calculus are called webbed models because they are built from lower level structures called "webs" (see Berline [START_REF] Berline | From computation to foundations via functions and application: the λ -calculus and its webbed models[END_REF][START_REF] Berline | Graph models of λ -calculus at work, and variations[END_REF] for an accurate survey). Typically a web is a set with additional structure and a webbed model is a partial order (usually a domain) whose elements are special subsets of the web. We now introduce a class of webbed models of λ -calculus arising from information systems that include many others, among which the filter models of λ -calculus living in CPO.

Let A be an information system. A subset x ⊆ A is finitely consistent if each of its finite subsets belongs to Con A . We define a partial operator (•) ↓ A : P(A) ⇀ P(A) by setting x ↓ A = {α ∈ A : ∃a ⊆ f x. a ⊢ α} if x is finitely consistent and undefined otherwise. We may drop the subscript when the underlying information system is clear from the context. Note that (•)↓ is a monotone map satisfying the following conditions: x ⊆ x ↓, x ↓ ↓= x ↓ and x ↓= ∪ a⊆ f x a ↓.

Up to a trivial isomorphism, A + = Inf(⊤, A ) is the set finitely consistent subsets x ⊆ A such that x = x ↓. Therefore use the word point to denote these latter subsets.

Let A , B be information systems and let f : A → B be a function. We define two Scott continuous functions f • : A + → B + and f • : B + → A + as follows:

f • (x) = { f (α) : α ∈ x} ↓ B ; f • (y) = {α : f (α) ∈ y} ↓ A
for every point x of A and every point y of B. We want to give simple conditions under which f can generate a continuous retraction from A + to B + : these conditions were introduced in [10].

Definition 2.3 ([10]).

Let A , B be information systems. A morphism from A to B is a function f : A → B satisfying the following property:

(Mo) a ∈ Con A iff f * (a) ∈ Con B Definition 2.4 ([10]). A morphism f : A → B is a b-morphism (resp. f-morphism) if it satisfies the following property (bMo) (resp. (fMo)) (bMo) if f * (a) ⊢ B f (α), then a ⊢ A α (fMo) if a ⊢ A α, then f * (a) ⊢ B f (α)
The "b" (resp. "f") in the name of the axiom stands for backward (resp. forward). We leave to the reader the easy relativization of the various notions of morphism given in Definition 2.4 to the case in which f is a partial map.

Proposition 2.2. Let f : A → B be a b-morphism. Then ( f • , f • ) is a retraction pair from A + into B + . Proof. From (bMo) it follows f • • f • = id A + . Definition 2.5. An i-web is a pair A = (A , φ A ) where A is

an information system and φ

A : A ⇒ A → A is a b-morphism.
The set of tokens of A is called the web of A. Proposition 2.3. Let A = (A , φ A ) be an i-web. Then A + is a reflexive object in the category SD.

Proof. As anticipated, there is a continuous isomorphism θ :

(A ⇒ A ) + → [A + → A + ]
and by Proposition 2.2 the domain (A ⇒ A ) + can be embedded into A + via the retraction pair

((φ A ) • , (φ A ) • ). Therefore (θ • (φ A ) • , θ -1 • (φ A ) • )
is the desired retraction pair in the category SD.

We set

A + = (A + , θ • (φ A ) • , θ -1 • (φ A ) • ) and call A + an i-model. Of course, since A + is a reflexive object in SD, then A + is
also a λ -model and λ -terms are interpreted as elements of A + (i.e. as points of A ) as follows:

x i A + ρ = ρ(x) λ y.M A ρ = {φ A (a, α) : α ∈ M A + ρ[y:=a↓] } ↓ A MN A ρ = {β ∈ A : ∃a ⊆ f N A + ρ . (a, β ) ∈ {(a ′ , β ′ ) : φ A (a ′ , β ′ ) ∈ M A + ρ } ↓ A⇒A }
The λ -model structure associated to the i-model A + is the following. The basic combinators are k A + = λ xy.x A + and s A + = λ xyz.xz(yz) B + , and the application operation is given by

u • v = {β ∈ A : ∃a ⊆ f v. (a, β ) ∈ {(a ′ , β ′ ) : φ A (a ′ , β ′ ) ∈ u} ↓ A⇒A }
for all points u, v.

Well-known instances of i-webs

An extended abstract type structure (EATS, for short, [13, Def. 1.1]) is a partially ordered algebra (A, ∧, →, ω), where "∧" and "→" are binary operations and "ω" is nullary one. Then the structure A = (A, P f (A), ⊢, ω), where a ⊢ α iff ( a) ≤ α, is an information system. For two

EATSs (A, ∧ A , → A , ω A ) and (B, ∧ B , → B , ω B ) a bf-morphism ψ : A → B between the corresponding information systems is a function satisfying α ≤ A α ′ iff ψ(α) ≤ B ψ(α ′ ).
Recall from [13, Def. 2.12,Thm. 2.13] that the Filter models living in the Scott semantics are obtained by taking the set of filters of EATSs satisfying the following condition:

( * ) n i=1 (α i → β i ) ≤ γ → δ , then ( i∈{i:γ≤α i } β i ) ≤ δ
In such a case, defining φ : P f (A) × A → A by φ (a, α) = ( a) → α one obtains a b-morphism and hence an i-web A = (A , φ A ) and the corresponding filter model is exactly the i-model A + (see [START_REF] Carraro | Easy lambda-terms are not always simple[END_REF] for the details).

In Larsen & Winskel [19] the definition of information system is slightly different: there is no special token ν. We remark that the corresponding class of i-models generated by the two definitions is the same. We adopt Scott's original definition just for technical reasons. With Larsen & Winskel's definition we can capture some other known classes of models, as illustrated below.

A preordered set with coherence (pc-set, for short) is a triple (A, ≤, ≎), where A is a non-empty set, ≤ is a preorder on A and ≎ is a coherence (i.e., a reflexive, symmetric relation on A) compatible with the preorder (see [START_REF] Berline | From computation to foundations via functions and application: the λ -calculus and its webbed models[END_REF]Def. 120]). A pc-set "is" an information system A = (A, P coh f (A), ⊢), where P coh f (A) is the set of finite coherent subsets of A and a ⊢ α iff ∃β ∈ a. β ≥ α. A pc-web (see [START_REF] Berline | From computation to foundations via functions and application: the λ -calculus and its webbed models[END_REF]Def. 153]) is determined by a pc-set together with a map φ :

P coh f (A) × A → A satisfying: (1) φ (a, α) ≎ φ (b, β ) iff (a ∪ b ∈ P coh f (A) ⇒ α ≎ β ) (2) if φ (a, α) ≤ φ (b, β ), then α ≤ β and (∀γ ∈ b ∃δ ∈ a.γ ≤ δ ).
A pc-web is a particular instance of i-web and properties (1),(2) say exactly that φ is a b-morphism. Krivine webs [6, Sec. 5.6.2] are pc-webs in which ≎ = A × A (so that P coh f (A) = P f (A)). Total pairs [6, Sec. 5.5] are Krivine webs in which ≤ is the equality: in fact in this the requirement of φ to be a b-morphism boils down to injectivity. Therefore a total pair is simply defined as a set A together with an injection i A : P f (A) × A → A; the underlying information system is A = (A, P f (A), ∋). The graph model associated to the total pair is then the i-model A + , obtained by taking the powerset of A (see [START_REF] Berline | From computation to foundations via functions and application: the λ -calculus and its webbed models[END_REF]Def. 120]). There is usually some ambiguity in the terminology since by "graph model" sometimes is meant the total pair (as in [START_REF] Bucciarelli | The minimal graph model of lambda calculus[END_REF], for example) underlying the model itself.

Minimal models: general results

In general, given a class C of λ -models, a natural question to be asked is whether there exists a member A of C such that Eq(A) is contained in the theories of all other members of C : one such model A is called minimal in C . This point was raised in print by C. Berline [START_REF] Berline | From computation to foundations via functions and application: the λ -calculus and its webbed models[END_REF] who was mainly referring to the classes of webbed models of λ -calculus. If a positive answer is obtained, usually it is done by purely semantical methods and Eq(A) does not need to be characterised in the syntactical sense: this is the case of Di Giannantonio et al. [START_REF] Di Gianantonio | Uncountable limits and the lambda calculus[END_REF], in which the authors prove that the class all extensional reflexive CPOs has a minimal model. Of course if one is able to gather enough information about Eq(A), then one may be in the position to answer the related completeness question for the class C : is λ β (or λ β η) a theory induced by a member of C ? An example of result of this kind can be found again in [START_REF] Di Gianantonio | Uncountable limits and the lambda calculus[END_REF], where the authors construct a model with theory λ β η in the ω 1 -semantics.

In this section we give general conditions for a class C of λ -models under which we have the guarantee that C has a minimal model. In the forthcoming section 4 we will apply this general result to the class of i-models and some of its well-known classes of models. Definition 3.1. A class C of λ -models has the finite intersection property (fip, for short) if for every two members A, B of C , there exists a member C of C such that Eq(C) ⊆ Eq(A) ∩ Eq(B).

For example the class of all λ -models has the fip, and in general every class closed under direct products has the fip. Every subclass which is axiomatized over the λ -models by first-order universal sentences has the fip, but of course these conditions do not hold in general for the classes of webbed models, e.g. for the i-models. We will see that they do hold for the filter models.

The fip is a property which is weaker than the closure under direct products. Of course a class which is closed under arbitrary (non-empty) direct products has a minimal model. The next definition isolates a property that, together with the fip, can overcome the lack of direct products and guarantee the existence of minimal models. Definition 3.2. A class C of λ -models has the ultraproduct property (upp, for short) if for every nonempty family {A i } i∈I of members of C and for every proper ultrafilter U of sets on P(I) the ultraproduct (∏ i∈I A i )/U can be embedded into a member of C .

For example the class of all λ -models has the upp, and in general every class closed under ultraproducts has the upp. Every subclass which is axiomatized over the λ -models by first-order sentences has the upp, but of course these conditions do not hold in general for the known classes of webbed models, e.g. for the i-models. Theorem 3.1. Let C be a class of λ -models having both the fip and the upp. Then C has a minimal model.

Proof. Let I be the set of all equations e betweeen closed combinatory terms for which there exists a model A in C such that A |= e. For every e ∈ I, consider the set K e = {J ⊆ f I : e ∈ J}. Since K e ∩ K e ′ = {J ⊆ f I : e, e ′ ∈ J} = / 0 for all e, e ′ ∈ I, then there exists a non-principal ultrafilter U on P f (I) containing the family (K e : e ∈ I). By the finite intersection property of the class C , for every J ⊆ f I there exists a model A J in C such that e ∈ Eq(A J ) for every e ∈ J. Let {A J } J⊆ f I be the family composed by these models and consider the ultraproduct P U = (∏ J⊆ f I A J )/U. Let e ∈ I be a closed equation and let X e = {J ⊆ f I : A J |= e}. Then X e ⊇ K e ∈ U, so that X e belongs to the ultrafilter U. Since e is a closed first-order formula, by Loś Theorem 2.1 P U |= e. Since e was an arbitrary equation in I, we have that P U |= e for every e ∈ I, so that Eq(P U ) ⊆ A∈C Eq(A). Finally, since the class C has the ultraproduct property, then there exists a model B in C such that P U embeds into B. Then Eq(B) = Eq(P U ) ⊆ A∈C Eq(A) ⊆ Eq(B) and we get the desired conclusion.

Corollary 3.2. Let C be a class of λ -models which has the fip and is closed under ultraproducts. Then C has a minimal model.

We conclude the section by giving some other general results that can be proved by just assuming the fip and the upp for a class C of λ -models. In particular we can prove a compactness theorem for lambda-theories whose equations hold in members of C . Another result that can be proved is that if there exists a λ -term that can be proved easy in C , then there exists a continuum of C -theories i.e. there are uncountably many different lambda-theories induced by models of the class C .

Theorem 3.3 (Compactness). Let C be a class of λ -models having the upp, and let E be a set of equations between closed λ -terms. If every finite subset of E is satisfied by a member of C , then E itself is satisfied by a member of C .

Proof. For every J ⊆ f E, let K J = {I ⊆ f E : J ⊆ I} and let A J ∈ C be a model satisfying J. Let U be a proper ultrafilter on P f (E) containing K J for every J ⊆ f E. Then the ultraproduct (∏ J⊆ f E A J )/U satisfies E. Finally by the upp there exists a model B in C such that (∏ J⊆ f E A J )/U embeds into B, and thus has the same lambda-theory. We conclude that B satisfies E.

Let C be a class of λ -models. A closed λ -term M is C -easy if for every closed λ -term N there exists a member B of C such that M B = N B . Theorem 3.4. Let C be a class of λ -models having the upp such that there exists a C -easy λ -term. Then there exist uncountably many C -theories.

Proof. Let M be a C -easy λ -term. For n ≥ 1, we let π n ≡ λ x 1 . . . x n .x n . We prove that for every n ≥ 1 the term Mπ n is C -easy.

Let X = (N n ) n≥1 be an arbitrary infinite sequence of closed β η-normal λ -terms and define E(X) = {Mπ n = N n : n ≥ 1}. Let K = {Mπ n 1 = N n 1 , . . . , Mπ n k = N n k } be a finite subset of E(X). Without loss of generality, we may assume that n 1 < • • • < n k . Let y be a fresh variable and define inductively

Z 1 := y I • • • I n 1 -1 N n 1 ; Z m+1 := Z m I • • • I n m+1 -n m -1 N n m Now set Z = λ y.Z k . Since M is C -easy, then there is a member A of C such that A |= M = Z. Therefore A |= Mπ n i = Zπ n i = N n i for all i = 1, . . . , k so that K ⊆ Eq(A)
. Since every finite subset of E(X) is satisfied by a member of C , then by Theorem 3.3 E(X) itself is satisfied by a member of C , i.e. there exists a member A X of C such that E(X) ⊆ Eq(A X ). Moreover if X and Y are two different infinite sequences of closed β η-normal λ -terms, then Eq(A X ) = Eq(A Y ). The result then follows from the fact that there are uncountably many infinite sequences of closed β η-normal λ -terms.

Applications

In the present section we apply the general results developed in §3. In particular we prove that the class of i-models has both the finite intersection property and the ultraproduct property. Then we comment on how these general results also apply to other well-known classes of webbed models.

Finite intersection property for i-models

The goal of the first part of this section is to prove that for every pair A 1 , A 2 of i-webs there exists an i-web B such that Eq(B + ) ⊆ Eq(A + 1 ) ∩ Eq(A + 2 ). Such result would be trivial if the categorical product A 1 A 2 could always be endowed with a suitable structure of i-web, but this is not the case. The best that we can do in general is to make A 1 A 2 into a partial i-web. A partial i-web in general is a pair A = (A , φ A ), where φ A : A ⇒ A ⇀ A is a partial b-morphism. In particular we can set

φ (a, α) =      (ν A 1 , ν A 2 ) if a ⊆ {(ν A 1 , ν A 2 )} and α = (ν A 1 , ν A 2 ) (ν A 1 , φ A 2 (snd * (a), snd(α))) if a ∪ {α} ⊆ f {ν A 1 } × A 2 (φ A 1 (fst * (a), fst(α)), ν A 2 ) if a ∪ {α} ⊆ f A 1 × {ν A 2 } obtaining that A 1 A 2 = (A 1 A 2 , φ
) is a partial i-web. A partial i-web does not give in general an imodel, but we can complete it to an i-web through a limit process that involves countably many extension steps.

We say that B is an extension of S , notation S B, if S ⊆ B, Con S = Con B ∩ P f (S), ⊢ S = ⊢ B ∩(Con S × S). We say that B is an extension of S, notation S B, if S B and φ S is the restriction of φ B to Con S × S.

Let us call B the extension of result of the (yet undefined) completion process. Of course B must be somehow related to the original i-webs A 1 and A 2 . In particular, we want that for every closed λ -term

M if (ν A 1 , β ) ∈ M B + (resp. (α, ν A 2 ) ∈ M B + ), then β ∈ M A + 2 (resp. α ∈ M A + 1
) because this will guarantee that Eq(B + ) ⊆ Eq(A + 1 ) ∩ Eq(A + 2 ). We will achieve this property by means of the notion of f-morphism of partial i-webs.

Notation. Let f : A → B be a function. We define f * : P f (B) → P f (C) and f : The following proposition explains that, in general, f-morphisms of i-webs "commute" well to the interpretation of λ -terms. We remark that the two projection functions fst and snd are f-morphisms of partial i-webs from A 1 A 2 to A 1 and A 2 , respectively.

(P f (B) × B) → (P f (C) × C) as follows: f * (b) = { f (β ) | β ∈ b, β ∈ do( f )} and f (b, β ) = ( f * (b), f (β )). Hence f * : P f (P f (B) × B) → P f (P f (C) ×C). If f is
Our goal now is to construct a series of triples {(S n , ψ 1 n , ψ 2 n )} n≥0 such that S n S n+1 and ψ i n : S n → A i (i = 1, 2) is an f-morphism of partial i-webs such that ψ i n+1 extends ψ i n (i = 1, 2). The idea is that the input parameter of the whole construction is the triple (S 0 , ψ 1 0 , ψ 2 0 ) where S 0 := A 1 A 2 , ψ 1 0 = fst, and ψ 2 0 = snd. All subsequent triples are constructed via an algorithm that, given

(S n , ψ 1 n , ψ 2 n ) as input, returns (S n+1 , ψ 1 n+1 , ψ 2 n+1
). The union of all partial i-webs and all f-morphisms of partial i-webs finally gives an i-web S ω (called completion) and two f-morphisms ψ i ω (i = 1, 2) of i-webs that allow to show that Eq(S + ω ) ⊆ Eq(A + 1 ) ∩ Eq(A + 2 ). The 0-th stage of the completion process, i.e., the triple (S 0 , ψ 1 0 , ψ 2 0 ) has already been described. Now assuming we reached stage n, we show how to carry on with stage n + 1. Definition 4.2.

• S n+1 = S n ∪ do(φ S n )

• Con S n+1 is the smallest family of sets x ⊆ f S n ∪ do(φ S n ) such that either [START_REF] Alessi | Filter Models and Easy Terms[END_REF] there exist a ∈ Con n and X ∈ Con S n ⇒S n such that X ⊆ do(φ S n ) and x = a ∪ X and ψ i n * (a) ∪

φ A i * ( ψ i n * (X)) ∈ Con A i (i = 1, 2) or (2) there exists X ∈ Con S n ⇒S n such that x ⊆ f (X ∩ do(φ S n )) ∪ (φ S n * (X ∩ do(φ S n ))) ↓ S n • a ⊢ S n+1 α iff either a ∩ S n ⊢ S n α or α ∈ a • ν S n+1 = ν S n • φ S n+1 (a, α) =      φ S n (a, α) if (a, α) ∈ do(φ S n ) (a, α) if (a, α) ∈ do(φ S n ) undefined if (a, α) ∈ (S n+1 ⇒ S n+1 ) -(S n ⇒ S n ) • for i = 1, 2 we set ψ i n+1 (α) = ψ i n (α) if α ∈ S n φ A i (ψ i n * (b), ψ i n (β )) if α = (b, β ) ∈ S n+1 -S n Theorem 4.2. We have that (i) S n+1 = (S n+1 , Con S n+1 , ⊢ S n+1 , ν S n+1 ) is an information system such that S n S n+1 , (ii) S n+1 = (S n+1 , φ S n+1 ) is a partial i-web such that S n S n+1 , (iii) ψ i n+1 : S n+1 → A i (i = 1, 2
) is an f-morphism of partial i-webs.

Proof. (i) We show that S n+1 is an information system, checking the four properties of Definition ??.

= φ A i * ( ψ i n * (X ∩ do(φ S n ))) ∪ φ A i * ( ψ i n * (X ∩ do(φ S n ))) = φ A i * ( ψ i n * (X))
This proves that ψ i n+1 * (y) ∈ Con A i . Now using property (fMo) ψ i n we obtain that ψ i n+1 * (y) ⊢ A i ψ i n+1 * (x), and hence ψ i n+1 * (x) ∈ Con A i .

(⇐) By the very definition of Con S n+1 , in particular by the clause (1).

(fMo

) Suppose a ⊢ S n+1 α. If α ∈ a, then of course ψ i n+1 * (a) ⊢ A i ψ i n+1 (α). If a ∩ S n ⊢ S n α, then ψ i n+1 * (a) = ψ i n+1 * (a -S n ) ∪ ψ i n * (a ∩ S n ) ⊢ A i ψ i n * (a ∩ S n ) ⊢ A i ψ i n (α) (iMo) Let (a, α) ∈ S n ⇒ S n . Then ψ i n+1 (φ S n+1 (a, α)) = φ A i (ψ i n * (a), ψ n (α)) = φ A i (ψ i n+1 (a), ψ i n+1 (α)
), by definition of ψ i n+1 and the fact that it extends ψ i n .

The completion of the triple

(A 1 A 2 , π 1 , π 2 ) is the triple (S ω , ψ 1 ω , ψ 2 ω )
, where S ω = (S ω , Con S ω , ⊢ S ω , ν S ω ) and S ω = (S ω , φ S ω ) are given by the following data:

S ω := m<ω S m Con S ω := m<ω Con S m ⊢ S ω := m<ω ⊢ S m ν S ω := ν A 1 A 2 φ S ω := m<ω φ S m ψ i ω := m<ω ψ i m (i = 1, 2)
Lemma 4.3. S ω is an i-web and ψ i ω : S ω → A i (i = 1, 2) is an f-morphism of i-webs.

Proof. Indeed S ω is an information system as a consequence of Theorem 4.2(i). Moreover the map φ S ω is total and it is easy to prove that it is a b-morphism from S ω ⇒ S ω using the fact that for every n the map φ S n+1 is a partial b-morphism (Theorem 4.2(ii)). Similarly one can prove that ψ i ω is an f-morphism of i-webs from S ω to A i (i = 1, 2) simply using the fact that for every n the map ψ i n is an f-morphism from the partial i-web S n to the i-webs A i (i = 1, 2) (Theorem 4.2(iii)). Theorem 4.4. Eq(S + ω ) ⊆ Eq(A + 1 ) ∩ Eq(A + 2 ).

Proof. Suppose M = N ∈ Eq(A + 1 ) ∩ Eq(A + 2 ). Suppose, w.l.o.g., that M = N ∈ Eq(A + 1 ). Then there exists

α ∈ A 1 such that α ∈ M A + 1 -N A + 2 . It is not difficult to check that α ∈ M A + 1 implies (α, ν A 2 ) ∈ M S + ω , since S ω extends A 1 A 2 . Now suppose, by way of contradiction, that (α, ν A 2 ) ∈ N S + ω . Since ψ 1 ω (α, ν A 2 ) = α, by Proposition 4.1 we have that α ∈ N A + 1 , which is a contradiction. This proves that (α, ν A 2 ) ∈ M S + ω -N S + ω , so that M = N ∈ Eq(S + ω ).
In §2.4.1 we indicate how some of the most known classes of webbed models are recovered as particular instances of i-models (more details for Filter Models are in [START_REF] Carraro | Easy lambda-terms are not always simple[END_REF]). Along these lines the notion of partial i-web generalizes those of partial pair [START_REF] Berline | From computation to foundations via functions and application: the λ -calculus and its webbed models[END_REF] (related to graph models) as well as the notions of partial webs of the other types.

The idea of partial pair and of a completion for obtaining a graph model generalizes the construction of the Engeler model and the of the Plotkin-Scott P ω model. It was initiated by Longo in [START_REF] Longo | Set-theoretical models of λ -calculus: theories, expansions, isomorphisms[END_REF] and further developed and applied by Kerth [START_REF] Kerth | Isomorphism and equational equivalence of continuous lambda models[END_REF]. Definition 4.2 is the core of a completion of i-webs that Theorem 4.6. There exists an embedding of combinatory algebras from the λ -model (∏ j∈J A + j )/U into the λ -model P + U .

Proof. We let x, y, . . . range over elements of ∏ j∈J A + j , so that x( j) ∈ A + j is a point of the graph model A j . We write x/U for the equivalence class of x w.r.t. the congruence on ∏ j∈J A + j given by x ∼ U y ⇔ { j ∈ J : x( j) = y( j)} ∈ U, i.e., x/U = {y ∈ ∏ j∈J A + j : x ∼ U y}. Recall that θ U is the relation on ∏ j∈J A j given by (α, β ) ∈ θ U ⇔ { j ∈ J : α( j) = β ( j)} ∈ U. We define a map f : (∏ j∈J A + j )/U → P + U as follows:

f (x/U) = {α/θ U : α ∈ ∏ j∈J A j , ∀ j ∈ J. α( j) ∈ x( j)}

It is easy to show that the definition of f is independent of the choice of the representatives of ∼ Uequivalence classes as, for all y ∈ x/U, we have { j ∈ J : y( j) = x( j)} ∈ U.

We prove that f is injective. Suppose x/U = y/U and let Z = { j ∈ J : x( j) = y( j)}. Define X = {k ∈ J : x(k) ⊆ y(k)} and Y = {k ∈ J : y(k) ⊆ x(k)}. Then X ∩Y = Z ∈ U. This means that it is not possible that both X and Y belong to the ultrafilter U. Assume that X ∈ U. Then for every k ∈ J -X we have x(k) ⊆ y(k), so that for each k ∈ J -X there exists an element γ k ∈ A k such that γ k ∈ x(k)y(k). Let δ ∈∈ ∏ j∈J A j be an arbitrary sequence and let β ∈ ∏ j∈J A j be defined by β (i) = γ i for i ∈ J -X and β (i) = δ (i) for i ∈ J -X. By definition of f we have β /θ U ∈ f (x/U), while β /θ U ∈ f (y/U), so that f (x/U) = f (y/U). Now we prove that f is homomorphism of combinatory algebras. We start proving that f preserves application. We have f (x/U) • f (y/U) = {α/θ U : α ∈ ∏ j∈J A j , ∃a/θ U ⊆ f f (y/U). φ P U (a/θ U , α/θ U ) ∈ f (x/U)} = {α/θ U : α ∈ ∏ j∈J A j , ∃a ⊆ f ∏ j∈J A j .∀γ ∈ a.∀ j ∈ J. γ( j) ∈ y( j) ∧ ∀i ∈ J. φ A i (a(i), α(i)) ∈ x(i)} = {α/θ U : α ∈ ∏ j∈J A j , ∀ j ∈ J.∃a ⊆ f y( j). φ A j (a, α( j)) ∈ x( j)} = {α/θ U : α ∈ ∏ j∈J A j , ∀ j ∈ J. α( j) ∈ {β ∈ A j : ∃a ⊆ f y( j). φ A j (a, β ) ∈ x( j)}} = {α/θ U : α ∈ ∏ j∈J A j , ∀ j ∈ J. α( j) ∈ x( j) • y( j)} = f ((x • y)/U) = f (x/U • y/U)

We now regard the basic combinators. Recall that by definition for each j ∈ J we have k A + j = λ xy.x A + j = {φ A j (a, φ A j (b, β )) : β ∈ a}. Then

f (k (∏ j∈J A + j )/U ) = f ((k ∏ j∈J A + j )/U) = {α/θ U : α ∈ ∏ j∈J A j , ∀ j ∈ J. α( j) ∈ k A + j } = {φ P U (a/θ U , φ P U (b/θ U , β /θ U )) : β /θ U ∈ a/θ U } = λ xy.x P + U = k P + U Similarly f (s (∏ j∈J A + j )/U ) = s P + U .
We remark that in the general case in which all the A j ( j ∈ J) and P U are i-webs the map f : (∏ j∈J A + j )/U → P + U is defined as f (x/U) = {α/θ U : α ∈ ∏ j∈J A j , ∀ j ∈ J. α( j) ∈ x( j)} ↓ P U . We commented at the end of §4.2 that the fip can be derived for subclasses by suitably modifying the general construction detailed for i-models. Also the upp holds vor the various classes of models. Here

  a partial function, we write do( f ) to indicate the domain of f . Definition 4.1 ([10]). Let B, C be partial i-webs. An f-morphism from B to C is an f-morphism ψ : B → C satisfying the following additional property: (iMo) if (a, β ) ∈ do(φ B ), then (ψ * (a), ψ(β )) ∈ do(φ C ) and ψ(φ B (a, β )) = φ C (ψ * (a), ψ(β ))

Proposition 4 . 1 (

 41 [START_REF] Carraro | Reflexive Scott domains are not complete for the extensional lambdacalculus[END_REF]). Let B, C be i-webs, let ψ : B → C be an f-morphism of i-webs, and let M be a closed λ -term. If α ∈ M B + , then ψ(α) ∈ M C + .

(I1) Suppose a ∈ Con S n+1 and a ⊢ S n+1 b. If a has been added to Con S n+1 by clause [START_REF] Alessi | Filter Models and Easy Terms[END_REF], then exists i ∈ {1, 2}, a ′ ∈ Con S n and X ∈ Con S n ⇒S n such that X ⊆ do(φ S n ) and a = a ′ ∪ X and ψ i n * (a ′ ) ∪

Therefore b is added to Con S n+1 by clause [START_REF] Alessi | Filter Models and Easy Terms[END_REF].

If a has been added to Con S n+1 by clause [START_REF] Baeten | Omega can be anything it should not be[END_REF], then also b is added to Con S n+1 by the same clause.

(I2) If α ∈ a, then a ⊢ S n+1 α by definition of ⊢ S n+1 .

(I3) Suppose a ⊢ S n+1 {α 1 , . . . , α k } and {α 1 , . . . , α k } ⊢ S n+1 γ. If γ ∈ {α 1 , . . . , α k } then clearly a ⊢ S n+1 γ.

Otherwise {α 1 , . . . , α k } ∩ S n ⊢ S n γ and since a ∩ S n ⊢ S n {α 1 , . . . , α k } ∩ S n we can conclude using the property (I3) of S n .

(I4) Immediate.

Finally it is immediate to see that S n S n+1 .

(ii) Note that the fact that S n S n+1 automatically implies S n ⇒ S n S n+1 ⇒ S n+1 . Now we prove that φ S n+1 : S n ⇒ S n → S n+1 is a total b-morphism, so that it is automatically a partial b-morphism from

). Now we have

) and since both φ A i and ψ i n are morphisms of information systems, then so is their composition

(iii) Now we prove that ψ i n+1 (i = 1, 2) is an f-morphism of i-webs. (Mo) (⇒) Suppose x ∈ Con S n+1 . We consider the clauses (1) and (2) of the definition of Con S n+1 .

If x is added by clause (1), i.e. x = a ∪ X for suitable a and X, then

further generalizes Longo and Kerth's work. As such, it can be adapted case by case so that the entire completion adapts to the various instances of i-webs in the sense that if we start with partial pair, at the end we obtain a total pair, if we start with a partial pcs-web, we end up in a total pcs-web etc. Of course Theorem 4.4 proves the finite intersection property for the class of i-models, but in view of the above discussion it can also give proofs of the finite intersection property for the sublcasses of models mentioned in section 2.4.1.

For the particular case of graph models the fip was proved by Bucciarelli&Salibra [START_REF] Bucciarelli | Graph lambda theories[END_REF][START_REF] Bucciarelli | The minimal graph model of lambda calculus[END_REF], via a construction that they call weak product which has the same spirit of our completion method. For the other classes of models the fip was not known to hold. For the particular case of filter models one may prove the fip as a simple consequence of the closure of filter models under the contruction of direct products, a result that does not appear in the literature and we do not sketch here.

Ultraproduct property for i-models

In this subsection we deal with the ultraproduct property for the class of i-models: for every non-empty family {A i } i∈I of i-webs and every ultrafilter U on P(I) the ultraproduct (∏ i∈I A + i )/U can be embedded into an i-model.

Let J be a non-empty set and let {A j } j∈J be a family of information systems and let U be a proper ultrafilter on P(J). Define a binary relation θ U on ∏ j∈J A j by setting (α,

Note that θ U is an equivalence relation on ∏ j∈J A j . As a matter of notation, for every finite subset a ⊆ f ∏ j∈J A j , we let a/θ U = {α/θ U : α ∈ a}, i.e., a/θ U is the finite subset of (∏ j∈J A j )/θ U constituted by the θ U -equivalence classes of the tokens of a. Since each element α ∈ a is a J-indexed sequence, we denote by α( j) the j-th projection of α and we let a( j) = {α( j) : α ∈ a}. Definition 4.3. We define an information system P U = (P U , Con U , ⊢ U , ν U ) as follows:

We also define an i-web P U = (P U , φ P U ) by setting φ P U (a/θ U , α/θ U ) = (λ λ j.φ A j (a( j), α( j)))/θ U .

We leave to the reader the easy verification of the fact that P U and P U indeed are an information system and an i-web, respectively.

We conclude the second main theorem of the section, the one that deals with the ultraproduct property. Let {A j } j∈J be a family of i-webs, let U be an ultrafilter over P(J) and let P U be the i-web of Definition 4.3. Since P U is an i-web, then P + U is a reflexive Scott domain and hence a λ -model. On the other hand each i-web A j gives rise to a reflexive Scott domain A + j , which is a λ -model. Then (∏ j∈J A + j )/U is an ultraproduct of λ -models, and thus again a λ -model. Theorem 4.5. There exists an embedding of combinatory algebras from the λ -model (∏ j∈J A + j )/U into the λ -model P + U . The proof of Theorem 4.5 is rather technical and cumbersome. For this reason we state and prove a particular case of Theorem 4.5 that only deals with graph models; the proof will appear clear and readable, and at the same time gives the core idea about the proof of the more genereal result.

we proved it for graph models, because it looks it looks very clear for this case, but the proof can be adapted (adding details and complication) to the other cases.

Summing up, graph models, pcs-models, Krivine models, filter models and in general i-models have both the fip and the upp. For this reason Theorem 3.1 applies to all these classes, producing a minimal model in each case. It is known that there exist filter-easy terms [START_REF] Alessi | Filter Models and Easy Terms[END_REF] as well as graph-easy terms [START_REF] Baeten | Omega can be anything it should not be[END_REF] (for example (λ x.xx)(λ x.xx)), and every graph-easy term is also pcs-easy and Krivine-easy, since the latter classes contain the graph models. Therefore Theorem 3.3 and Theorem 3.4 both hold for all these classes, saying that each one of them induces a continuum of lambda-theories.

Conclusions

We have presented a method for proving that a given class of models of the λ -calculus possesses a minimal element, i.e. an element whose λ -theory is the intersection of all the λ -theories represented in the class.

Then, we have applied this method to the class of i-models, a subclass of Scott models defined in [START_REF] Carraro | Reflexive Scott domains are not complete for the extensional lambdacalculus[END_REF], containing several well-known instances of "webbed" models like the graph-models and the filter models living in the category of Scott domains.

Various extensions of this work can be explored, both toward the proof that the whole class of Scott models has the minimality property, and more generally toward the application of the method to other classes of models of the λ -calculus.

Concerning the former extension, a preliminary result would be the finite intersection property for the whole class of Scott models, the completion method described in section 4 being adapted to i-models.

More generally, it is interesting to notice that webs, even beyond i-webs, are first-order axiomatisable, hence closed by ultraproducts (by the way, this observation is an alternative way of showing that Definition 4.3 is sound).

By providing a first-order axiomatisation of sentences like A + M = N, for given terms M, M and web A, we could invoke Los theorem for showing that (∏ j∈J A j )/θ U ) + and (∏ j∈J A + j )/U have the same theory, and hence for deriving a strong form of the ultraproduct property for the class of models corresponding to the considered webs.