Tutorial FoC

Description

A brief FoC tutorialVersion 0.0July, 01, 2003The FoC development teamConservatoire National des Arts et Metiers (CNAM)Institut National de Recherche en Informatique etAutomatique (INRIA)Laboratoire d’Informatique de Paris 6 (LIP6)AbstractIn this tutorial, we show through sample examples the main constructions of FoC.The rst part of this tutorial is a general description of FoC together with a FoCdevelopment of cartesian products of monoids (a set with an associative operationfor which there is a neutral element). In this part, we omit some properties. Thesecond part focuses on proof and explained how to make proof in Coq from a FoCdevelopment. Last, the third part shows how programming within FoC.1Contents1 First steps within FoC 61.1 Starting with FoC: Setoids . . . . . . . . . . . . . . . . . . . . . . . . . . . 61.2 Inheritance: Monoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81.3 Parameterized species: Cartesian product of setoids . . . . . . . . . . . . . 91.4 Multiple inheritance: product of monoids . . . . . . . . . . . . . . 101.5 Collection: Implementation ofZ andZZ . . . . . . . . . . . . . . . . . . 101.6 Compilation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111.6.1 Steps of compilation . . . . . . . . . . . . . . . . . . . . . . . . . . . 111.6.2 Interface of species . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121.6.3 Inheritance graph . . . . . . . . . . . . . . . . . ...

Sujets

• informatique

Informations

• Publié par: Ernae
• Nombre de lectures: 31
• Langue: English

Extrait

A brief FoC tutorial Version 0.0 July, 01, 2003

The FoC development team

ConservatoireNationaldesArtsetMe´tiers(CNAM) Institut National de Recherche en Informatique et Automatique (INRIA) Laboratoire d’Informatique de Paris 6 (LIP6)

Abstract In this tutorial, we show through sample examples the main constructions ofFoC. The first part of this tutorial is a general description ofFoCtogether with aFoC development of cartesian products of monoids (a set with an associative operation for which there is a neutral element). In this part, we omit some properties. The second part focuses on proof and explained how to make proof inCoqfrom aFoC development. Last, the third part shows how programming withinFoC.

1

Contents 1 First steps within FoC 6 1.1 Starting withFoC . . . . . . . . . . . . . . . . . . . . . . . . . . . 6: Setoids 1.2 Inheritance: Monoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.3 Parameterized species: Cartesian product of setoids . . . . . . . . . . . . . 9 1.4 Multiple inheritance: Cartesian product of monoids . . . . . . . . . . . . . . 10 1.5 Collection: Implementation ofZandZ×Z 10. . . . . . . . . . . . . . .. . . 1.6 Compilation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.6.1 Steps of compilation . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.6.2 Interface of species . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.6.3 Inheritance graph . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.6.4 Dependencies graph . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 1.7 More on dependencies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2 Proving properties: from FoC specifications to Coq specifications 17 2.1 Setoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.1.1 Defining a type for setoids . . . . . . . . . . . . . . . . . . . . . . . . 17 2.1.2 Methods of the species of setoids . . . . . . . . . . . . . . . . . . . . 19 2.1.3 Making a setoid . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 2.1.4 Coercion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.2 Monoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.3 Cartesian product of setoids . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2.4 Redefinitions: a little help from theFoC 29. . . . . . . . . . . . . compiler . 3 Programming 30 3.1 Defining data types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3.2 Defining species and collections . . . . . . . . . . . . . . . . . . . . . . . . . 30 3.3 Recursive types and Pattern-matchings . . . . . . . . . . . . . . . . . . . . . 35 3.4 UsingOcamlcode inFoC. . . . . . . . . . . . . . . . . . . . .. . . . . .  36 2

