arXiv subjects

Margherita Zorzi

Publications and source records attributed to Margherita Zorzi.

16 recordsLinked to original sources

arXiv2024

Compositional theories for host-core languages

Linear type theories, of various types and kinds, are of fundamental importance in most programming language research nowadays. In this paper we describe an extension of Benton's Linear-Non-Linear type theory and model for which we can prove some extra properties that make the system better behaved as far as its theory is concerned. We call this system the host-core type theory. The syntax of a host-core language is split into two parts, representing respectively a host language H and a core language C, embedded in H. This idea, derived from Benton's Linear-Non-Linear formulation of Linear Logic, allows a flexible management of data linearity, which is particularly useful in non-classical computational paradigms. The host-core style can be viewed as a simplified notion of multi-language programming, the process of software development in a heterogeneous programming language. In this paper, we present the typed calculus HC, a minimal and flexible host-core system that captures and standardizes common properties of an ideal class of host-core languages. We provide a denotational model in terms of enriched categories and we state a strong correspondence between syntax and semantics through the notion of internal language. The latter result provides some useful characterizations of host-core style, otherwise difficult to obtain. We also discuss some concrete instances, extensions and specializations of the system HC.

cs.LO↗

arXiv2021

From 2-sequents and Linear Nested Sequents to Natural Deduction for Normal Modal Logics

We extend to natural deduction the approach of Linear Nested Sequents and of 2-sequents. Formulas are decorated with a spatial coordinate, which allows a formulation of formal systems in the original spirit of natural deduction -- only one introduction and one elimination rule per connective, no additional (structural) rule, no explicit reference to the accessibility relation of the intended Kripke models. We give systems for the normal modal logics from K to S4. For the intuitionistic versions of the systems, we define proof reduction, and prove proof normalization, thus obtaining a syntactical proof of consistency. For logics K and K4 we use existence predicates (following Scott) for formulating sound deduction rules.

cs.LO↗

arXiv2020

A journey in modal proof theory: From minimal normal modal logic to discrete linear temporal logic

Extending and generalizing the approach of 2-sequents (Masini, 1992), we present sequent calculi for the classical modal logics in the K, D, T, S4 spectrum. The systems are presented in a uniform way-different logics are obtained by tuning a single parameter, namely a constraint on the applicability of a rule. Cut-elimination is proved only once, since the proof goes through independently from the constraints giving rise to the different systems. A sequent calculus for the discrete linear temporal logic ltl is also given and proved complete. Leitmotiv of the paper is the formal analogy between modality and first-order quantification.

cs.LO↗

arXiv2019

Quantum Programming Made Easy

We present IQu, namely a quantum programming language that extends Reynold's Idealized Algol, the paradigmatic core of Algol-like languages. IQu combines imperative programming with high-order features, mediated by a simple type theory. IQu mildly merges its quantum features with the classical programming style that we can experiment through Idealized Algol, the aim being to ease a transition towards the quantum programming world. The proposed extension is done along two main directions. First, IQu makes the access to quantum co-processors by means of quantum stores. Second, IQu includes some support for the direct manipulation of quantum circuits, in accordance with recent trends in the development of quantum programming languages. Finally, we show that IQu is quite effective in expressing well-known quantum algorithms.

cs.LO↗

arXiv2019

It could be worse, it could be raining: reliable automatic meteorological forecasting

