Wednesday, July 09, 2008


Additive free soap

There is a gap between scientific knowledge and our common sense which is learned by our everyday experiences. I will illustrate this gap by describing my recent experience with additive free soap. I have concluded that as long as there are people who feel “additive free” products are “good”, these products will flourish.

Recently, there have been many “additive free” products on the shelf of the grocery store, and these products are advertised as “safe” products. Now, I am skeptical of these “additive free” things for a scientific reason. One of the reasons (I am skeptical) is because I question the safety of “natural” or “traditional” products. Another reason I am skeptical is because of the definition of “additive free”.

First, “natural” or “traditional” products can be just as dangerous as “artificial” or “synthetic” products. The most toxic substance known to human beings is Botulin, which is created by the bacteria Clostridium botulinum. The strongest cancer causing substance known to human beings is Aflatoxin, which is naturally created by mold. Tobacco is traditionally used by Native Americans, yet it causes more cancer than any other chemical substance. Contrary to these naturally occurring substances, additives may actually improve safety. Additives are often added for safety reasons. For example, preservatives prevent bacterial decomposition of food. Such decomposition of foods creates cancer causing substances. Aflatoxin is an example of such substances. If you want to prevent decomposition by traditional methods, you need, for example, to add more salt to food. Unfortunately salt causes high blood pressure and stomach cancer.

Another issue concerning “additive free” products is the definition of “additive”. For example, let us consider additive free soap. How do we define additives to soap? In a sense, soap itself is an additive. During most of human history, people washed themselves by hot or cold water. Only in the industrial age was soap available for ordinary people to wash their body. So, we can say that soap is an additive to the natural cleaning process of the human body. Moreover, soap is created by a chemical reaction called Saponification, so it can be said that soap is a chemically synthetic product.

So, do I use additive free products? Funny thing is that actually I do. Recently, I switched facial and body soaps from soap with chemically synthetic ingredients to “additive free” soap. I have sensitive skin which tends to be dry. I often suffer skin irritation because of this. When I was using soap with chemically synthetic ingredients, I had an itchy feeling around my lips. Also, I had inflammation of the skin around my eyes. After switching to additive free soap, the itchy feeling around my lips disappeared. The inflammation around my eyes is still there, but it has gotten better. I do not know the reason for this change. Maybe it was just a change of weather which caused the improvement. But I like the feeling of additive free soap because it does not have an artificial odor.

More recently, I learned that there is a difference among additive -free soaps. I bought a soup made by “wakuneri”. Now, I do not know what “wakuneri” means, but I just know that it is a more “traditional” method of making soap. At first, I was skeptical. If the ingredients are the same, the method of making soap does not matter. But after I used this “wakuneri” soap, I found that it is creamier than ordinary soap. Now I use “wakuneri” soap for washing my body and face.

Conclusion? Experience outweighs scientific knowledge. Science cannot explain every detail of our daily life. As long as there is a problem which cannot be solved by science, we will continue to rely on our experience, and as long as there are people who feel that “additive free” products are “good”, these products will flourish.

P.S. Ms Maria Schneider pointed out that there is a long history of making soap by traditional methods before the industrial production of soap began. But I still concur that only after industrial age ordinary people can use soap in a bath room everyday.

Acknowledgement: Ms Maria Schneider check the English and did many suggestion to improve the article. I thank her greatly.

Saturday, June 21, 2008


The Future of Personal Computing

When I was introduced to a used Sun Workstation (a very dusty one) in my University, I was very excited. Although UNIX workstations have been around for a while, I was very much in awe of them for a long time. My view was a bit outdated perhaps, because other technology can now compete. Since then, I have had a long “quest” to obtain ultimate personal computing devices, and nowadays mostly use a cell phone and a paper-based diary for personal purposes. This article recounts my quest, the lessons learned and what insight can be gained from them for the future of personal computing.

My personal history on computers

My personal history on computers has a long prehistory. When I was an elementary school kid, I was given a PC magazine by my parents. I was amazed at what could be done by computers and I was very interested in programming. Unfortunately, my parents thought that PCs were too expensive to serve as a child's toy, so I could only play with an MSX computer, which my friends owned. My friends used the MSX computer for playing games, but it could be programmed using BASIC. Later I was given a pocket computer, which was a calculator with programming capability in BASIC. It was a nice toy, and I remember it with nostalgia. It was very small and light (it could be held in the palm of your hand) and since it was powered by batteries, you could carry it anywhere. Yet, you could do amazing things (like solving differential equations) using BASIC programming. Unfortunately, it had a very small amount of memory, it only showed 3 lines on the display, and it used audio tapes for external memory. Hence, it was useless for practical tasks like word processing. (Note that pocket computers were developed mainly for laboratories which needed complex calculations during experiments. For this purpose, I think they were very practical. Nowadays, they would be replaced by the ubiquitous PC.) Then, as with any adolescent there came a time when my pocket computer was forgotten on a dusty shelf.