Introduction The aim of theFoCproject is to build an environment dedicated to the development of certified computer algebra libraries. TheFoCenvironment provides a completely formal- ized representation of the relations between mathematical structures, which will serve as a common framework for both proofs and implementations. TheFoCsyntax allows the user to write programs, statements and proofs. Computer algebra libraries are based on a hierarchy of implementations of mathemat- ical structures. In mathematics, algebraic structures are defined according to a rather strict hierarchy: rings come up after groups, which rely themselves on monoids, and so on. In theFoCsystem, we represent these structures byspecieswhich are made of some func- tions, either abstract or defined by appropriate algorithms, as well as properties (some of them are abstract statements to be proved later, while other already have a proof). Going from a species to another along the hierarchy as a lot to do with the notion of inheritance in Object-Oriented Programming and with refinement-based software development. A species can be built from existing species through inheritance and refinement mechanisms provided by theFoCsystem 1 an informal point of view, the. From FoC’ ground concepts are the following ones: EntitiesEntities are the “things” we manipulate. They represent mathematical objects, such as 0,1 orX 2 + 3∗X∗Yin the computer universe. At this level, the main problem is that there is no simple relationship between these two worlds. For instance, the constant 1 of the integer type can be used to represent 1∈ 2 Z Z as well as 1∈ 5Z Z . Of course, it would be a mistake to mix them up, since they do not have the same properties at all. On the other hand, we have a lot of possible representations for the polynomialX it can be+ 2: viewed as an ordered list of coefficients, [1;2] , or as a list of pairs (sparse representation): [(1,1);(2,0)]  this case, adding (or multiplying) two polynomials who don’t share the. In same concrete representation is likely to produce an error. To avoid such confusion, we use an Abstract Data Type (ADT) mechanism: entities are accessible to the end user only through appropriate functions. SpeciesSpecies play a very important role inFoCIndeed they are the nodes of the. hierarchy of structures upon which the library is based. They are the equivalent of the algebraic structures in mathematics. A species can be seen as a set ofmethods, which are identified by their names. A method can be eitherdeclaredordefined.Declared methods reflect the constants, primitive operations, and axioms that define a structure in mathematics, whiledefinedones represent implemented operations and theorems built up (and proved) from the declared methods in a given structure. There are several different categories of methods: •The carrier, or representation type, introduced by the keyword rep , of a species is a type from theFoCit can be an atomic type, a other words, type language. In 1 Note that combining these features may introduce some inconsistencies, invalidating some properties of the formal specifications or even leading to programming errors. Hence, theFoCsystem performs static analyses, which reject such problematic programs.

3

product, an arrow, or parameterized type (such as list(int)  represents the type). It of the entities that the species manipulates. Each speciesmusthave auniquecarrier. •the “computational” methods which can be declared (as a signature) or defined (as a function). Such methods are introduced by the keyword sig when they are declared and by the keyword let  denote the operations that are Theywhen they are defined. allowed on carrier’s inhabitants. •The “non-computational” methods can also be declared or defined. They allow the developer of a new species to specify the properties that further implementations of this species must meet. He may also prove some of these properties through theorems (for the current definitions of functions or properties). –Declared methods introduced by the keyword property express properties that must be satisfied. Hence, before the complete implementation of the species, one will have to prove them. –Defined methods introduced by the keyword letprop correspond to definitions of (non necessary decidable) relations (or predicates). –Defined methods introduced by the keyword theorem express properties that are proved in the context of the species. In this case, the proof itself constitutes the definition. InheritanceThe general mechanism for defining a new species from previous one(s) is calledinheritance If two. Thenew species inherits all the methods of its parent(s).  parents have methods that share the same name, their types must be unifiable. If both methods are defined, then we have to choose the definition that will be exported in the new species. Currently, we have chosen to follow the order of inheritance specified by the species’ developer 2 course, a species is free to define some methods that were . Of previously only declared or even didn’t exist. It can also declare a new method (but not redeclare an old one, since a method must have the same type all along the inheritance graph). At last, it may redefine some methods. For instance, a group inherits from monoid, and declares a new operation (for the opposite) with its axioms. InterfaceEach species defines aninterfacesimply the list of all the methods of the is : it species considered as declared. Interfaces correspond to the end-user point of view, who wants to know which functions he can use, and which properties these functions have, but doesn’t care about the details of the implementation. InFoC, eachspeciesmust have a correspondinginterfaceby abstracting all its defined fields. 2 However, it is not always possible to choose some definitions from speciesAand others from species B, and some coherence checks must be done (that are not needed by the policy chosen yet). For instance, assume we have two speciesAandBthat both defines a recursive functionfand give a prooff endsthat f if we want to build a species that inherits both fromalways terminates. Then,AandB, it won’t be safe to take the definition offinA, and the prooff endsofB. Indeed, the resulting species will have a proof f endsthat does not correspond to the body off.

