Noname manuscript No.
(will be inserted by the editor)

Sequential Operations in LogicWeb

arXiv:1412.1221v1 [] 3 Dec 2014

Daeseong Kang · Keehang Kwon ·
Zulkarnine Mahmud

the date of receipt and acceptance should be inserted later

Abstract Sequential tasks cannot be effectively handled in logic programming based on classical logic or linear logic. This limitation can be addressed
by using a fragment of Japaridze’s computability logic. We propose SeqWeb,
an extension to LogicWeb with sequential goal formulas. SeqWeb extends the
LogicWeb by allowing goals of the form G ∧s G and G ∨s G where G is a goal.
These goals allow us to specify both sequential-conjunctive and sequentialdisjunctive tasks.
Keywords Prolog · sequentiality · LogicWeb

1 Introduction
1.1 LogicWeb
Logic languages such as Prolog support nondeterminism (and automatic
backtracking) and thus is at a higher level of abstraction than imperative
programming languages. Unfortunately, logic programming has been popular
only in limited applications including AI, expert systems, and compilers. In
particular, logic programming languages has been little used for Web programming. Only recently has the work called LogicWeb [1] begun on the relationship between logic programming and the Web. LogicWeb views the Web as a
collection of logic programs.
LogicWeb thus allows us to build a web of information that machines can
understand and reason about. This includes the ability to answer complex
queries. The standard language that has been introduced so far is a subset of
first-order logic called Horn clauses with embedded implications.
Daeseong Kang · Keehang Kwon · Zulkarnine Mahmud
School of Electronics and Computer Eng., DongA Univ, 604-714 Busan, Korea
E-mail: khkwon@dau.ac.kr

2

Daeseong Kang et al.

Implementing LogicWeb, however, requires more than Horn clauses with
embedded implications. It must be able to deal with name scoping or local
constants to support information hiding. A language called first-order hereditary Harrop formulas (f ohh) [12,13,11] has been extensively studied. This
language offers modularity abstraction with local constants.
1.2 First-order herediatary Harrop formulas
The syntax of goals (or queries) permitted in Prolog is the following: they
can be atomic formulas or conjunctions or disjunctions of goals. In the context of Prolog, conjunctions are written using commas, while disjunctions use
semicolons.
The language of f ohh extends this set of logical symbols to include implications and universal quantifiers. In this language, formulas such as D ⊃ G and
∀xG will be permitted as goals, provided that D is a program and G is itself
a goal. The intended semantics of these two new operations is the following.
A goal such as D ⊃ G is to be solved by adding D to the current program.
Hence, D is to be available only during the course of solving G. As for a goal
such as ∀xG, it is intended to be solved by instantiating x in G by a new
constant c and then solving the resulting goal. Interpreted in this fashion, the
universal quantifier provides a means for limiting the availability of names.
We illustrate the problem mentioned above by considering the definition of
the fibonacci relation in Prolog. An efficient fibonacci program can be written
by using the idea of an accumulator. Implementing this idea in Prolog requires
an auxiliary predicate, called f ib aux below, to be defined. The following definition is a traditional way of realizing this:
module f ib.
f ib(N, F ) :- f ib aux(2, N, 1, 1, F ).
f ib aux(M, N, F 1, F 2, F 2) :- M >= N. % Nth fibonacci number reached
f ib aux(M, N, F 1, F 2, F ) :- M < N, f ib aux(M + 1, N, F 2, F 1 + F 2, F ).
The declarative interpretation of f ib aux here is that it is true if F 1 is the
(M −1)th, F 2 is the M th fibonacci number and F is the N th fibonacci number.
In this example, it is worth noting that f ib aux is a specialized predicate whose
only purpose for existence is its usefulness in defining f ib.
The addition of implication to goals provides a means for solving at least
part of this problem. Thus, the definition of f ib aux can be made “local” to
that of f ib, as indicated below:
f ib(N, F )) :(module f iba) ⊃ f ib aux(2, N, 1, 1, F ).
where
module f iba.
f ib aux(M, N, F 1, F 2, F 2) :- M >= N. % Nth fibonacci number reached
f ib aux(M, N, F 1, F 2, F ) :- M < N, f ib aux(M + 1, N, F 2, F 1 + F 2, F ).