Meteorological forecasting provides reliable prediction about the future weather within a given interval of time. Meteorological forecasting can be viewed as a form of hybrid diagnostic reasoning and can be mapped onto an integrated conceptual framework. The automation of the forecasting process would be helpful in a number of contexts, in particular: when the amount of data is too wide to be dealt with manually; to support forecasters education; when forecasting about underpopulated geographic areas is not interesting for everyday life (and then is out from human forecasters' tasks) but is central for tourism sponsorship. We present logic MeteoLOG, a framework that models the main steps of the reasoner the forecaster adopts to provide a bulletin. MeteoLOG rests on several traditions, mainly on fuzzy, temporal and probabilistic logics. On this basis, we also introduce the algorithm Tournament, that transforms a set of MeteoLOG rules into a defeasible theory, that can be implemented into an automatic reasoner. We finally propose an example that models a real world forecasting scenario.

cs.AI↗

arXiv2018

QPCF: higher order languages and quantum circuits

qPCF is a paradigmatic quantum programming language that ex- tends PCF with quantum circuits and a quantum co-processor. Quantum circuits are treated as classical data that can be duplicated and manipulated in flexible ways by means of a dependent type system. The co-processor is essentially a standard QRAM device, albeit we avoid to store permanently quantum states in between two co-processor's calls. Despite its quantum features, qPCF retains the classic programming approach of PCF. We introduce qPCF syntax, typing rules, and its operational semantics. We prove fundamental properties of the system, such as Preservation and Progress Theorems. Moreover, we provide some higher-order examples of circuit encoding.

cs.LO↗

arXiv2017

Automagically encoding Adverse Drug Reactions in MedDRA

Pharmacovigilance is the field of science devoted to the collection, analysis and prevention of Adverse Drug Reactions (ADRs). Efficient strategies for the extraction of information about ADRs from free text resources are essential to support the work of experts, employed in the crucial task of detecting and classifying unexpected pathologies possibly related to drug assumptions. Narrative ADR descriptions may be collected in several way, e.g. by monitoring social networks or through the so called spontaneous reporting, the main method pharmacovigilance adopts in order to identify ADRs. The encoding of free-text ADR descriptions according to MedDRA standard terminology is central for report analysis. It is a complex work, which has to be manually implemented by the pharmacovigilance experts. The manual encoding is expensive (in terms of time). Moreover, a problem about the accuracy of the encoding may occur, since the number of reports is growing up day by day. In this paper, we propose MagiCoder, an efficient Natural Language Processing algorithm able to automatically derive MedDRA terminologies from free-text ADR descriptions. MagiCoder is part of VigiWork, a web application for online ADR reporting and analysis. From a practical view-point, MagiCoder radically reduces the revision time of ADR reports: the pharmacologist has simply to revise and validate the automatic solution versus the hard task of choosing solutions in the 70k terms of MedDRA. This improvement of the expert work efficiency has a meaningful impact on the quality of data analysis. Moreover, our procedure is general purpose. We developed MagiCoder for the Italian pharmacovigilance language, but preliminarily analyses show that it is robust to language and dictionary changes.

cs.CL↗

arXiv2016

From narrative descriptions to MedDRA: automagically encoding adverse drug reactions

The collection of narrative spontaneous reports is an irreplaceable source for the prompt detection of suspected adverse drug reactions (ADRs): qualified domain experts manually revise a huge amount of narrative descriptions and then encode texts according to MedDRA standard terminology. The manual annotation of narrative documents with medical terminology is a subtle and expensive task, since the number of reports is growing up day-by-day. MagiCoder, a Natural Language Processing algorithm, is proposed for the automatic encoding of free-text descriptions into MedDRA terms. MagiCoder procedure is efficient in terms of computational complexity (in particular, it is linear in the size of the narrative input and the terminology). We tested it on a large dataset of about 4500 manually revised reports, by performing an automated comparison between human and MagiCoder revisions. For the current base version of MagiCoder, we measured: on short descriptions, an average recall of $86\%$ and an average precision of $88\%$; on medium-long descriptions (up to 255 characters), an average recall of $64\%$ and an average precision of $63\%$. From a practical point of view, MagiCoder reduces the time required for encoding ADR reports. Pharmacologists have simply to review and validate the MagiCoder terms proposed by the application, instead of choosing the right terms among the 70K low level terms of MedDRA. Such improvement in the efficiency of pharmacologists' work has a relevant impact also on the quality of the subsequent data analysis. We developed MagiCoder for the Italian pharmacovigilance language. However, our proposal is based on a general approach, not depending on the considered language nor the term dictionary.

cs.CL↗

arXiv2015

Wave-Style Token Machines and Quantum Lambda Calculi

Particle-style token machines are a way to interpret proofs and programs, when the latter are written following the principles of linear logic. In this paper, we show that token machines also make sense when the programs at hand are those of a simple quantum lambda-calculus with implicit qubits. This, however, requires generalising the concept of a token machine to one in which more than one particle travel around the term at the same time. The presence of multiple tokens is intimately related to entanglement and allows us to give a simple operational semantics to the calculus, coherently with the principles of quantum computation.

cs.LO↗

arXiv2013

Wave-Style Token Machines and Quantum Lambda Calculi (Long Version)

Particle-style token machines are a way to interpret proofs and programs, when the latter are defined according to the principles of linear logic. In this paper, we show that token machines also make sense when the programs at hand are those of a simple linear quantum $λ$-calculus. This, however, requires generalizing the concept of a token machine to one in which more than one particle can possibly travel around the term at the same time. This is intimately related to entanglement and allows to give a simple operational semantics to the calculus coherently with the principles of quantum computation.

cs.LO↗

arXiv2012

Interactive Realizability and the elimination of Skolem functions in Peano Arithmetic

We present a new syntactical proof that first-order Peano Arithmetic with Skolem axioms is conservative over Peano Arithmetic alone for arithmetical formulas. This result - which shows that the Excluded Middle principle can be used to eliminate Skolem functions - has been previously proved by other techniques, among them the epsilon substitution method and forcing. In our proof, we employ Interactive Realizability, a computational semantics for Peano Arithmetic which extends Kreisel's modified realizability to the classical case.

cs.LO↗

arXiv2011

Probabilistic Operational Semantics for the Lambda Calculus

Probabilistic operational semantics for a nondeterministic extension of pure lambda calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics are both inductively and coinductively defined. Moreover, small-step and big-step semantics are shown to produce identical outcomes, both in call-by- value and in call-by-name. Plotkin's CPS translation is extended to accommodate the choice operator and shown correct with respect to the operational semantics. Finally, the expressive power of the obtained system is studied: the calculus is shown to be sound and complete with respect to computable probability distributions.

cs.LO↗

arXiv2010

General Ramified Recurrence is Sound for Polynomial Time

Leivant's ramified recurrence is one of the earliest examples of an implicit characterization of the polytime functions as a subalgebra of the primitive recursive functions. Leivant's result, however, is originally stated and proved only for word algebras, i.e. free algebras whose constructors take at most one argument. This paper presents an extension of these results to ramified functions on any free algebras, provided the underlying terms are represented as graphs rather than trees, so that sharing of identical subterms can be exploited.

cs.LO↗

arXiv2009

Confluence Results for a Quantum Lambda Calculus with Measurements

A strong confluence result for Q*, a quantum lambda-calculus with measurements, is proved. More precisely, confluence is shown to hold both for finite and infinite computations. The technique used in the confluence proof is syntactical but innovative. This makes Q* different from similar quantum lambda calculi, which are either measurement-free or provided with a reduction strategy.

cs.LO↗

arXiv2008

A Qualitative Modal Representation of Quantum Register Transformations

We introduce two modal natural deduction systems that are suitable to represent and reason about transformations of quantum registers in an abstract, qualitative, way. Quantum registers represent quantum systems, and can be viewed as the structure of quantum data for quantum operations. Our systems provide a modal framework for reasoning about operations on quantum registers (unitary transformations and measurements), in terms of possible worlds (as abstractions of quantum registers) and accessibility relations between these worlds. We give a Kripke--style semantics that formally describes quantum register transformations and prove the soundness and completeness of our systems with respect to this semantics.

cs.LO↗

arXiv2007

Quantum Lambda Calculi with Classical Control: Syntax and Expressive Power

We study an untyped lambda calculus with quantum data and classical control. This work stems from previous proposals by Selinger and Valiron and by Van Tonder. We focus on syntax and expressiveness, rather than (denotational) semantics. We prove subject reduction, confluence and a standardization theorem. Moreover, we prove the computational equivalence of the proposed calculus with a suitable class of quantum circuit families.

cs.LO↗