Completeness for Two Left-Sequential Logics
Daan Staudt
Abstract:
Left-sequential logics provide a means for reasoning about (closed)
propositional terms with atomic propositions that may have side
effects and that are evaluated sequentially from left to right. Such
propositional terms are commonly used in programming languages to
direct the flow of a program. In this thesis we explore two such
left-sequential logics. First we discuss Fully Evaluated
Left-Sequential Logic, which employs a full evaluation strategy, i.e.,
to evaluate a term every one of its atomic propositions is evaluated
causing its possible side effects to occur. We then turn to
Short-Circuit (Left-Sequential) Logic as presented in [BP10b], where
the evaluation may be 'short-circuited', thus preventing some, if not
all, of the atomic propositions in a term being evaluated. We propose
evaluation trees as a natural semantics for both logics and provide
axiomatizations for the least identifying variant of each. From this,
we deﬁne a logic with connectives that prescribe a full evaluation
strategy as well as connectives that prescribe a short-circuit
evaluation strategy.