Encountering a UNIX Workstation

My interests in computers were rekindled when I was introduced to a used Sun workstation in my University class. Although UNIX workstations have been around for a while, I was very much in awe of them for a long time. My view was a bit outdated perhaps, because other technology could now compete them already. When they were invented, they provided a unique environment for computing. Unlike “mainframes”, large central computers from this same time period, UNIX workstations were often individually owned. Yet unlike these day’s PC, they could communicate with each other. Therefore, they could be used for collaborative work. Unfortunately, UNIX workstations were expensive, so only rich organizations had them. So, individuals like me needed to attend a University class, or be employed by a high-tech company to use UNIX workstations.

In the university class, we were taught how to setup workstations, use email, share files, browse the World Wide Web, and launch the web server. They were exciting programs, but they took a lot of work. We had to replace the core part of the operating system, and input arcane variables to connect to the internet. There were no automatic update systems for software and no auto configuration of network parameters.

Linux Revolution

Then, there came a Linux PC. The revolutionary feature of Linux is that it provides the same functionality of a UNIX workstation, yet Linux can run on the ordinary PC. It means that now individuals can own the power of a UNIX workstation at home. Moreover, Linux is more advanced than traditional UNIX workstations. OK, I speak imprecisely. Linux means a kernel, the core part of the operating system. Linux as a kernel is a little more advanced than traditional UNIX. But more importantly, it comes with a lot of advanced tools and functionality. Most Linux “distribution” packages which include Linux kernel, are equipped with automatic update systems. It is for not only for the operating system itself, but also for the system software. We can choose a vast number of free and commercial software and install these programs. The operating system automatically keeps the software updated. Another good thing about Linux is that most software for Linux machines is free, and its source code is published. So, if you have programming skills, you can read the actual code and can learn a lot of things.

I played a long time with Linux on my favorite PC. I setup preferred software, created my favorite desktop configuration, surfed the internet, wrote articles, read and modified source code, played games, and most importantly, developed my own free software.

From Linux to Windows

Unfortunately, the magic of Linux did not last long. Linux is too complex. Linux is too complex partially because it is designed to be versatile. Linux can be used from a server, to an embedded controller in a computer-controlled machine. Linux also has an obsolete design philosophy. Linux follows the ‘UNIX philosophy’ , that is, a system is designed to be an ensemble of tools dedicated to simple tasks and communicating using plain (human readable) text. All configurations are done by writing a configuration file whose syntax differs from tool to tool. UNIX philosophy has the advantage that it allows users do complex tasks using a combination of simple components, and since all data is human readable, it allows users maximum control over what a system does. On the other hand, using multiple tools even for a common task is cumbersome and error-prone. Unless tools are very carefully designed, they often do not work together very well.

Switching to Windows has other advantages. First, Linux often does not support the newest PC hardware. The easiest way to run Linux on a PC is to run it as a Virtual machine (like VMWare) on Windows. So, you have to install Windows on your PC anyway. There are other reasons to install Windows. Most PC vendors do not support Linux officially, so you need Windows to troubleshoot your PC. Sometimes, you may need to run software which does not have a Linux version, such as Microsoft Office. Doing all jobs on the Windows platform simplifies the configuration of your PC and reduces the amount of disk space necessary to run everything.

Because a lot of data occupied the hard-drive of my PC, I removed Linux from my PC and am doing all tasks on Windows instead.

From PC to Cell phone

Windows, however, is not the ultimate answer for all my computing needs. Windows is still too complex. It requires configuration to connect to the internet. You need to manage any software packages that you installed. The software is often buggy and slow.

While fighting with Windows, I was more and more inclined to use my cell phone for communication, instead of PC mail. The biggest difference between a PC and a cell phone is that a cell phone is more casual. PC mail is used more often by technology oriented people in a professional capacity. Cell phones are used by everyone all every time. Usually, a cell phone works flawlessly and you do not need to configure it to use its basic functions. Recently, functionality of cell phones has expanded greatly, and nowadays you can see Web pages, Word documents, and Excel sheets on a cell phone.

