arXiv:1508.03837v2 [] 24 Jan 2018

Incorporating User Interaction into
Imperative Languages
Keehang Kwon
khkwon@dau.ac.kr
Abstract: In this paper, we present two new forms of the write statement:
one of the form write(x); G where G is a statement and the other of the form
write(x); D where D is a module. The former is a generalization of traditional
write statement and is quite useful. The latter is useful for implementing
interactive modules.

1

Introduction

In this article, we describe a variant of C with some features that are inspired
by the work of [2]. These features include
(1) A write statement dual to the read statement which has the form
of write(x); G. This statement has the following new semantics: the
machine finds a value v for x so that the statement G can be successfully
completed.
(2) A interactive module of the form write(x); D where D is a set of procedure declarations. This write statement has the following interchanged
semantics: the user chooses a value v for x.
The notion of interactive methods/modules is quite indispensable in modern imperative languages. Interactive methods interact with the environment, therefore providing some form of interactive computing. This paper
aims to achieve interaction by providing interactive modules to imperative
languages. Thus we allow, within a module, declarations of the form write(x)
where x is a variable. The intended meaning is that the value of x is obtained
dynamically from the environment. To see the usefulness of interactive modules, let us consider the following method which produces the mobile phone
number of each employee.
write(y);
phone(x) =
1

case Tom : number = 8375;
case Jill : number = 2312;
case Kim : number = y;
In the above, the variable y - which is Kim’s Phone - will be obtained at
run time by requesting the environment to type in Kim’s phone number.
Implementing our language poses no serious problem. In this paper, we
introduce one way of implementing interaction. Our implementation scheme
is the following; when a module is loaded, the variables in the write statements will be replaced by the input values typed in by the environment.

2

The Language

The language is a subset of the core (untyped) C with some extensions. It is
described by G-, D- and E-formulas given by the syntax rules below:
G ::= true | A | x = exp | G; G | write(x); G
D ::= A = G | ∀x D | D ∧ D
E ::= D | write(x); E
In the above, A represents a head of an atomic procedure definition of the
form p(x1 , . . . , xn ). A D-formula is a set of procedure declarations. A Eformula is an interactive module.
In the transition system to be considered, a G-formula will function as
a statement and an E-formula enhanced with the machine state (a set of
variable-value bindings) will constitute a program. Thus, a program is a pair
hE, θi where θ represents the machine state. θ is initially empty and will be
updated dynamically during execution via the assignment statements.
We will present an interpreter for our language via a proof theory [1, 6].
Note that in the initialization phase (denoted by exec(P, G, P ′ )), our interpreter replaces all the variables in write in P with new input values from
the environment. After that, our interpreter proceeds like traditional C interpreter. To be specific, it alternates between the execution phase and the
backchaining phase. In the execution phase (denoted by ex(P, G, P ′ )), it
executes a statement G with respect to P and produce a new program P ′
by reducing G to simpler forms. The rules (6)-(9) deal with this phase.
If G becomes a procedure call, the machine switches to the backchaining
2

mode. This is encoded in the rule (5). In the backchaining mode (denoted
by bc(D, P, A, P ′ )), the interpreter tries to find a matching procedure for
a procedure call A inside the module D by decomposing D into a smaller
unit (via rule (4)-(5)) and reducing D to its instance (via rule (2)) and then
backchaining on the resulting definition (via rule (1)). To be specific, the rule
(2) basically deals with argument passing: it eliminates the universal quantifier x in ∀xD by picking a value t for x so that the resulting instantiation,
[t/x]D, matches the procedure call A. The notation S seqand R denotes the
sequential execution of two tasks. To be precise, it denotes the following:
execute S and execute R sequentially. It is considered a success if both executions succeed. Similarly, the notation S parand R denotes the parallel
execution of two tasks. To be precise, it denotes the following: execute S
and execute R in any order. It is considered a success if both executions
succeed. The notation S ← R denotes reverse implication, i.e., R → S.
Definition 1. Let G be a statement and let P be a program. Then the
notion of executing hP, Gi and producing a new program P ′ – exec(P, G, P ′ )
– is defined as follows:
(1) bc((A = G1 ), P, A, P1 ) ←
ex(P, G1 , P1 ). % A matching procedure for A is found.
(2) bc(∀xD, P, A, P1 , ) ←
bc([t/x]D, P, A, P1 ). % argument passing
(3) bc(D1 ∧ D2 , P, A, P1 ) ←
bc(D1 , P, A, P1 ). % look for a matching procedure in D1 .
(4) bc(D1 ∧ D2 , P, A, P1 ) ←
bc(D2 , P, A, P1 ). % look for a matching procedure in D2
(5) ex(hD, θi, A, P1 ) ← bc(D, P, A, P1 ). % A is a procedure call
(6) ex(P, true, P). % True is always a success.
(7) ex(P, x = exp, P ⊎ {hx, exp′ i}) ← eval(P, exp, exp′ ).
% In the assignment statement, it evaluates exp to get exp′ . The symbol
⊎ denotes a set union but hx, V i in P will be replaced by hx, E ′ i.
(8) ex(P, G1 ; G2 , P2 ) ←
ex(P, G1 , P1 ) seqand ex(P1 , G2 , P2 ). % a sequential composition
3

(9) ex(P, write(x); G1 , P1 ) ←
choose (and print) a value v for x so that ex(P1 , [v/x]G1 , P1 ). % write
statement
(10) exec(hwrite(x1 ) . . . write(xn )D, θi, G, P1) ←
read(y1) . . . . . . read(yn ) seqand ex(h[y1 , . . . , yn ]D, θi, G, P1). % In the
initialization phase, each xi is replaced with a new input value yi typed
by the environment.
If ex(P, G, P1 ) has no derivation, then the interpreter returns the failure.
The rule (9) deals with the new feature.

3

Examples

The following code displays the employee’s age to be determined at run time.
write(y1);
write(y2);
write(y3);
age(x) =
switch (x) {
case tom: age = y1; break;
case kim: age = y2; break;
case sue: age = y3; break;
default: age = 0;
}
Now consider the procedure call age(tom). The above code will be changed
to the one below in the initialization phase assuming the environment typed
in 30,40,22 for y1,y2,y3 respectively.
age(x) =
switch (x) {
case tom: age = 30; break;
case kim: age = 40; break;
case sue: age = 22; break;
default: age = 0;
4

}

Then execution proceeds in the usual way.

4

Conclusion

In this paper, we have presented a new form of the write statement of the
form write(x); S. This statement is a generalization of traditional write
statement write(exp), as we can write the latter as write(x); x == exp. Here
we assume that we allow boolean expressions as statements. In addition, we
have presented a notion of interactive modules. The notion of interactive
modules is an indispensable tool in modern interactive programming.

5

Acknowledgements

This work was supported by Dong-A University Research Fund.

References
[1] G. Kahn, “Natural Semantics”, In the 4th Annual Symposium on Theoretical Aspects of Computer Science, LNCS vol. 247, 1987.
[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] K. Kwon, S. Hur and M. Park, “Improving Robustness via Disjunctive
Statements in Imperative Programming”, IEICE Transations on Information and Systems, vol.E96-D,No.9, pp.2036-2038, September, 2013.
[5] J. Hodas and D. Miller, “Logic Programming in a Fragment of Intuitionistic Linear Logic”, Information and Computation, vol.110, No.2,
pp.327-365, 1994.

5

[6] 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.
[7] D. Miller, G. Nadathur, Programming with higher-order logic, Cambridge
University Press, 2012.

6