Sequential Operations in LogicWeb

3

Given this definition of f ib, the following points might be observed. First, the
clauses defining f ib aux are not available at the top-level. Secondly, while the
definition of f ib aux is not available at the top-level, we see that it will become
available when solving the body of f ib.
However, there is one problem that still remains. The meaning of the predicate f ib aux inside the body of f ib is not insulated from definitions in existence
outside the body. This problem may be solved by using a universal quantifier.
f ib(N, F )) :∀f ib aux ((module f ib) ⊃ f ib aux(2, N, 1, 1, F )).
The indicated semantics of the universal quantifier dictates picking a new
name for f ib aux and then solving the instantiation of the given query with
this name.
The examples presented here have been of a very simple nature. They are,
however, sufficient for understanding the intended semantics of the new logical
symbols and also for appreciating some of their value from a programming
perspective. We note that the usefulness of the scoping mechanisms provided
by these symbols have been extensively studied and we point the interested
reader to, e.g. [12].

1.3 Contributions of this paper
Although the class of f ohh is quite attractive, sequential tasks cannot be
naturally handled in it. This limitation can be addressed by using a fragment of
Japaridze’s Computability Logic(CL) ([2] – [9]). CL is a new semantic platform
for reinterpreting logic as a theory of computable tasks. Formulas in CL stand
for instructions that can carry out some computational tasks. Queries stand
for actually executing these instructions.
This paper proposes Sequential LogicWeb (SeqWeb), an extension of LogicWeb [11] with sequentiality in goal formulas. Traditionally, LogicWeb has the
problem of expressing sequential tasks. The class of sequential goal formulas
enables the programmer to express these sequential tasks. They offer the possibility to combine imperative programming with declarative programming.
We need to define some terminology. A move (or a choice) is a string
over the keyboard alphabet. To be specific, executing ∃xG where G is a goal
requires a move by the machine. Similarly, executing ∀xC where C is a clause
also requires a move by the machine.
– A sequential-multiplicative-conjunctive(SMC) goal is of the form G1 ∧s G2
where G1 , G2 are goals. Executing this goal has the following intended
semantics: execute both G1 and G2 sequentially. In other words, all the
moves in G1 must precede all the moves in G2 . Both executions must
succeed for executing G1 ∧s G2 to succeed. It can be seen as a restricted
version of the parallel-conjunctive goal G1 ∧ G2 where all the moves in G1
must precede all the moves in G2

4

Daeseong Kang et al.

– A sequential-multiplicative-disjunctive(SMD) goal is of the form G1 ∨s G2
where G1 , G2 are goals. Executing this goal has the following intended
semantics: execute both G1 and G2 sequentially. At least one of these two
executions must succeed for executing G1 ∨s G2 to succeed. A SMD goal
can be used to express success with a degree. That is, new successes are
seeked, even after a success(solution) was found, as long as there probably
are more successes to come. Imagine Kim decides to buy a used BMW
from the local car dealers. Everytime he finds one at a local dealer(i.e., a
success), he will probably go to another dealer for a cheaper price(i.e., for
another success). Coming up with multiple successes does not affect the
successfulness of the effort, but the behaviors of the subsequent tasks such
as how much Kim has to pay for the car (Remember that we now have the
notion of sequential tasks, hence the notion of subsequent tasks.).
In this paper we present the syntax and semantics of this extended language, show some examples of its use and study the interactions among the
newly added constructs.
The remainder of this paper is structured as follows. We describe SeqWeb
based on a first-order sequential hereditary Harrop formulas in the next section. In Section 3, we present some examples of SeqWeb. Section 4 concludes
the paper.

2 The Language
The language we use is an expanded version of hereditary Harrop formulas. It
is described by G- and D-formulas given by the syntax rules below:
G ::= A | G ∧ G | G ∨ G | D ⊃ G | ∀x G | ∃x G | G ∧s G | G ∨s G
D ::= A | G ⊃ A | ∀x D | D ∧ D
In the rules above, A represents an atomic formula. A D-formula is called
a clause or an instruction.
In the transition system to be considered, G-formulas will function as
queries and a set of D-formulas will constitute a set of available instructions.
For this reason, we refer to a G-formula as a a query, to a set of D-formula
as an instruction set. Our language is an extension to first-order Hereditary
Harrop formulas with the main difference that new sequential constructs are
added in G-formulas.
We will present an operational semantics for this language. These rules in
fact depend on the top-level constructor in the expression and have the effect
of producing a new program and a new available instruction set.
The rules for executing queries in our language are based on “goal-directness”
in the sense that the next rule to be used depends on the top-level construct
of the goal formula. This property is known as uniform provability[13]. This

