powerset :: [a] -> [[a]]
powerset [] = [[]] -- (1)
powerset (x:xs) = powset ++ [x:ys | ys <- powset] -- (2)
where
powset = powerset xs
Statement: |powerset ys| = 2^|ys|
(We use the shorthand notation |ys| to mean length ys.)
|powerset []| = | [ [] ] | -- using (1) = 1 -- obvious: definition of "|.|" (length)OK!
|powerset ys| = |powerset x:xs| -- since ys = x:xs = |powerset xs ++ [x:ys | ys <- powerset xs]| -- definition (2) of powerset = |powerset xs| + |[x:ys | ys <- powerset xs]| -- prop. of "++" and "|.|" = |powerset xs| + |powerset xs| -- prop. of list comprehension = 2^|xs| + 2^|xs| -- by INDUCTION ASSUMPTION = 2^(1+|xs|) -- maths = 2^|x:xs| -- prop. of ":" and "|.|"
data Mydatatype = Case_1 | Case_2 | ... | Case_n... each "branch" of the data type corresponds to one case in the induction. Some branches will be base cases of the induction (if they are not recursive, i.e., don't depend on Mydatatype), while others will be induction steps (if they are recursive, i.e., contain Mydatatype).
For example x[2*j+1] := sqrt(u+v) is a command (also called (assignment) statement) with two expressions embedded in it: 2*j+1 and sqrt(u+v) .
Evaluation is the process of computing the value denoted by an expression.
Definition:
In more conventional languages like C, a variable declaration creates a binding between an identifier and a storage location. The declaration may or may not initialize the variable, i.e. bind the location to a value.
One of the most fundamental commands is the assignment command. An assignment changes (i.e., updates "destructively" since the old value is lost) the value that is bound to a storage location.
This is a main "feature" of imperative programming languages, that is, whose main structure (within a possible block structure) is a sequence of commands:
...
do_something(x,y,z);
z := do_something_else(x,17.0);
....
while (...) {
... do_this(...);
... do_that(...);
}
..
Variables are created and initialized by declarations. More formally, the effect of a declaration is to produce one or more bindings between an identifier and a value.
In (pure) functional languages like Haskell, variables cannot be updated (there is no "destructive assignment"). Instead, an identifier like myexpr0 above, denotes either a constant (recall that in Haskell constants are also functions), or it is a formal parameter of a definition/declaration of the function. For example, x and s in the following Haskell fragment are formal parameters:
push :: a -> Stack a -> Stack a push x s = ... x ... s ...Formal parameters exist also in traditional imperative or object-oriented languages.
When a function (in Haskell), a procedure (in Pascal), or a method (in object-oriented terminology) is called, we supply the actual parameters:
Main> push 2 (push 1 create)
type boolean = {false, true};
const mynot1: array [boolean] of boolean := [true, false];
function mynot2 (x: boolean): boolean;
begin
if x then return false else return true;
end;
Conceptually mynot1 and mynot2 both have the same
mapping type, i.e. Bool -> Bool
In Haskell the syntax for constant declarations and function declarations are really the same thing:
mynot1 x = if x then False else True -- a function mynot2 = mynot1 -- a (constant) function
create :: Stack a -- create an empty stack push :: a -> Stack a -> Stack a -- push an element on the stack pop :: Stack a -> (a, Stack a) -- pop an element off the stack empty :: Stack a -> Bool -- is the stack empty?Note the modifed pop which now returns the popped off (formerly topmost) element. Hence the axioms for pop change:
pop (push x s) = (x, s) pop (create) ==> error
public class Stack
{
private Object[] stackArray;
private int maxSize, top;
public Stack( int s )
{
maxSize = s;
stackArray = new Object[ maxSize ];
top = -1;
}
public void push( Object j )
{ stackArray[ ++top ] = j; }
public Object pop()
{ return stackArray[ top-- ]; }
public boolean isEmpty()
{ return ( top == -1 ); }
}
Alternatively, we can use an ADT: in Java the signature of an
ADT is called an interface:
public interface Stack
{
...
public void push( Object j );
public Object pop();
public boolean empty();
}
(Note that we don't return a stack..)
And here is an implementation using linked lists
public class ListStack implements Stack
{
private Node top;
private Int nItems;
public create () { top = null; nItems = 0; }
public void push( Object j )
{
Node newNode = new Node( j, top );
top = newNode; nItems++;
}
public Node pop()
{
Object tmp = top.getKey();
top = top.getNext(); nItems--;
return tmp;
}
public boolean empty() { return ( top == null ); }
}
Here we have made use of a class Node
public class Node
{
private Object key;
private Node next;
public Node( Object k, Node n )
{ key = k; next = n; }
public Object getKey()
{ return key; }
public Node getNext()
{ return next; }
public void setKey( Object k )
{ key = k; }
public void setNext( Node n )
{ next = n; }
}