Submitted for publication.
We present the natural confluence of higher-order hereditary Harrop
formulas (HH formulas) as developed concretely in Lambda Prolog,
Constraint Logic Programming (CLP), and Concurrent Constraint
Programming (CCP) as a fragment of (intuitionistic, higher-order)
logic. The combination is motivated by the need for a simple
executable, logical presentation for static and dynamic semantics of
modern programming languages. The power of HH formulas is needed
for higher-order abstract syntax, and the power of constraints is
needed to naturally abstract the underlying domain of computation.
Underpinning this combination is a sound and complete operational interpretation of a two-sided sequent presentation of (a large fragment of) intuitionistic logic in terms of behavioral testing of concurrent systems. Formulas on the left hand side of a sequent style presentation are viewed as a system of concurrent agents, and formulas on the right hand side as tests against this evolving system. The language permits recursive definitions of agents and tests, allows tests to augment the system being tested and allows agents to be contingent on the success of a test.
We present a condition on proofs, operational derivability (OD), and show that the operational semantics generates only operationally derivable proofs. We show that a sequent in this logic has a proof iff it has an operationally derivable proof.
G =>D (bottom of Page 7) has a typo. That paragraph
should be read as:
G => D. This interacts with Lambda by testing whether Lambda
passes G (using G => D as a resource if needed) and, if so, by
running D in parallel with Lambda. Thus we should require
Lambda, G => D ||- c iff for some Lambda': ((Lambda, G=>D),
c) -*-> ((Lambda', G=>D), c), and (i) Lambda' ||- c
or (ii) Lambda', G=>D ||- G and Lambda', D ||- c.
Notice that, in contrast to E, G functions as a deep guard in this
kind of agent formula. Further, the evolution of ((Lambda, G=>D),
c) may itself involve a recursive use of G=>D, but this time in
the context of establishing G' for a different G'=>D' in the
current configuration.
Correspondingly the formal rule for Deep Guard in Appendix C should be changed to:
Deep guard: Lambda, G => D ||- c iff for some Lambda': ((Lambda, G=>D),
c) -*-> ((Lambda', G=>D), c), and (i) Lambda' ||- c
or (ii) Lambda', G=>D ||- G and Lambda', D ||- c.