Up                                  

Analogical reasoning and analogical programming.

The motivation to study analogical reasoning and analogical programming is based on the fact that people think analogically, and program analogically. I studied the analogical reasoning in the derivational sense, i.e., not only the solution of the problem, but also the derivation of the solution, is analogically mapped.

I studied two aspects where analogical reasoning can aid software development. In the research of new paradigms for software development, one approach is to specify a system formally, and use formal methods to derive an implementation from specification. One goal of the research in this area is to seek the methods for (semi-) automatic transformation from specification to program. Another more modest goal is to provide some automated support to improve the system maintenance problem. This can be formulated as the problem of replaying: instead of modifying the implementation directly, the user can adapt the specification first, then derive its implementation by replaying the derivation.

Analogical reasoning can contribute to both of the above two problems. By means of the derivational analogical reasoning, I studied the problem of analogical program derivation in a formal way. My approach differs the others mainly in that the process is completely formalized. The analogical program derivation system is constructed using Visual C++.

The automatic acquisition of schematic rules within fold/unfold approach to program transformation.

Program transformation is to transform clear but inefficient programs to efficient ones. This is especially necessary in the area of functional programming. The program transformations rules can be classified into two categories: one is the catalog approach (e.g., in CIP). These rules are schematic. They can represent compact, large and useful transformation steps. But the applicability is limited to the initial catalog provided. Another approach is the generative approach (e.g., Fold/unfold system, Deductive program synthesis). The set of the rules is small but powerful. Though it is almost complete in that almost all the programs can be transformed, people find it difficult to combine the small steps to form meaningful transformations. So people are looking for heuristics such as fusion and tupling to guide the search of the appropriate transformation.

Some classes of program transformations (e.g., conversion to tail recursion) are more naturally expressed using schematic rules. The problem is that how should such schematic rules be provided? We hope that some fold/unfold transformations can be turned into schematic rules by means of higher order generalization. Also, we hope new tactics can be learnt from the concrete transformations.

The generation of proof schema and the reuse of proofs

It is probable that theorem provers can be improved by reusing previously computed proofs. Existing proofs can help in two ways: one way is that the concrete proof is directly adapted into another proof, another way is that two or more proofs are generalized into a schema which is to be instantiated later. I am interested in the study of generalizing existing proofs into a proof schema, and the heuristics in reusing the concrete proofs.

Generalization (anti-unification)

Generalization is a fundamental operation of inductive inference. Originated from the first order syntactic anti-unification, there are various extensions of generalizations. One direction of extending the anti-unification problem is to take into consideration of some kinds of background information. Another direction of extension is to promote the order of the underlying language.

There are two motivations to study the generalization problems: one is that the problem itself is interesting. There are various forms of unification such as E-unification, sorted unification, AC-unification, and higher order unification. For the first order ordinary unification, there is a pretty good corresponding notion of anti-unification. It is quite natural to ask what is the corresponding problem for other kinds of unification problems, and what is the solutions. Another motivation is that just as unification is a fundamental to deductive reasoning, generalization is fundamental to non-deductive reasoning.

I studied syntactic higher order generalization in a higher order language $\lambda 2$.The reason to use $\lambda 2$ is that it can be used to formalize various concepts in programming languages, such as type definition, abstract data types, and polymorphism. Based on the application ordering, we proved that the least general generalization exists and is unique up to renaming. An algorithm to compute the least general generalization is presented. Now the algorithm is under construction.

The higher order generalization procedure is used to find the analogical correspondence, and to generate program schemas and proof schemas. Recently I found that it also can be used in inductive programming.

Type theory

In the above study, I feel higher order logic is needed to do the meta-level inference. With the Curry-Howard homomorphism, we can regard propositions as types, and hence specifications as types. So type theory is a good vehicle to discuss the formal program development problems. On the other side, program development has its own characteristics. It is to be studied that how to $naturally represent the notions such as program transformation schemas, program development processes, programs and specifications. I studied type theories and formed a specific type theory that has an aim at the above targets. I tried to encode the algorithm design strategies such as divide-and-conquer in the type theory.

Programming by examples and program synthesis.

Program synthesis (e.g., the deductive approach, the transformational approach) is often criticized for two reasons: one is that for human beings the formal specification itself is not easy to obtain, the other is that for machines it is unlikely that we can completely automate the process of transforming the specification to the corresponding program.

On the other hand, program examples (e.g., input/output pairs) can help in both of the two aspects. Examples can clarify the concepts. Quite often, examples serve as a better mechanism to specify the problem than both declarative specifications and procedural programs. It is not easy for people to think in terms of mathematical logic, or in terms of recursions or variables. Besides, examples can also help in forming the concrete algorithms. The trace contains some information

The restriction of the programming by example approach is that, in general, a sequence of examples alone is not adequate to specify the whole software requirements.

It seems that both the program synthesis approach and programming by example approach are not adequate, and they may complement each other. I am interested in the study of the interaction and combination of the two approaches.

Generally speaking, it would be quite hard to automate the general purpose programming task. A more modest approach is to restrict the general purpose programming to end-user programming. By end-user programming we mean the various techniques to enable end users to create their own custom commands.

Specification acquisition.

Specification acquisition is always suffering from the problems of ambiguity, incompleteness, and inconsistency. I am interested in the study of mechanical support for the acquisition of specifications, and in particular, in the study of the reuse of existing specifications by analogical reasoning. Taking the advantage of giving lectures on VDM and Z at Fudan, I conducted some cognitive experiments to find the reasons and the ways analogy is used in specification writing. The target is to formulate a formal model and a tool to aid the writing of software specifications .