4

CollectionsAcollection means that every fieldis a completely defined species. This must be defined, and every parameter instantiated. In addition, a collection is “frozen”. Namely, it can not be used as a parent of a species in the inheritance graph. It represents a particular mathematical structure, such asZ, orZ[X]. Moreover, we can not access directly the entities belonging to a given collection. ParametersIn addition, we distinguish between “atomic” species and “parameterized” ones. There are two types of parameters: entities and collections. For instance, a species defining the matrices will take two integers (representing its dimensions) as parameters. This integers are entities of a certain type. For its coefficients, it will also take a collection as argument, which must have at least all the features specified by the interface of ring . Of course, it can be a richer structure, a field for instance. Programming within FoCThe current version of the language is tuned to a kind of functional programming style, in order to ease proofs of correctness. The main pro- gramming features are multiple inheritance, late binding and parameterisation, which are used to build species and an abstraction mechanism, used to build collections. However, programming withFoCleads to a new style of development. one starts by Typically, expressing the specification of the problem, by introducing some properties and some dec- larations. Then, the representation and definitions can be given, step by step. At last, proofs are done. Some pitfalls must be avoided. Sometimes, it is possible to express some facts either by abstract properties or more concretely, using defintions. As late bindings lead to redo proofs def-depending upon definitions, this a very good idea to express prop- erties as abstractly as possible. This leads to a better understanding on what are the properties coming from the specification and the ones which are dependent of the cho- sen representation. In the same spirit, it is sometimes possible to code an algorithm, by considering only some properties of the representation. A good example is Strassen algo- rithm, which computes the product of square matrices of dimension 2 n by decomposing them into matrices of dimension 2 n−1 . Thealgorithm may be written at the species level,  the recursive call being done on matrices of dimension 2 n−1 . Or it may be written at the representation level, the recursive call being done on arrays of dimension 2 n−1  last. This version does not fit withFoCas the mathematical structures are lost in recursivestyle calls. Such a coding cannot reap the benefits of compiler verification and almost forbids proofs.

5

