Page 14 - Textos de Matemática Vol. 40

2 Introduction
them here. We also do not want to argue that one is superior to the other, but we would like to stress that both have their own right to exist. By choosing here an untyped approach, we just give preference to the higher expressivity of untyped languages. “Expressivity” is meant in the way that we can, in general, write down more terms; or in other words: we do not have to bother with syntactical restrictions while writing down terms. However, we have to do more—but also, can do more—when we start proving properties of such terms.
Datatypes. Peano arithmetic is probably the best studied non-trivial for- mal system. It is powerful enough to prove most of the properties of a computer program in which one is interested. However, since Peano arithmetic deals with natural numbers only, every formalization requires that the computer program is coded by natural numbers. Although this is possible for all practical datatypes (like lists, trees, etc.), such a coding makes the treatment clumsy. For instance, proofs by induction on the original structure of a datatype have to be carried out in an unnatural way by use of complete induction for the natural numbers. Therefore, it is desirable to have a framework which allows the addition of new datatypes in a way that they can be used without extra coding machinery. This is one of the basic features of applicative theories.
Partiality. The phenomenon of partiality came into focus with the for- malization of the notion of computability. In fact, the question of termination of computations is one of the main issues in theoretical computer science. In principle, there are two formal approaches to this question (which often run in parallel to the distinction of typed and untyped languages): In the “restrictive” approach, one tries to set up a formal language in a way that every term rep- resents a terminating computation; then, the challenge is to find a representing term for a given computation. In the “unrestricted” approach, one may write down arbitrary terms, representing computations, but the question of termi- nation has to be proven afterwards, within the formal framework. To do so, one needs the possibility to express termination within the formal language. This is, to some extent, already possible in Peano arithmetic, considering prov- able total functions as those functions f for which the Peano arithmetic proves ∀x.∃y.f(x) = y. However, to speak about termination in a more abstract way— also independently of an implicit typing of the variables (natural numbers in the case of Peano arithmetic)—one can introduce a special definedness predicate on the logic level. In fact, it turned out that it is quite natural in this context to adapt the usual first-order predicate calculus such that variables range over defined objects only. This is done in the logic of partial terms which forms the basis of applicative theories. This logic allows us to speak within the language about termination, and it turned out that this feature distinguishes applica- tive theories for applications in computer science, in particular, for functional programming.
In this work, we will give as applications to programming languages a case study on least fixed points (Section 1.8) and a remark on the implementation of streams in functional programming languages (Section 3.3). We can also refer to