![]() |
Functional Programs |
![]() |
AProVE Help System → Input Languages → | Functional Programs |
structure nat 0 : nat succ : nat->natIn 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 -> listHowever, 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 -> bThere 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 _.