======================================================================
Computing-As-Editing Paradigm --- Boomborg Softwares
Masami HAGIYA and Tomoki SHIRATORI
Department of Information Schence
Graduate School of Science, University of Tokyo
======================================================================
CAEP (Computing-As-Editing Paradigm) is a programming paradigm in
which we intend to unify the process of editing a program and that of
doing computation by executing a program. The fundamental philosophy
of CAEP is summarized as follows.
* The purpose of using a computer is to produce the final text
such as report, paper, book, etc., and not to write a program.
* Pieces of information in the final text are related with one another
by various kinds of constraint.
* The process of editing text includes that of setting and solving such
constraints.
* Constraint solving is considered as computing.
We use the word "text" in a rather wide meaning. For example, a
so-called "computational trace" that describes a process of obtaining
an output from a given concrete input is also considered as "text".
According to the above philosophy, we are developing a series of
softwares called "Boomborg" (for stationary in Japanese), which
consists of programs running on GNU Emacs, the widely used
genereral-purpose text editor on PCs and workstations. In order to
support the process in which editing and computing are unified,
Boomborg softwares have the following features.
* All the constraints on text are visible. This means that all
the information available to a user is on the editor buffer and
visible to the user. --- visibility
* Text is edited by a general-purpose text editor and no structure
is induced on text while editing. Structures are interpreted
as the time of constraint solving. --- structure-freedom
These two features in particular allow smoothe editing with trials and
errors, which is important for the process of unifying editing and
computing. In the softwares, one can freely insert symbols denoting
constraints into text and invoke constraint solvers to solve those
constraints at any time of editing by executing appropriate commands.
One can solve all the constaints in text at once or can also
incrementally solve them while editing the text.
The following two softwares are typical in the series.
* Boomborg-PC
* Boomborg-KEISAN
Boomborg-PC is a proof-checker running on GNU Emacs (more precisely,
Nemacs or Mule). It has a built-in type-checker of a typed
lambda-calculus. Unlike other existing proof-checkers, one can also
typecheck incomplete proofs, and after modification of any part of
proof text, one can immediately check the modified part.
Boomborg-KEISAN is a software running on GNU Emacs that might be
called "free-format spread sheet". A user of this software inserts
into text symbols denoting constraints such as computing a sum,
evaluating an expression, etc. Parts of text are thus related with
one another. Constraint solving is naturally included in the process
of editing text.
========================================================
Computing-as-Editing Paradigm and Programming-by-Example
========================================================
We briefly introduce the software Boomborg-KEISAN, and then explain
the relationship between CAEP (Computing-As-Editing Paradigm) and PBE
(Programming-By-Example). We finally list some research directions in
the future.
１. What is Boomborg-KEISAN?
============================
● Overview of Boomborg-KEISAN
Boomborg-KEISAN is a software developed on GNU Emacs that might be
called "free-format spread sheet". Boomborg-KEISAN is based on the
CAEP philosophy described above. KEISAN is for computation in
Japanese.
Boomborg-KEISAN supports an Emacs mode called "keisan-mode" in which a
user can do text-editing without any restrction. While editing text,
one can insert symbols meaning computing a sum, evaluating an
expression, puting labels, specifing repetition, etc.
Those symbols denote constraints that relate various parts of text
with one another. The process of setting and solving constraints is
naturally included in the process of editing.
In the following, we explain commands, constraint symbols and the
constrait solver of Boomborg-KEISAN.
(This text is also written on Mule with Boomborg-KEISAN.)
● Commands
M-x do-keisan (C-c C-c)
Searches for a constraint symbol after the cursor position,
and solves the constraint corresponding to the first symbol found.
C-u M-x do-keisan (C-u C-c C-c)
Solves all the constraints in the text buffer.
C-u C-u M-x do-keisan (C-u C-u C-c C-c)
Executes do-keisan in the stepwide mode.
M-x keisan-region (C-c C-r)
Executes do-keisan in the current region.
M-x compute-expression (C-c C-e)
Evaluates an expression and writes the output.
M-x sum-horizontally (C-c C-h)
Computes the sum of the numbers to the right.
M-x sum-vertically (C-c C-v)
Computes the sum of the numbers downwards.
● Constraint Symbols
:: Evaluate the expression to the right.
↓+ Sum vertically.
+→ Sum horizontally.
↓L Copy the contents of label L downwards.
L→ Copy the contents of label L to the right.
↑L Put label L to the number above.
←L Put label L to the number to the left.
｛P｝ Check expression P.
∫C Give constraint C to the numbers above and down.
♂ Iterate the lines up to ♀.
■ Specify conditional constraints.
● Constraint Solver
* The Algorithm for Solving Constraints
repeat
save the buffer;
repeat in each line from the beginning of the buffer
repeat for each constraint symbol from the beginning of the line
solve the constraint denoted by the symbol
until the end of the line
until the end of the buffer
until the buffer has not been modified
At this moment, we do not use sophisticated techniques for constraint
satisfaction such as constraint hierarchy. For small examples, the
above algorithm seems sufficient. We leave incorporating those
techniques as a research topic in the future.
● Example --- tax computation by a university teacher
-*- keisan -*-
↓+収入金額 ↓+源泉徴収税額
給与,賞与 小田原大学 6624018 600000
賞与 箱根短大 21505 1505
------------------------------------------------
給与所得計算:: 6645523 *9/10-1095000 = 4885970 601505
↑(7)給与 ↑源泉給与分
↓+収入金額 ↓+ ↓+源泉徴収税額
印税(初版) 大波書店:: 200000 *7/10 = 140000 20000
印税(重版) 小波書店:: 100000 *8/10 = 80000 10000
原稿料 集凡社:: 11111 *7/10 = 7777 1111
原稿料 集凡社:: 22222 *7/10 = 15555 2222
講演料 日本冗談学会:: 33333 *7/10 = 23333 3333
-----------------------
266665 36666
↑(8)雑 ↑(35)の一部
---------
必要経費計算:: 366666 - ↑ = 100001
↓+所得計算 ↓+控除計算
(7)給与→ 4885970
(8)雑→ 266665
(12)医療費控除 100000
(13)社会保険料控除 566130
(15)生命保険料控除 50000
(24)扶養控除 350000
(25)基礎控除 350000
----------------------------------------
課税所得計算:: 5152635 - 1416130 = 3736505
(10)合計 (26)合計 ↑所得
:: 所得 / 1000 * 1000 = 3736000 ←(27)課税所得
↑所得
■ 1000 <= 所得 & 2999000 >= 所得 ⇒ 10 ←税率 0 ←控除額
□ 3000000 <= 所得 & 5999000 >= 所得 ⇒ 20 ←税率 300000 ←控除額
□ 6000000 <= 所得 & 9999000 >= 所得 ⇒ 30 ←税率 900000 ←控除額
□ 10000000 <= 所得 & 19999000 >= 所得 ⇒ 40 ←税率 1900000 ←控除額
□ 20000000 >= 所得 ⇒ 50 ←税率 3900000 ←控除額
↓+源泉計算
源泉給与分→ 601505
(35)の一部→ 36666
--------
638171
↑(35)源泉徴収税額
↓所得 ↓税率 ↓控除額 ↓+納税額
税額計算:: 3736000 *20/100 - 300000 = 447200 (28)税額
↓(35)源泉徴収税額
源泉*(-1):: 638171 *(-1) = -638171
---------
-190971 (36)申告納税額
２. Relationship between CAEP and PBE
=====================================
CAEP is naturally related to PBE.
● Two Approaches to PBE (Programming-By-Example)
Interactive PBE vs. Automatic PBE → Theretically interesting,
but not practical.
↓
Expects human interaction.
Constructs a system that helps humans do generalization.
User-interface is important.
The so-called demonstrational programming in the field of
user-interface is a typical example of interactive PBE. In
demonstrational programming, a sequence of operations that a user has
invoked is taken as a computational trace and generalized to a
program. This means that computatinal traces are represented
temporally.
In this research, we are interested in constructing a demonstrational
programming system in which computational traces are represented not
temporally but spacially. In such a system, it is important that one
can naturally and easily write computational traces.
● CAEP
Computing-As-Editing Paradigm (= programming-as-editing paradigm)
--- construction of computational traces with an editor
Merits of Using an Editor
--- By allowing constraint solving during editing,
one needs not write every part of a trace by hand.
The constraint solver augments the trace.
--- It may be possible to use a user's editing operations
for inferring constraints in a trace.
* PBE in CAEP
computational trace
｜
｜ Programming-by-Example problem --- the problem of inferring
｜ constraints from the process
↓ of editing
computational trace --- Constraints are ｖｉｓｉｂｌｅ！
with (iteration) constraint ================
||
program --- Modifing a part of a trace corresponds to
giving an input to a program.
(Re)solving constraints corresponds to
executing a program.
Example: Program to compute the sum of squares of 1〜n
(1) Write expressions for some n
(construct a computational trace for some n)
(case where n=3)
↓+
:: 1 * 1 = 1
:: 2 * 2 = 4
:: 3 * 3 = 9
----------------------------
14
(2) Insert an iteration constraint (see the next page for iteration).
In this example, the pattern ":: n * n = "
is repeated until above "----" while n is increased by 1.
↓+
♂ :: 1 * 1 = 1
♀ :: 2 * 2 = 4
:: 3 * 3 = 9
----------------------------
14
If we regard the position of "------" as an input, this text can be
considered as a program to compute the sum of squares.
^^^^^^^
To compute the sum of squares of 1〜10,
↓+
♂ :: 1 * 1 = 1
♀ :: 2 * 2 = 4
:: 3 * 3 = 9
(insert seven empty lines)
----------------------------
14
│
│ (after constraint solving)
↓
↓+
♂ :: 1 * 1 = 1
♀ :: 2 * 2 = 4
:: 3 * 3 = 9
:: 4 * 4 = 16
:: 5 * 5 = 25
:: 6 * 6 = 36
:: 7 * 7 = 49
:: 8 * 8 = 64
:: 9 * 9 = 81
:: 10 * 10 = 100
----------------------------
385
--------------------------------------------------------------------
Appendix: Details of Iteration
- The part of text from the line ♂ up to the line ♀ is considered
as a pattern of iteration.
Example:
♂ A A
For text of the form B , the iterated pattern is B .
C C
♀ D
- The iterated pattern may have parts that are increased (or decreased)
in each iteration step. The differences between the line ♂ and the
line ♀ are used as increments.
Example:
♂ 1
For text of the form 10 , the increment is (2-1=)1.
100
♀ 2
2
Following ♀ are lines 11 .
101
- Lines are iterated until "----" appears.
Example:
♂ 1
♀ 2
-----------
│
│ (after constraint solving)
↓
♂ 1
♀ 2
3
4
5
-----------
--------------------------------------------------------------------
● Generalization to Regular Traces
Regular trace expressions are computational traces that have
structures representing iteration and conditional branching whose
basic units are lines.
Inserting symbols denoting constraints into computational trace, one
implicitly defines regular trace expressions behind computational
traces.
* Iteration
♂ 1
1
♀ 2
2
3
3
4
4
------
* Nesting of Iteration
♂♂ 1
♀ 2
3
4
♀♂ 2
♀ 3
4
5
♂ 3
♀ 4
5
6
--------
The above example can be regarded as iteration of simple computational
traces though the outer iteration has increments.
The following example, however, can only be interpreted as iteration
of regular trace expressions.
♂♂ 2
♀ 1
†｛ ↑ == 1 ｝
♀♂ 3
♀ 2
1
†｛ ↑ == 1 ｝
♂ 4
♀ 3
2
1
†｛ ↑ == 1 ｝
------------------
†｛ ↑ == 1 ｝ expresses the terminating condition of iteration.
Inside ｛｝ is a conditional expression.
↑ denotes the number above itself.
The inner iteration continues until the line with 1 appears.
* Condition
6 ←x
■ x%2==0 ⇒ :: x/2 = 3 ←x
Constraints to the right of ■P⇒ are active only when the expression
P is true.
⇒ at the beginning of a line means continuation.
■ x%2==0 ⇒ :: x/2 = 3 ←x
⇒ :: z*z = 9 ←z
* Conditional Branching
By using lines with complementary conditions, we can represent
conditoinal branching.
6 ←x
■ x%2==0 ⇒ :: x/2 = 3 ←x
□ x%2!=0 ⇒ :: x-1 = 5 ←x
Lines with complementary conditions are taken into account when
interation constraints are solved.
6 ←x
♂ ■ x%2==0 ⇒ :: x/2 = 3 ←x
♀ ■ x%2!=0 ⇒ :: x-1 = 2 ←x
■ x%2==0 ⇒ :: x/2 = 1 ←x
The above iteration is considered as equivalent to the following one.
6 ←x
♂ ■ x%2==0 ⇒ :: x/2 = 3 ←x
□ x%2!=0 ⇒ :: x-1 = 5 ←x
♀ ■ x%2==0 ⇒ :: x/2 = 1 ←x
□ x%2!=0 ⇒ :: x-1 = 2 ←x
■ x%2==0 ⇒ :: x/2 = 1 ←x
□ x%2!=0 ⇒ :: x-1 = 1 ←x
By using conditional branching in iteration, one can express programs
such as the following, which computes z=y^x.
6 ←x
2 ←y
1 ←z
♂ ■ x%2==0 ⇒ :: x/2 = 3 ←x
⇒ :: y*y = 4 ←y
♀ ■ x%2!=0 ⇒ :: x-1 = 2 ←x
⇒ :: y*z = 4 ←z
■ x%2==0 ⇒ :: x/2 = 1 ←x
⇒ :: y*y = 16 ←y
■ x%2!=0 ⇒ :: x-1 = 0 ←x
⇒ :: y*z = 64 ←z
† ｛ x == 0 ｝
:: z = 64
３. Future Research Directions
==============================
● Constraint Solving
There is much room to do research in heuristics and user-interface for
solving iteration constraints, in particular, with conditional
branching.
● Constraint Inference
It may be possible to infer constraints from editing operations.
--- For example, it may be possible to infer iteration constraints
from the operations of coping one line downwards and modify the new one.
--- One may insert ↓+ after the command C-c C-v (M-x sum-vertically).
● Variation of Iteration
- Blockwise Increments
♂ 1 ♂ 1
10 10
100 100
♀ 2 ♀ 2
20 ⇒ 20
200 200
3
30
300
------------- -------------
- Iteration with Constraints
:: 1 * 1 = 1 :: 1 * 1 = 1
♂ ∫+3 ♂ ∫+3
:: 2 * 2 = 4 :: 2 * 2 = 4
♀ ∫+5 ♀ ∫+5
:: 3 * 3 = 9 ⇒ :: 3 * 3 = 9
∫+7
:: 4 * 4 = 16
∫+9
:: 5 * 5 = 25
----------------------- -----------------------
(Already implemented.)
- Horizontal Iteration
♂ ♀ | ♂ ♀ |
♂ 1 2 | ♂ 1 2 3 4 5 |
♀ 2 | ♀ 2 3 4 5 6 |
| ⇒ 3 4 5 6 7 |
| 4 5 6 7 8 |
| 5 6 7 8 9 |
----------------------------- -----------------------------
(Can Pascal's triangle be expressed?)