As for personal information management, I go back to traditional paper. I now carry a large binder which contains my diary, TODO list, address list, a list of restaurants, and so on. Paper is the most reliable (it never crashes), flexible (you can stick post-it notes to pages, for example), and is an information-rich medium (your handwriting is preserved as is).

Lesson Learned

I argue that the real personal computing tool ought to be:

· really personal; that is, everyone can own their own computing tools and carry them everywhere

· able to communicate

· specialized for personal use

· centrally managed

In the end, it looks like a cell phone!

the real personal computing tool ought to be like a part of someone's body, owned personally, and carried everywhere. The term personal computer is a contradiction because they are often not very personal. They are owned by a company or family, and not truly owned by an individual. Another problem with a PC is its size and weight, which prevent people from carrying it everywhere.

The second important criterion is communication. It is an indispensable part of current computing. The constant ability to communicate is the modern "must" of life. By its universal computing power, computers can mimic any information medium. Combining handiness and portability, computing tools can give individuals the maximal communication ability.

The third criteri
on is to create a computer that is "specialized for personal use." This idea may need more explanation. Computers have an infinite computing capability. Any computation which can be performed manually can be performed by computers. This capability is the strength of computers. The versatility enables computers to be used everywhere, from kitchen equipment to space exploration. On the other hand, this can be a weakness, since it means that computers can be used maliciously, can perform in an unexpected fashion, and their functionality increases the complexity of the machines in general. The results are software bugs, malware, security problems, and viruses. Therefore, something has to be done to control universal computing power. Moreover, since computers are versatile, computers need configuration before they are used for specific purposes. Configuration costs a large sum during the lifetime of the computer.

By specifically designing a computer for personal use, the ability of computers can be restricted to those specific functions that are needed for personal use. This restriction makes security less problematic. For example, cell phones, a device specifically designed for personal use, allow very few computer viruses. Further, this restriction makes configuration easier. For example, cell phones are used by most people now, while using a PC usually requires more professional skill.

The fourth criterion, “centrally managed,” is in contrast to PCs, which are not centrally managed. Decentralization causes problems in three areas: compatibility, management and security. First, decentralized computers have compatibility problems. They have different software, different version of the same software, and different settings. These differences cause problems when data is transferred from one computer to another, or computers try to connect to each other. Second, decentralized computers have management problems. The same updates and the same settings must be updated onto each computer independently. This means that a large amount of effort is wasted to do the same thing repeatedly. Each computer must be managed and updated individually. If a mistake is made, it will be made repeatedly Third, decentralized computers have security problems. If computers are managed individually, software in some computers would not be updated properly. This causes a security risk.

Centrally managed computers such as cell phones solve these three issues. First, centrally managed computers are compatible with each other, since the software and setup are identical. Second, centrally managed computers eliminate tedious management tasks which should have been done on each computer. Third, centrally managed computers are more secure, since they always have the newest security updates.


How far will we go with the ideal of personal computing? As I have shown, the cell phone is a good candidate for an ideal personal computing medium. Unfortunately, as cell phones become more powerful, they become more and more PC-like; that is, slow, unreliable, and complex. So, in the foreseeable future, perhaps we cannot dispense with paper-based personal information management tools when we need reliability, simplicity and freeness of use.


Ms Maria Schneider read the text before publishing and suggested many improvements. I thank her greatly.

Saturday, May 31, 2008


APAL paper: A sequent calculus for limit computable mathematics