1 First steps within FoC In this section, we present aFoCdevelopment of the productZ×Z development. This is obtained by defining: 1. setoids as non empty sets on which an equivalence relation is defined (equal) 2. monoids as setoids with a binary operation ( mult ) and a particular element (the neutral element one ) 3.Zas a monoid over the typeint. 4. cartesian product of two setoids (which is a setoid) 5. cartesian product of two monoids (which is a monoid) 6.Z×Z Such a development involves the main constructions ofFoC: •nitionsofspeciesdfie)a..,.dsecllconddı¨otes(ı¨onom,s(sitnoZandZ×Z). •declared and defined methods •inheritance (monoids inherits from setoids) and multiple-inheritance (for the carte- sian product of monoids) •parameterized species (for cartesian products) 1.1 Starting with FoC: Setoids The root of the considered hierarchy, developed in a file species general.foc , is the species basic object whose specification is contained in the file basic.foc  our specification. Hence, begins with the two following directives: usesbasics;; openbasics;; The first directive allows to use the definitions contained in the file basics.foc  files. This introduces basic functions over integers and booleans and the root of theFoChierarchy which is the species basic object . By using this directive, in the file species general.foc , names of functions defined in basics.foc has to be prefixed by the name basics . If f is a function defined in a file a file.foc then one can use f in a file another file.foc after the directive uses a file;; by prefixing f as follows a file#f . The second directive ( open ) allows to avoid to prefix the names of functions defined in another files. However, in order to use this directive, each name has to be unique. For instance, if the files file1 and file2 both contain the definition of a function f , it won’t be possible to use the directive open with these two files.

6

The first species which inherits of the root of theFoChierarchy corresponds to setoids. A setoid is a non-empty setEwith an equivalence relation overE(i.e., a reflexive, symetric and transitive relation) and is defined withinFoCas follows: speciessetoidinheritsbasic object= sigequalin self−>self−>bool;(** equal is decidable equality *) (** element returns some element of our non empty setoid *) sigelementin self; propertyequal reflexive:allxin self, !equal(x,x); propertyequal symetric:allx yin self, !equal(x,y)−>!equal(y,x); propertyequal transitive:allx y zin self, !equal(x,y)−>!equal(y,z)−>!equal(x,z); letdifferent(x,y) =basics#not b(!equal(x,y)); theoremsame is not different:allx yin self, !equal(x,y)−>not(!different(x,y)) proof: def:different; decl:equal; assumed; end The species setoid inherits of the root of the hierarchy, the species basic object , containing three methods: the carrier rep and two tools parse and print  carrier is. The only declared in the species basic object (it will be instantiated later during inheritance between species). The function parse , of type 3 string->self , is defined (i.e., implemented) as a function allowing to convert a string into an element of the collection, the function print  Inperforms the inverse conversion. basic object , we provide a generic definition of both: parse always fails, while print returns the constant string "<abst>" . It is up to the more refined species of the hierarchy to define more specialized versions. The species setoid introduces its own methods: • equal and element are methods corresponding to some effective computations (from which executable code will be obtained). Here, they are only declared. Such methods are introduced by the keyword sig  only know that they exist for each setoid: we but we don’t know how they will be implemented. The explicit definitions of these methods will be done later during inheritance. equal is the equivalence relation 3 Recall that in theFoClanguage,selfdenotes the current collection andc!mdenotes the methodm of the collectionc(if the name of the collection is not specified then it isself).

7

over the setoid. Its type is obloself->self-> clearly specifies that it is a binaryand relation between elements of the setoid. Furthermore, this relation is decidable since the type of the result of equal is bool , and then, later, during the definition of this method, one will have to implement a total function of this type and to prove its termination. The method element in order to ensure that a setoid is ais declared non-empty set. •The three methods equal reflexive , equal symetric and equal transitive are also abstract. However they don’t correspond to effective computations: they specify the properties making the relation equal an equivalence relation. Such methods are introduced by the keyword property . Here again, later, during the implementation of the species, one will have to define these methods by providing the proofs of these properties. In theFoClanguage all denotes the universal quantifier∀. Furthermore, as we said, !equal is a shortcut to self!equal and then denotes the method equal of each collection corresponding to an implementation of the species setoid . • different  methods are introduced by theis a “computational” defined method. Such keyword let . Its body uses the _ tion: not b  global”is a function, basics#not b func “ defined in the file basics.foc , corresponding to the negation operator over the type bool . •Last, the method same is not different is introduced by the keyword theorem : it corresponds to a “non-computational” defined method 4 expressing a property, so its definition is a proof which is given after the keyword proof  keyword. The not corresponds to the negation over propositions. First, before the proof, we have to express some dependencies between methods. There are two kinds of dependency. A decl-dependency, introduced inFoCby the keyword decl , specifies a dependency upon methods viewed as declared methods. In this case, the proof will only depend on the types of these methods. In other words,Ais decl-dependent uponBif it suffices to know the type ofBto typeA def-dependency, introduced in. AFoCby the keywork def , specifies a dependency upon methods viewed as defined methods. In this case, the proof will depend both upon the types and the definitions of these methods. In other words,Ais def-dependent uponBif typingArequires to know both the type and the definition ofB our example, the proof depends upon the. In type and the definition of different – it is a def-dependency – while it only depends upon the type of equal (it is not necessary to know how equal is implemented) – it is a decl-dependency. Now, the proof can be done: we write here assumed to express that we don’t want to prove the property. Thus, this property will be viewed as an axiom. 1.2 Inheritance: Monoids We can now define monoids as setoids with a binary operation ( mult ) and a particular element ( one ) from which we can define the declared method element of the species setoid as the result of mult applied to one and one . TheFoCspecification of monoids is defined 4 even if we define it here from the “computational” methodsequalanddifferent

8

as follows: speciesmonoidinheritssetoid= sigmultin self−>self−>self; sigonein self; letelement= !mult(!one,!one); end Of course, the type of the defined method element in the species monoid must be compatible with (i.e., be the same as) the type of element in the species setoid . 1.3 Parameterized species: Cartesian product of setoids WithinFoCone can define a species parameterized by some collections. For,  example, we can define the species of cartesian products of two setoidsaandbas a setoid (thus this new species inherits of the species setoid ) whose carrier is the product of the carrier ofaandband whose methods are defined as follows: speciessetoid product(aissetoid,bissetoid)inheritssetoid= rep=a*b; letequal(x,y) = #and b(a!equal(#first(x),#first(y)), b!equal(#scnd(x),#scnd(y))); proof ofequal reflexive=assumed; proof ofequal symetric=assumed; proof ofequal transitive=assumed; letmk sp(x,y)in self=#crp(x,y); letelement=self!mk sp(a!element,b!element); letprint=funx−> #sc("(", #sc(a!print(#first(x)), #sc(" " , , #sc(b!print(#scnd(x)), ")")))); end In the definition of the method rep , a*b denote a!rep * b!rep  functions. The #crp , #first and #scnd are primitives which allow respectively to obtain a pair, to obtain the first component of a pair, and to obtain the second component of a pair. The method equal 9

defines a relation between two pairs (x 1 , y 1 ) and (x 2 , y 2  that) in a standard way. Remark it is defined from the methods equal of a and b . The method mk sp is introduced in order to be able to build an object “in self ” from entities of a and b 5 . Last, the method element is defined from the methods element of a and b  that we also define the method. Note print . 1.4 Multiple inheritance: Cartesian product of monoids Multiple inheritance is possible withinFoC. For example, we can define the cartesian product of two monoids a and b as a species which inherits both from the species monoid (since the cartesian product of two monoids is also a monoid) and from the species setoid product(a,b)  we write the. HenceFoCspecification as follows: speciesmonoid products(aismonoid,bismonoid) inheritsmonoid,setoid product(a,b) = letone= !mk sp(a!one,b!one); letmult(x,y) =#crp(a!mult(#first(x),#first(y)), b!mult(#scnd(x),#scnd(y))); end Here, the species monoid products inherits of all the methods of its two parents. However, both of them have methods that have the same name: in this case, theFoCcompiler verifies that the types of these methods are unifiable. This is the case in our example. Furthermore, the two methods from which monoid products inherits define the method element : theFoCcompiler solve such a “conflict” by choosing the definition of the last species (containing it) in the list of parent species. In our example, the definition of element will be obtained from the species setoid product . 1.5 Collection: Implementation ofZandZ×Z Now, we can introduce the collection integers implementingZby defining the carrier as int and by defining the methods as basics operations over int  order to give a definition. In 5 Recall that outside of a species, self is an abstract data type.

10

to all the methods, we also have to provide proofs of properties over equal . collectionintegersimplementsmonoid= rep=int; letone=1; letmult=basics#int mult; letequal=basics#base eq; letprint=basics#string of int; letparse=basics#int of string; proof ofequal reflexive=assumed; proof ofequal symetric=assumed; proof ofequal transitive=assumed; end Then, it suffices to implement the species monoid products with integers as parameters to obtainZ×Z. collectionintegers2implementsmonoid products(integers,integers) = end Now, we can define entites of such collections as follows: letfive=integers!parse("5");; letfive 2=integers!mult(#five,#five);; letfoo=integers2!mk sp(#five,#five 2);; letfoo2=integers2!mult(#foo,#foo);; #print string(integers2!print(#foo2));; 1.6 Compilation 1.6.1 Steps of compilation Compilation of aFoCfile is obtained in several steps (in the directory focc ): •fromFoCtoOcamlandCoq [Example]$ focc ../lib/species_tutorial.foc •compilation ofCoqsource [Example]$ coqc ../lib/species_tutorial.v •compilation ofOcamlsource [Example]$ ocamlc ../lib/species_tutorial.mli [Example]$ ocamlc -c -w mv ../lib/species_tutorial.ml [Example]$ ocamlc -I ‘focc -where‘ openmath.cmo caml basics.cmo _ basics.cmo ../lib/species tutorial.ml _

Then, one can execute aFoC our example, we obtain:program. In [Example]$ a.out (25,625)

11