Sequential Operations in LogicWeb

5

property guarantees that the programmer knows exactly how execution will
proceed.
Definition 1. Let G be a goal and let P be a finite set of available instructions.
Then the notion of executing hP, G1 i – executing G relative to P – is defined
as follows:
(1)
(2)

(3)
(4)

(5)
(6)
(7)
(8)
(9)

If G is an atom and is identical to an instance of a program clause in P,
then the current execution terminates with a success.
If G is an atom and an instance of a program clause in P is of the form
G1 ⊃ G, execute hP, G1 i. This execution must succeed for the current
execution to succeed.
If G is G1 ∧ G2 , then execute both hP, G1 i and hP, G2 i in parallel. Both
executions must succeed for the current execution to succeed.
If G is G1 ∨ G2 , then execute both hP, G1 i and hP, G2 i in parallel. At
least one of these two executions must succeed for the current execution to
succeed.
If G is ∃xG1 , then execute hP, [t/x]G1 i where t is a term. This execution
must succeed for the current execution to succeed.
If G is ∀xG1 , then execute hP, [a/x]G1 i where a is a new constant. This
execution must succeed for the current execution to succeed.
If G is D ⊃ G1 , then execute h{D} ∪ P, G1 i. This execution must succeed
for the current execution to succeed.
If G is G1 ∧s G2 , then execute both hP, G1 i and hP, G2 i in sequence. Both
executions must succeed for the current execution to succeed.
If G is G1 ∨s G2 , then execute both hP, G1 i and hP, G2 i in sequence. At
least one of these executions must succeed for the current execution to
succeed.

The symbols ∧s and ∨s provide sequential executions of instructions: they
allow, respectively, for the sequential conjunctive execution of the instructions
and the sequential disjunctive execution of instructions.

3 SeqWeb
In our context, a SeqWeb page corresponds simply to a set of D-formulas or
a G-formula with a URL. The module construct mod allows a URL to be
associated to a set of D-formulas or a G-formula. An example of the use of
this construct is provided by the following “arithmetic” module which contains
some basic arithmetic-handling instructions written in conventional Prolog.
mod(www.dau.com/arith).
cube(X, Y ) : −Y = X ∗ X ∗ X.
f ib(0, 1). % first Fibonacci number
f ib(1, 1). % second Fibonacci number
f ib(X, Y ) : − X > 1 ∧ X1 is X − 1∧

6

Daeseong Kang et al.

X2 is X − 2 ∧ f ib(X1, Z)∧
f ib(X2, W ) ∧ Y is W + Z.
prime(X) : −. . . .
Our language in Section 2 permits sequential conjunction in goals. This
allows for sequential interactions between the user and the system. An example
of the use of this construct is provided by the page which does the following
sequential tasks: read a number from the user, output the number, and then
output its fibonacci number:
mod(www.dau.com/query1).
read(N ) ∧s
write(N ) ∧s
f ib(N, O) ∧s
write(′ f ib :′ ) ∧s
write(O)
These pages can be made available in specific contexts by explicitly mentioning
the URL via a hyperlink. For example, consider a goal www.dau.com/arith ⊃
www.dau.com/query1. Solving this goal has the effect of executing query1
with respect to the instructions in arith.
Imagine the number typed in is twin prime in the sense that both the
number and its successor by two are prime. In such cases we want to indicate
in addition that the number is twin prime. One way of displaying this extra
information is through the sequential disjunctive goals. The following is a
modification of the query1 page based on this idea.
mod(www.dau.com/query2).
read(N ) ∧s
write(N ) ∧s
(
(f ib(N, O) ∧s
write(′ its f ib :′ ) ∧s
write(O))
∨s
((prime(N ) ∧ prime(N + 2)) ∧s
write(′ twin prime′ ))
)
It is interesting to note that the above task requires the parallel-AND, the
sequential-AND, and the sequential-OR executions of instructions altogether.
Consider the task of measuring the blood pressure of a patient, i.e., bp(X, Y ),
where bp(X, Y ) means “patient X has blood pressure Y ”. Successfully solving
this task requires performing the measurement by a nurse dynamically and, in
addition, the outcome to be less than 180. The following is a program based
on this idea.

