Inputs, Outputs, and Composition in the Logic of Information Flows

TL;DR

This paper advances the logic of information flows by defining inputs and outputs, analyzing their relationship, and exploring the expressive power of sequential composition, connecting LIF to first-order logic.

Contribution

It introduces semantic and syntactic definitions of inputs and outputs in LIF and studies the expressive power of sequential composition, linking LIF to first-order logic.

Findings

Semantic and syntactic definitions of inputs and outputs in LIF

Optimality of the syntactic definition of inputs and outputs

Relationship between LIF, FO, and bounded-variable FO

Abstract

The logic of information flows (LIF) is a general framework in which tasks of a procedural nature can be modeled in a declarative, logic-based fashion. The first contribution of this paper is to propose semantic and syntactic definitions of inputs and outputs of LIF expressions. We study how the two relate and show that our syntactic definition is optimal in a sense that is made precise. The second contribution is a systematic study of the expressive power of sequential composition in LIF. Our results on composition tie in the results on inputs and outputs, and relate LIF to first-order logic (FO) and bounded-variable LIF to bounded-variable FO.