Stefano Berardi and I co-authored a paper appeared Annals of Pure and Applied Logic.
A sequent calculus for limit computable mathematics
You need register ScienceDirect to read the article. If you are interested the article but do not have the access right, please write to me ( Then, I send a personal copy. The article is a part of the special issue dedicated "Classical Logic and Computation 06" held in Venice in 2006. The article is rewritten from scratch after the conference; although no new mathematical result is added, presentations are totally different from the conference version. Also, there is a technical report that extends the conference version by adding examples. The conference version and the technical report are freely available.
The purpose of the article is to give a sequent calculus which is sound and complete formulation of limit computable mathematical (LCM for short). Surprisingly, if we remove Exchange rule (changing order of formulas in sequents) from infinitary sequent calculus for classical logic, we obtain sequent calculus for LCM. This is the first formal (albeit infinitary) system for LCM, since previously LCM was defined by semantics (realizability or games).

But, what is LCM? Now, let me explain the motivation behind LCM first. There are thoughts called "intuitionism", or "constructivism". For "ordinal" mathematics, proofs are exercise to establish the truthness of the conclusion. In a sense, the focus is on statements established by proofs, not proofs themselves. "Intuitionism” or "constructivism” argues that proofs themselves have meaning as a "guidance" to establish "intuition" of statements. Using modern computer science word, proofs are programs which output "direct evidence" of statements.

Mathematics based on intuitionism has rich structures, and applied to automatic program derivation from proofs. Yet, it has a draw back that it invalidates an important logical principle called Excluded Middle. Excluded Middle states that for any statements “A”, “A” holds or “not A” holds. Intuitionism rejects Excluded Middle because there is no general way to construct intuition of either “A” or “not A”, since if it is possible, there is a decision procedure of truthness of statements of the given languages, which is generally not the case.

However, this draw back is serious draw back since Excluded Middle is heavily used in “ordinal” Mathematics.

Here comes LCM comes to rescue. LCM allows limited form of Excluded Middle, that is, existential statements for decidable properties. Yet, its proofs have a meaning as a “learning process” of evidence of statements. Unlike intuitionism, proofs of LCM do not construct evidence of statements directly. Instead, they output infinite stream of “guess” of the correct evidence, and reach the correct answer after finite (but unpredictable numbers of) steps. Difference here is that in LCM, there is no general way to know whether proofs construct the correct evidence already or not. Only we can know sure that proofs reach the correct evidence after infinite step, hence they are called “limit” computable.

Unfortunately, before our article, there is no simple syntactic description of correct inferences in LCM. Correct inferences of LCM were defined as proofs which allow interpretation as learning processes. Later, characterization using game semantics is found, which is greatly related to our article. In fact, our article proves not just soundness and completeness, but formal proofs of our system are isomorphic to winning strategies of game interpretation of its conclusion. There is some subtlety here. What “isomorphic” means? This is the reason that we had to rewrite the article. I do not content the final formulation appeard in the APAL paper either. I would love suggestions from the readers.

Saturday, September 30, 2006



BrainScan is a source-code model checker for BrainF*ck. Source tar ball and statically-linked x86 linux binary. BrainScan is written by OCaml, so to compile you need OCaml (> =3.09) , findlib and extlib.

BrainScan can check
-H or --hash options allow to compress the state space using hash values. This makes the check imprecise, but save large amount of memory. should be integer from 1 to 31.


Sunday, August 20, 2006


Camomile 0.7.1

Camomile 0.7.1 is relased, to solve Camomile 0.7.0 installation problem.



Here is a patch to fix the problem mentioned in the previous post

RCS file: /cvsroot/camomile/camomile/,v
retrieving revision 1.78
diff -c -r1.78
*** 19 Aug 2006 07:58:29 -0000 1.78
--- 19 Aug 2006 17:42:28 -0000
*** 94,100 ****
public/caseMap.cmo public/uRe.cmointernal/uReStrParserType.cmointernal/uReStrParser.cmo internal/uReStrLexer.cmo public/uReStr.cmo! public/main.cmo


--- 94,100 ----
public/caseMap.cmo public/uRe.cmointernal/uReStrParserType.cmointernal/uReStrParser.cmo internal/uReStrLexer.cmo public/uReStr.cmo! public/main.cmo public/default.cmo


*** 195,201 ****
TOOLSLIB=bigarray.cma str.cma toolslib.cma

! tools : $(TOOLS) tools/parse_allkeys.byte tools/camomilelocaledef.byte

$(TOOLS) : %.byte : toolslib.cma %.cmo
$(OCAMLC) $(BFLAGS) -o $@ $(TOOLSLIB) $*.cmo
--- 195,201 ----
TOOLSLIB=bigarray.cma str.cma toolslib.cma

! tools : $(TOOLS)

$(TOOLS) : %.byte : toolslib.cma %.cmo
$(OCAMLC) $(BFLAGS) -o $@ $(TOOLSLIB) $*.cmo
*** 354,360 ****
public/uCharInfo.mli public/uNF.mli public/uCol.mli public/caseMap.mli public/uRe.mli public/uReStr.mli public/charEncoding.mli public/uTF8.mli public/uTF16.mli public/uCS4.mli ! public/uPervasives.mli public/main.mli

install: $(INSTALL) install-data install-bin

--- 354,360 ----
public/uCharInfo.mli public/uNF.mli public/uCol.mli public/caseMap.mli public/uRe.mli public/uReStr.mli public/charEncoding.mli public/uTF8.mli public/uTF16.mli public/uCS4.mli ! public/uPervasives.mli public/main.mli public/default.mli

install: $(INSTALL) install-data install-bin

Index: public/
RCS file: public/
diff -N public/
*** /dev/null 1 Jan 1970 00:00:00 -0000
--- public/ 19 Aug 2006 17:39:40 -0000 1.1
*** 0 ****
--- 1 ----
+ module Camomile = Main.Make(CamomileDefaultConfig)
Index: public/default.mli
RCS file: public/default.mli
diff -N public/default.mli
*** /dev/null 1 Jan 1970 00:00:00 -0000
--- public/default.mli 19 Aug 2006 17:39:40 -0000 1.1
*** 0 ****
--- 1,19 ----
+ (** modules with default configuration. Almost compatible to Camomile 0.6.x *)
+ module Camomile : Main.Type with
+ module ISet = ISet and
+ module IMap = IMap and
+ module XArray = XArray and
+ module OOChannel = OOChannel and
+ module UChar = UChar and
+ module USet = USet and
+ module UMap = UMap and
+ module UCharTbl = UCharTbl and
+ module UnicodeString = UnicodeString and
+ module UText = UText and
+ module XString = XString and
+ module SubText = SubText and
+ module ULine = ULine and
+ module UTF8 = UTF8 and
+ module UTF16 = UTF16 and
+ module UCS4 = UCS4
Index: public/main.mlip
RCS file: /cvsroot/camomile/camomile/public/main.mlip,v
retrieving revision 1.2
diff -c -r1.2 main.mlip
*** public/main.mlip 13 Aug 2006 20:29:25 -0000 1.2
--- public/main.mlip 19 Aug 2006 17:42:28 -0000
*** 135,155 ****
module UTF8 = UTF8 and
module UTF16 = UTF16 and
module UCS4 = UCS4
- module Camomile : Type with
- module ISet = ISet and
- module IMap = IMap and
- module XArray = XArray and
- module OOChannel = OOChannel and
- module UChar = UChar and
- module USet = USet and
- module UMap = UMap and
- module UCharTbl = UCharTbl and
- module UnicodeString = UnicodeString and
- module UText = UText and
- module XString = XString and
- module SubText = SubText and
- module ULine = ULine and
- module UTF8 = UTF8 and
- module UTF16 = UTF16 and
- module UCS4 = UCS4
--- 135,137 ----
Index: public/main.mlp
RCS file: /cvsroot/camomile/camomile/public/main.mlp,v
retrieving revision 1.3
diff -c -r1.3 main.mlp
*** public/main.mlp 13 Aug 2006 20:29:25 -0000 1.3
--- public/main.mlp 19 Aug 2006 17:42:28 -0000
*** 185,189 ****

module UReStr = UReStr.Configure(Config)
- module Camomile = Make(CamomileDefaultConfig)
--- 185,187 ----
Index: tools/
RCS file: /cvsroot/camomile/camomile/tools/,v
retrieving revision 1.16
diff -c -r1.16
*** tools/ 19 Dec 2003 17:24:34 -0000 1.16
--- tools/ 19 Aug 2006 17:42:28 -0000
*** 1,6 ****
--- 1,7 ----
(* $Id:,v 1.16 2003/12/19 17:24:34 yori Exp $ *)
(* Copyright 2002 Yamagata Yoriyuki *)

+ open Toolslib
open Unidata
open AbsCe

Saturday, August 19, 2006


Camomile 0.7.0 installation problem

Clean install of Camomile 0.7.0 fails, because it tries to read a data file from a directory which is not populated yet. This is due to wrong design of module dependancy. The bug fix would be shipped shortly.

Monday, August 14, 2006


Camomile 0.7.0

I'm pleased to announce Camomile-0.7.0, new version of a comprehensive Unicode Library for OCaml.

This release is a major change of module structures. Now the whole library becomes a functor over "configuration" module, which specifies the location of data files necessary to run Camomile. This enables to distribute binary with compiled Camomile library, which may run on machines with different directory structures. If you just want to use default configuration, use CamomileLibrary.Main.Camomile module in the place of Camomile module of previous versions.

This page is powered by Blogger. Isn't yours?