Sequential Operations in LogicWeb

7

mod(www.dau.com/nurse). % DongA hospital
bp(X, Y ) : − read(Y ) ∧ (Y < 180).
Now imagine a system that diagnoses the blood pressure of a patient by
having him taken the measurements twice in sequence. One way of expressing
this system is the following query.
mod(www.dau.com/query3).
read(X) ∧s % X is a patient
(((bp(X, Y 1) ∧s write(Y 1)) ∨s (bp(X, Y 2) ∧s write(Y 2)))
Consider a goal www.dau.com/nurse ⊃ www.dau.com/query3. Solving this
goal has the effect of executing query3 with respect to the instructions in
nurse. At the beginning, the system waits until the user specifies a patient
X. After X = Kim is selected, the system requests the nurse to measure
Kim’s blood pressure. If this is a success, the nurse reports the outcome to the
system. Once the outcome – say Y 1 = 150 – is received, the system requests
the nurse to measure Kim’s blood pressure once more. Again once the outcome
– say Y 2 = 130 – is received, the system reports Z = 130.

4 Conclusion
In this paper, we have considered an extension to LogicWeb with sequential
hereditary Harrop formulas. This extension allows goals of the form G ∧s G
and G∨s G where G is a goal. These goals are particularly useful for sequential
executions of instructions.
In [3], Japaridze introduced two sequential operators △ and ▽. These are
additive versions of our ∧s , ∨s : For goals A△B or A▽B to succeed, it is required
to succeed in only one of the tasks. These features in goal formulas are probably
desirable in terms of expressiveness. Our future interest is in a language which
extends sequential hereditary Harrop formulas with these features.
Acknowledgements This work was supported by Dong-A University Research Fund.

References
1. S.W. Lok and A. Davison, Logic Programming with the WWW, Proceedings of the 7th
ACM conference on Hypertext, ACM Press, 1996.
2. G. Japaridze, Introduction to computability logic, Annals of Pure and Applied Logic,
vol.123, pp.1–99, 2003.
3. G. Japaridze, Sequential operators in computability logic, Information and Computation,
vol.206, No.12, pp.1443-1475, 2008.
4. G. Japaridze. Computability logic: a formal theory of interaction. In Interactive Computation: The New Paradigm, Goldin D, Smolka S A, Wegner P (eds.), Springer, 2006, pp.
183-223.

8

Daeseong Kang et al.

5. G. Japaridze. Introduction to cirquent calculus and abstract resource semantics. Journal
of Logic and Computation, 2006, 16(4): 489-532.
6. G. Japaridze. The intuitionistic fragment of computability logic at the propositional level.
Annals of Pure Applied Logic, 2007, 147(3): 187-227.
7. G. Japaridze. Many concepts and two logics of algorithmic reduction. Studia Logica,
2009, 91(1): 1-24.
8. G. Japaridze. Towards applied theories based on computability logic. Journal of Symbolic
Logic, 2010, 75(2): 565-601.
9. G.
Japaridze.
On
the
system
CL12
of
computability
logic.
http://arxiv.org/abs/1203.0103, June 2013.
10. Kwon K, Hur S. Adding Sequential Conjunctions to Prolog. International Journal of
Computer Technology and Applications, 2010, 1(1): 1-3.
11. K. Kwon, Extending Logicweb via hereditary Harrop formulas, IEICE transactions on
Information and Systems, vol.E91-D, no.6, pp.1827–1829, 2008.
12. D. Miller, A logical analysis of modules in logic programming, Journal of Logic Programming, vol.6, pp.79–108, 1989.
13. D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov, Uniform proofs as a foundation
for logic programming, Annals of Pure and Applied Logic, vol.51, pp.125–157, 1991.

