Implementation
Application
In Prolog ... the form ... generator(P) ... fail . Backtracking produces the successive elements of the generator.
% Generators % Natural Numbers nat(0). nat(N) :- nat(M), N is M + 1. % Infinite sequence from I inf(I,I). inf(I,N) :- I1 is I+1, inf(I1,N). % An Alternate definition of natural numbers (more efficient) alt_nat(N) :- inf(0,N). % Sequence of Squares square(N) :- alt_nat(X), N is X*X. % Infinite Arithmetic Series inf(I,J,I) :- I =< J. inf(I,J,N) :- I < J, I1 is J + (J-I), inf(J,I1,N). inf(I,J,I) :- I > J. inf(I,J,N) :- I > J, I1 is J + (J-I), inf(J,I1,N). % Finite Arithmetic Sequences % Numbers between I and J increment by 1 between(I,J,I) :- I =< J. between(I,J,N) :- I < J, I1 is I+1, between(I1,J,N). between(I,J,I) :- I > J. between(I,J,N) :- I > J, I1 is I-1, between(I1,J,N). % Numbers between I and K increment by (J-I) between(I,J,K,I) :- I =< K. between(I,J,K,N) :- I < K, J1 is J + (J-I), between(J,J1,K,N). between(I,J,K,I) :- I > K. between(I,J,K,N) :- I > K, J1 is J + (J-I), between(J,J1,K,N). % Infinite List -- Arithmetic Series the Prefixes inflist(N,[N]). inflist(N,[N|L]) :- N1 is N+1, inflist(N1,L). % Primes -- using the sieve prime(N) :- primes(PL), last(PL,N). % List of Primes primes(PL) :- inflist(2,L2), sieve(L2,PL). sieve([],[]). sieve([P|L],[P|IDL]) :- sieveP(P,L,PL), sieve(PL,IDL). sieveP(P,[],[]). sieveP(P,[N|L],[N|IDL]) :- N mod P > 0, sieveP(P,L,IDL). sieveP(P,[N|L], IDL) :- N mod P =:= 0, L [], sieveP(P,L,IDL). last([N],N). last([H|T],N) :- last(T,N). % Primes -- using the sieve (no list) sprime(N) :- inflist(2,L2), ssieve(L2,N). ssieve([P],P). ssieve([P|L],NP) :- L [], sieveP(P,L,PL), ssieve(PL,NP). % B-Tree Generator -- Inorder traversal (Order important) traverse(btree(Item,LB,RB),I) :- traverse(LB,I). traverse(btree(Item,LB,RB),Item). traverse(btree(Item,LB,RB),I) :- traverse(RB,I). |
Among the primitive types provided by programming languages are
These are the types whose values are are usually represented as bit patterns in the computer.
Aside. Programming language definitions do not place restrictions on the primitive types. However hardware limitations and variation have considerable influence on actual programs so that, integers are an implementation defined range of whole numbers, reals are an implementation defined subset of the rational numbers and characters are an implementation defined set of characters.
Several languages permit the user to define additional primitive types. These primitive types are called enumeration types.
An elementary data object is always manipulated as a unit.
natural, fixed point, complex, and rational numbers
Structured data types: A structured data object is constructed as an aggregate of other data objects.
An abstract type is a type which is defined by its operations rather than its values.
The primitive data types provided in programming languages are abstract types. The representation of integer, real, boolean and character types are hidden from the programmer. The programmer is provided with a set of operations and a high-level representation. The programmer only becomes aware of the lower level when an error such as an arithmetic overflow occurs.
An abstract data type consists of a type name and operations for creating and manipulating objects of the type. A key idea is that of the separation of the implementation from the type definition. The actual format of the data is hidden (information hiding) from the user and the user gains access to the data only through the type operations.
There are two advantages to defining an abstract type as a set of operations. First, the separation of operations from the representation results in data independence. Second, the operations can be defined in a rigorous mathematical manner. As indicated in Chapter Semantics, algebraic definitions provide appropriate method for defining an abstract type. The formal specification of an abstract type can be separated into two parts. A syntactic specification with gives the signature of the operations and a semantic part in which axioms describe the properties of the operations.
In order to be fully abstract, the user of the abstract type must not be permitted access to the representation of values of the type. This is the case with the primitive types. For example, integers might be represented in two's complement binary numbers but there is no way of finding out the representation without going outside the language. Thus, a key concept of abstract types is the hiding of the representation of the values of the type. This means that the representation information must be local to the type definition.
Modula-3's approach is typical. An abstract type is defined using Modules -- a definition module (called an interface), and an implementation module (called a module).
Since the representation of the values of the type is hidden, abstract types must be provided with constructor and destructor operations. A constructor operation composes a value of the type from values from some other type or types while a destructor operation extracts a constituent value from an abstract type. For example, an abstract type for rational numbers might represent rational numbers as pairs of integers. This means that the definition of the abstract type would include an operation which given a pair of integers returns a rational number (whose representation as an ordered pair is hidden) which corresponds to the the quotient of the two numbers. The rational additive and multiplicative identities corresponding to zero and one would be provided also.
Figure~\ref{complex:adtspec}
Figure 3.N: Complex numbers abstract type
DEFINITION MODULE} ComplexNumbers; TYPE Complex; PROCEDURE MakeComplex ( firstNum, secondNum : Real ) : Complex; PROCEDURE AddComplex ( firstNum, secondNum : Complex ) : Complex; PROCEDURE MultiplyComplex ( firstNum, secondNum : Complex ) : Complex; ... END ComplexNumbers.
Figure 3.N: Complex numbers implementation
IMPLEMENTATION MODULE ComplexNumbers; TYPE Complex = POINTER TO} ComplexData; ComplexData = RECORD RealPart, ImPart : REAL}; END; PROCEDURE MakeComplex ( firstNum, secondNum : Real ) : Complex; VAR result : Complex; BEGIN new( result ); result^.RealPart := firstNum; result^.ImPart := secondNum return result END NewComplex; PROCEDURE} AddComplex ( firstNum, secondNum : Complex ) : Complex; VAR result : Complex; BEGIN new( result ); result^.RealPart := firstNum^.RealPart + secondNum^.RealPart; result^.ImPart := firstNum^.ImPart + secondNum^.ImPart return result END AddComplex; ... BEGIN ... END ComplexNumbers.
The terms abstract data type and ADT are also used to denote what we call an abstract type.
Given an abstract type stack, the stack items would be restricted to be a specific type. This means that an abstract type definition is required for stacks which differ only in the element type contained in the stack. Since the code required by the stack operations is virtually identical, a programmer should be able to write the code just once and share the code among the different types of stacks. Generic types or generics are a mechanism to provide for sharing the code. The sharing provided by generics is through permitting the parameterization of type definitions. Figure~\ref{stack:generic} contains a Modula-2 definition module for a generic stack.
Figure 3.N: A Generic Stack
DEFINITION MODULE GenericStack; TYPE stack(ElementType); PROCEDURE Push ( Element:ElementType; Var Stack : stack(ElementType) ); ... END GenericStack
Type Checking type free languages, data type parameterization (polymorphism)
The problem of writing generic sorting routines points out some difficulties with traditional programming languages. A sorting procedure must be able to detect the boundaries between the items it is sorting and it must be able to compare the items to determine the proper ordering among the items. The first problem is solved by parameterizing the sort routine with the type of the items and the second is solved by either parameterizing the sort routine with a compare function or by overloading the relational operators to permit more general comparisons.
Generic packages in Ada is a cheap way to obtain polymorphism. Generic packages are not compiled at compile time, rather they are compiled whenever they are parameterized with a type. So that if a programmer desires to sort a array of integers and an array of reals, the compiler will generate two different sort routines and the appropriate routine is selected at run-time.
Functional languages treat functions as first-class values: they can be passed as parameters, returned as results, built into composite values, and so on. Functions whose parameters are all non-functional are called first-order. A function that has a functional parameter is called a higer-order function or functional. Functional composition is an example of a functional.
double (x) = x * x
quad = double \circ double
twice (f) = f \circ f
odd = not \circ even
Functionals are often used to construct reusable code and to obtain much of the power of imperative programming within the functional paradigm.
An important functional results from partial application For example, suppose there is the function {\tt power} defined as follows:
power ( n, b) = if n = 0 then 1 else b*power(n-1, b)
As written {\tt power} raises a base {\tt b} to a positive integer power {\tt n}. The expression {\tt power(2)} is a function of one argument which when applied to a value returns the square of the value.
(\x.\y.((* x) y) 3 = \y.((* 3) y)
Since functional programs consist of function definitions and expression evaluations they are suitable for program transformation and formal proof just like any other mathematical system. It is the principle of referential transparency that makes this possible. The basic proof rule is that: identifiers may be replaced by their values. For example,
f 0 = 1 f n+1 = (n+1)*(f n)
fp 0 fn = fn fp n+1 in = fp n (n+1)*in
f n = fp n 1
f 0 = fp 0 1 by definition of {\sf f} and {\sf fp}
assume f n = fp n 1
show f n+1 = fp n+1 1
f n+1 = (n+1)*f n
= (n+1)*fp n 1
and
k*fp m n = fp m k*n since
1*fp m n = fp m 1*n
and
(k+1)*fp m n = k*fp m n + fp m n = fp m k*n + fp m n
Aside. which says that an occurrence of x in B can be replaced with e. All bound identifiers in B are renamed so as not to clash with the free identifiers in E.
The operational semantics of the lambda calculus define various operations on lambda expressions which enable lambda expressions to be reduced (evaluated) to a normal form (a form in which no further reductions are possible).
Thus, the operational semantics of the lambda calculus are based on the concept of substitution. A lambda abstraction denotes a function, to apply a lambda abstraction to an argument we use what is called beta-reduction. The following formula is a formalization of beta-reduction.
( lambda x.B M) <--> B[x:M]
The notation B[x:M] means the replacement of free occurrences of x in B with M.
One problem which arises with beta-reduction is the following. Suppose we apply beta-reduction as follows.
( lambda x.B M) <--> B[x:M]where y is a free variable in M but y occurs bound in B. Then upon the substitution of M for x, y becomes bound. To prevent this from occurring, we need to do the following.
To prevent free variables from becoming bound requires the replacement of free variables with new free variable name, a name which does not occur in B.
This type of replacement is called alpha-reduction. The following formula is a formalization of alpha-reduction,
Alpha Reduction: lambda x.B <--> lambda y.B[x:y]
where y is not free in B.
Figure N.2: The Alpha, Beta and Eta Reduction Rules
Alpha-reduction: If y does not occur in B \x.B --> \y.B[x:y] Beta-reduction: (\x.B) e --> B[x:e] Eta-reduction: \x.E x --> E
Figure .: Two lambda expressions, P and Q, are identical, in symbols P \equiv Q, if and only if Q is an exact (symbol by symbol) copy of P.
Note that function application associates to the right.
Figure .: The set of free variables of an \lambda-expression E, denoted by phi(E), is defined as follows:
- phi(x) = {x} for any variable x
- phi(\lambda x.P) = phi(P) -{x}
- phi((P)Q) = phi(P) union phi(Q)
Figure .: Two lambda expressions are considered essentially the same if they differ only in the names of their bound variables.
Figure .: The relation M==> N (read M \beta-reduces to N) is defined as follows:
- M ==> N if M \cong N
- M ==> N if M --> N is an instance of the \beta-rule
- If M ==> N for some M and N, then for any \lambda-expression E, both (M)N ==> (N)E and (E)M ==> (E)N
- If M ==> N for some M and N, then for any variable x, \lambda x.M ==> \lambda x.N also holds.
- If M ==> E and E ==> N then also M ==> N
- M ==> N only as specified above
Figure .: M is \beta-convertable (or simply equal) to N, in symbols M=N, iff M\congN, or M==>N, or N==>M, or there is a \lambda-expression E such that M=E and E=N
Theorem: (Church-Rosser theorem I) If E==> M and E ==> N then there is some Z such that M ==> Z and N ==> Z
If E ==> M and E ==> N, where both M and N are in normal form, then M \cong N
Church-Rosser Theorem I If E1 \leftrightarrow E2 then there is an expression E, such that E1 --> E and E2 --> E.
Theorem: (Church-Rosser theorem II) If E==> M and E = N then there is a Z such that M ==> Z and N ==> Z
Church-Rosser Theorem II If E1 --> E2, and E2 is in normal form, then there exists a normal order reduction sequence from E1 to E.
Integer, Real, Character, Tuples, Lists Enumerations, algebraic types (unions)
Pattern matching, Product type, sequences, functions, ML, Miranda
f 0 = 1 f (n+1) = (n+1)*f(n)
insert (item Empty\_Tree) = BST item Empty\_Tree Empty\_Tree
insert (item BST x LST RST) = BST x insert (item LST) RST if item < x
BST x LST insert( item RST ) if item > x