Abstract We introduce the notion of reflexivity for combinatory algebras. Reflexivity can be thought of as an equational counterpart of the Meyer–Scott axiom of combinatory models, which indeed allows us to characterize an equationally definable counterpart of combinatory models. This new structure, called strongly reflexive combinatory algebra, admits a finite axiomatization with seven closed equations, and the structure is shown to be exactly the retract of combinatory models. Lambda algebras can be characterized as strongly reflexive combinatory algebras that are stable. Moreover, there is a canonical construction of a lambda algebra from a strongly reflexive combinatory algebra. The resulting axiomatization of lambda algebras by the seven axioms for strong reflexivity together with those for stability is shown to correspond to the axiomatization of lambda algebras due to Selinger (2002, J. Funct. Program., 12, 549–566).

Automated driving systems(ADS) are major trend and the safety of such critical system has become one of the most important research topics. We usually use scenarios in order to define the specifications of ADS. In these scenarios, graphical diagrams are often used to represent abstractly the positioning and behavior of vehicles. However, such diagrams are not suitable for the development of high-reliability systems, because they are informal and may cause discrepancies among different engineers. In this paper, we propose a formal speci-fication language called Bounding Box Specification Language (BBSL) which allows us to write rigorous specifications of ADS. BBSL describe multiple types of objects in a driving environment, such as vehicles and pedestrians, as bounding boxes defined as two-dimensional interval, and describe positional relationships between them in mathematical notation. It is capable of strictly delineating many positional relationships while being also capable of expressing specifications that are concise enough to be read and written manually. Therefore, BBSL is suitable for describing the specification of Object and Event Detection and Response (OEDR) among the tasks of ADS. In this paper, we describe what kind of description BBSL enables, and describe its operations. Then, we show examples of specifications of ADS written in BBSL and discuss the advantages of specifications written in BBSL.

We investigate powerspace constructions on topological spaces, with a particular focus on the category of quasi-Polish spaces. We show that the upper and lower powerspaces commute on all quasi-Polish spaces, and show more generally that this commutativity is equivalent to the topological property of consonance. We then investigate powerspace constructions on the open set lattices of quasi-Polish spaces, and provide a complete characterization of how the upper and lower powerspaces distribute over the open set lattice construction.

We extend the notion of localic completion of generalised metric spaces by Steven Vickers to the setting of generalised uniform spaces. A generalised uniform space (gus) is a set X equipped with a family of generalised metrics on X, where a generalised metric on X is a map from the product of X to the upper reals satisfying zero self-distance law and triangle inequality. For a symmetric generalised uniform space, the localic completion lifts its generalised uniform structure to a point-free generalised uniform structure. This point-free structure induces a complete generalised uniform structure on the set of formal points of the localic completion that gives the standard completion of the original gus with Cauchy filters. We extend the localic completion to a full and faithful functor from the category of locally compact uniform spaces into that of overt locally compact completely regular formal topologies. Moreover, we give an elementary characterisation of the cover of the localic completion of a locally compact uniform space that simplifies the existing characterisation for metric spaces. These results generalise the corresponding results for metric spaces by Erik Palmgren. Furthermore, we show that the localic completion of a symmetric gus is equivalent to the point-free completion of the uniform formal topology associated with the gus. We work in Aczel's constructive set theory CZF with the Regular Extension Axiom. Some of our results also require Countable Choice. Comment: 39 pages

We show that the category of basic pairs (BP) and the category of concrete spaces (CSpa) are both small-complete and small-cocomplete in the framework of constructive Zermelo–Frankel set theory extended with the set generation axiom. We also show thatCSpais a coreflective subcategory ofBP.