1,720,971 research outputs found
An integrated low-cost system for object detection in underwater environments
Full text linkWe propose a novel low-cost integrated system prototype able to recognize objects/lifeforms in underwater environments. The system has been applied to detect unexploded ordnance materials in shallow waters. Indeed, small and agile remotely controlled vehicles with cameras can be used to detect unexploded bombs in shallow waters, more effectively and freely than complex, costly and heavy equipment, requiring several human operators and support boats. Moreover, visual techniques can be easily combined with the traditional use of magnetometers and scanning imaging sonars, to improve the effectiveness of the survey. The proposed system can be easily adapted to other scenarios (e.g., underwater archeology or visual inspection of underwater pipelines and implants), by simply replacing the Convolutional Neural Network devoted to the visual identification task. As a final outcome of our work we provide a large dataset of images of explosive materials: it can be used to compare different visual techniques on a common basis
Principal types as partial involutions
No full textWe show that the principal types of the closed terms of the affine fragment of λ-calculus, with respect to a simple type discipline, are structurally isomorphic to their interpretations, as partial involutions, in a natural Geometry of Interaction model à la Abramsky. This permits to explain in elementary terms the somewhat awkward notion of linear application arising in Geometry of Interaction, simply as the resolution between principal types using an alternate unification algorithm. As a consequence, we provide an answer, for the purely affine fragment, to the open problem raised by Abramsky of characterizing those partial involutions which are denotations of combinatory terms
Two Views on Unification: Terms as Strategies
Full text linkIn previous works, the authors have shown that linear application in Geometry of Interaction (GoI) models of lambda-calculus amounts to resolution between principal types of linear lambda-terms. This analogy also works in the reverse direction. Indeed, an alternative definition of unification between algebraic terms can be given by viewing the terms to be unified as strategies, i.e. sets of pairs of occurrences of the same variable, and verifying the termination of the GoI interaction obtained by playing the two strategies. In this paper we prove that such a criterion of unification is equivalent to the standard one. It can be viewed as a local, bottom-up, definition of unification. Dually, it can be understood as the GoI interpretation of unification.
The proof requires generalizing earlier work to arbitrary algebraic constructors and allowing for multiple occurrences of the same variable in terms
Oceanus: A context-aware low-cost navigation aid for yacht racing
No full textOceanus is a hardware and software platform designed and developed to provide useful information to the crew of a racing yacht. The key features of the proposed solution are its reliability, the possibility to extend and customise it, and its context-awareness, which simplifies its usage in an intelligent way. The target users of the system are both beginners who want a navigation aid, but cannot afford the expensive and often overly complicated commercial systems available on the market, and more experienced sailors who can benefit from an open and customisable instrument to study and fine-tune the setup and performance of their sailing boats. Furthermore, Oceanus strives to be as much as possible a low-cost architecture, both in software and hardware requirements
Acquisition and integration of differential pressure measurements on sails for boat performances improvement
Full text linkIn this paper, we integrated within a specifically developed acquisition system, denoted as Oceanus, the measurements from a differential pressure sensor between the two sides of a sail (windward and leeward sides); experiments have been performed using a light jib sail of a 35 feet cruising-racing yacht. We analyzed the correlation between such a signal and other standard signals usually present on board such as boat speed, intensity and direction of apparent or real wind; moreover, data from Inertial Measurement Units are handled. We also considered the Target Data, which depend on the actual point of sail, and the discrepancy between measured data and the predicted Targets is monitored as an error in terms of the true wind angle and boat velocity. In this way, the trimmer/helmsman can monitor the differential sail pressure together with Target data and decide to reduce the error with a correction in how sails are trimmed, rather than in how the boat is steered to achieve an improvement of boat performances. The resulting telemetry system represents an effective low cost solution, which is affordable even for amateur yachtsmen
The involutions-as-principal types/ application-as-unification analogy
Full text linkIn 2005, S. Abramsky introduced various universal models of computation based on Affine Combinatory Logic, consisting of partial involutions over a suitable formal language of moves, in order to discuss reversible computation in a game-theoretic setting. We investigate Abramsky’s models from the point of view of the model theory of λ-calculus, focusing on the purely linear and affine fragments of Abramsky’s Combinatory Algebras. Our approach stems from realizing a structural analogy, which had not been hitherto pointed out in the literature, between the partial involution interpreting a combinator and the principal type of that term, with respect to a simple types discipline for λ-calculus. This analogy allows for explaining as unification between principal types the somewhat awkward linear application of involutions arising from Geometry of Interaction (GoI). Our approach provides immediately an answer to the open problem, raised by Abramsky, of characterising those finitely describable partial involutions which are denotations of combinators, in the purely affine fragment. We prove also that the (purely) linear combinatory algebra of partial involutions is a (purely) linear λ-algebra, albeit not a combinatory model, while the (purely) affine combinatory algebra is not. In order to check the complex equations involved in the definition of affine λ-algebra, we implement in Erlang the compilation of λ-terms as involutions, and their execution
Λ-Symsym: An Interactive Tool for Playing with Involutions and Types
Full text linkWe present the web portal Λ-symsym, available at http://158.110.146.197:31780/automata/, for experimenting with game semantics of λ^!-calculus, and its normalizing elementary sub-calculus, the λ^{EAL}-calculus. The λ^!-calculus is a generalization of the λ-calculus obtained by introducing a modal operator !, giving rise to a pattern β-reduction. Its sub-calculus corresponds to an applicatively closed class of terms normalizing in an elementary number of steps, in which all elementary functions can be encoded. The game model which we consider is the Geometry of Interaction model I introduced by Abramsky to study reversible computations, consisting of partial involutions over a very simple language of moves.
Given a λ^!- or a λ^{EAL}-term, M, Λ-symsym provides:
- an abstraction algorithm A^!, for compiling M into a term, A^!(M), of the linear combinatory logic CL^{!}, or the normalizing combinatory logic CL^{EAL};
- an interpretation algorithm [[ ]]^I yielding a specification of the partial involution [[A^!(M)]]^I in the model I;
- an algorithm, I2T, for synthesizing from [[A^!(M)]]^I a type, I2T([[A^!(M)]]^I), in a multimodal, intersection type assignment discipline, ⊢_!.
- an algorithm, T2I, for synthesizing a specification of a partial involution from a type in ⊢_!, which is an inverse to the former. We conjecture that ⊢_! M : I2T([[A^!(M)]]^I). Λ-symsym permits to investigate experimentally the fine structure of I, and hence the game semantics of the λ^!- and λ^{EAL}-calculi. For instance, we can easily verify that the model I is a λ^!-algebra in the case of strictly linear λ-terms, by checking all the necessary equations, and find counterexamples in the general case.
We make this tool available for readers interested to play with games (-semantics). The paper builds on earlier work by the authors, the type system being an improvement
MAV-Link-Based Control and Coordination of a Multi-Drone Cluster for Intelligence, Surveillance and Reconnaissance Tasks
No full textResearch on drone systems is expanding rapidly and finds application in many fields. These systems provide powerful and precise means in several domains from surveillance to agriculture. If we look inside a drone system, we will find several parts: the aerial vehicle(s), the onboard sensors, a computing device, and the autopilot, a communication network, a ground control station, control software, and a security module, encrypting commands and messages. In a multi-drone application, the system becomes more complex and coordination along with synchronization of the Unmanned Aerial Vehicles (UAVs) forms the strategic parts of the whole system. This manuscript focuses on an Intelligence, Surveillance and Reconnaissance (ISR) application and investigates a complete HW/SW architecture for a number of deployments where the secure control architecture is based on theMAVLink protocol for automatic control of the UAVs fully enabled by audio and video acquisition and processing. Indeed, one of the key features and novelties introduced by this proposal is the combined use of audio and video inputs, in order to provide amore precise and robust detection of targets and the related reaction of the system. The proposed system setup, user control scheme, ciphering and synchronization methods, and the related experiments are explored for laying the basis for future ideas and developments
- …
