https://www.cs.ox.ac.uk/files/3287/PRG05.pdf

Опубликовано через год после смерти (в 1975) соавтора предыдущей работы

«The "paradox" of self-application ( as in x(x) ) is solved by allowing the same x to be used in two
differeht ways. This is done in ordinary recursion theory via Godel numbers ( as in {e}(e) ). but
the advantage of the present theory is that not only is the function concept the extensional one,
but it includes arbitrary continuous functions and not just the computable ones.»

Страница 539 (в файле - №20):

«What then is a data type? Answer: a type of data.
That is to say, a collection of data that have been grouped together
for reasons of similarity of structure or perhaps mere convenience.
Thus the collection may very well be a mixed bag, but more often than not canons of taste or demands of simplicity
dictate an adherence to regularity. The grouping may be formed to eliminate irrelevant objects and focus the attention in other ways.
It is frequently a matter of good organization that aids the understanding of complex definitions.
In programming languages, one of the major reasons for making an explicit declaration of a data type
(that is, the restriction of certain variables to certain "modes") is that the computed objects of that type can enjoy a special represemation
in the machine that allows the manipulation of thesc objects via the chosen representation to be reasonably efficient.
This is a very critical matter for good language design and good compiler writing.
In this report, however, we cannot discuss the problems of representation, ...

Страница 540 (в файле №21):

«... important as they may be. Our objective here is conceptual organization, and we
wish to show how such ideas, in the language for computable functions used here,
can find the proper expression.»

...

«The main innovation to be described in this section is the use of LAMBDA expressions to define types as well as elements.
Certain expressions define retracts (or better: retraction mappings), and it is the ranges (or as we shall see: sels of finite poinls)
of such retracts that form the groupings into types. Thus LAMBDA provides a calculus of type definitions including recursive
type definitions. Examples will be explained both here and in the following sections.
Note that types as retracts turn out to be types as lattices, that is, types of partial and many-valued objects.
The problem of cutting these lattice types down to the perfect or complete objects is discussed in § 6.
Another view of types and functionality of mappings is presented in § 7.»

Примечание: LAMBDA - это собственное название языка,
а не алиас для буквы λ (не λ-исчисление, не типизированное λ-исчисление, а ещё один язык с именем LAMBDA).

Отредактировано Лис (2024-08-13 22:35:37)