left

Functional Programs

right
AProVE Help SystemInput LanguagesFunctional Programs
The FP language used by AProVE is a small subset of the functional language Haskell. But in contrast to Haskell, FP uses innermost evaluation. FP is a strict typed first-oder functional programming language, using monomorphic algebraic data structures. An FP-program is a collection of data structures and algorithms. Algebraic data structures are defined by using the keyword structure. The following example shows a definition of nat, which represents the natural numbers using the data type constructors succ and 0.
      structure nat
	0    : nat
	succ : nat->nat
      
In this example 0 stands for the natural number zero and succ is the successor function. The above example makes only use of the type nat, but in general such data type definitions can be hierarchical. How this can be done is show in the following example, in which a data structure for a list of natural numbers is defined.
      structure list
	nil  : list
	cons : nat,list -> list
     
However, any data structure must not be empty, i.e, there must be a constructor ground term of the corresponding type. So a data structure definition like the following one is not allowed.
      structure a
	ac  : b -> a

      structure b
        bc  : a -> b
     
There exists also one predefined data structure named bool which has the two constructors true and false.Based on this data type we are now able to define If-statements. The overall structure of an If-statement is like this:
      if t1 then t2 else t3.      
      
The semantics of this statement is t2, if t1 evaluates to true and t3, if t1 evaluates to false.

Now we know how data structures can be defined in FP, what is missing up to now is how algorithms are defined, which ware working on these data structures. Algorithms in FP are defined by using the keyword function. Assuming that the above shown data structure nat is already defined, one could define the function plus for nat, for example like this:

      function plus : nat, nat -> nat
	 plus(x,0)        = x
	 plus(succ(x), y) = succ(plus(x,y))
      
AProVE uses pattern matching for evaluation like the one used in ordinary term rewriting. But the defining rules have to satisfy some more constraints. The definition of the function has to be complete in the sense that for every term, where f is applied to ground constructor, at least one rule of the function must be applicable. And on the other hand these rules must not be overlapping, i.e., at most one rule of the function must be applicable. Another example for a function is the following one, which defines length for a list of natural numbers.
      function length : list -> nat
	 length(nil)     = 0
	 length(cons(x)) = 1 + length(x)
      
There exists also the possibility to define infix functions. This is done by using Haskell a Haskell like syntax. The example below show a definition of the infix function +.
      function (+) 6: nat, nat -> nat
	 x + 0       = 0
	 x + succ(y) = succ( x + y)
      
The number after the function symbol defines the priority of this function symbol. This can be in the range from 0 to 9, where 0 is the highest priority and 9 is the lowest priority.

For further details on FP please consult the following EBNF.This EBNF is for simplicity reasons not complete. For an exhaustive presentation of FP please look at [Has04] :

      Program             = Declaration { Declaration }.
      Declaration         =  Structure | Function .
      Structure           = "structure" TypeName Constructor [ Constructor ].
      Constructor         = Identifier ":" TypeName [",", TypeName] "->" TypeName.
      Function            = "function" Identifier ":" TypeName [ "," TypeName ] "->" TypeName Rule [Rule].
      Rule                = LeftTerm "=" Term.
      LeftTerm            = FunctionApplication.
      FunctionApplication = Identifier "(" Term ["," Term] ")".
      Term                = "if" Term "then" Term "else" Term   |
                            "if" "(" Term "," Term "," Term ")" |
			    "let" LetList "in" Term             |
			     "(" Term ")"                       |
			     FunctionApplication                |
			     Constant                           |
			     Variable.
      LetList             = Variable "=" Term [ ","  Variable "=" Term ];
      
Variables, Identifiers, Constants and TypeNames could consist of any letter and digit with the only restriction that the first sign is a letter or a _.