How to write article writing examples

how to develop article writing skills and also describe how to write article writing examples
AnnyPearson Profile Pic
AnnyPearson,Qatar,Researcher
Published Date:03-07-2017
Your Website URL(Optional)
Comment
Chapter 1 Writing a Mizar article in nine easy steps After reading this chapter and doing the exercises, you will be able to write a basic Mizar article all by yourself. The chapter presents an explanation of the nine steps needed to finish a Mizar article. For each step it also shows how this turns out for a specific example. There are exercises too, so you can test your understanding. To be able to read this chapter you should know some basic mathematics but not much. You should know a little bit about: • first order predicate logic • some basic set theory Mizar is based on set theory on top of predicate logic, that’s why. The most difficult part of writing Mizar is finding what you need in the MML which is the name of the Mizar Mathematical Library. Unfortunately that problem has no easy solution. You will discover that apart from that, writing a Mizar article is straight-forward. 1.1 Step 1: the mathematics Before you start writing a Mizar article you need to decide what it should be about. It’s very important not to start writing the article too soon A proof that takes five minutes to explain – after which people look into the air and then mumble: ‘hm, yes, I see’ – takes about a week to formalize. So every improvementtothemathematicsthatyoucanmake beforeyoustartformalizing will pay off very much. The example As a running example in this chapter we write a small Mizar article called my_mizar.miz. It is about Pythagorean triples. Those are triples 12 CHAPTER 1. WRITING A MIZAR ARTICLE IN NINE EASY STEPS of natural numbersa,b,c for which holds that: 2 2 2 a +b =c ThePythagoreantheoremtellsusthatthesetriplescorrespondtosquareangled triangles that have sides of integer length. The best known of these triples are 3,4,5 and5,12,13 but there are an infinite number of them. The theorem that we will formalize says that all Pythagorean triples are given by the formula: 2 2 2 2 a =n −m b= 2mn c =n +m or are multiples of such a triple. For instance the triple 3,4,5 is given by n =2, m =1, and the triple5,12,13 is given by n = 3,m = 2. The proofof the theoremisstraight-forward. You onlyneeds toconsiderthe case where a and b are relative prime. Some thought about parity gives that one of the a andb has to be even, and that the other andc is odd. Then if b is the even number of the two we get that:      2 2 2 b c −a c−a c+a = = 2 4 2 2 But if the product of two relativeprime numbers is a square, then both of those numbers are squares. So you get: c−a c+a 2 2 =m =n 2 2 which leads to the required formula. Exercise 1.1.1 Study the Mizar Mathematical Library and try to decide whether Mizar is equally suited to all fields of mathematics and computer sci- ence, or that Mizar is best suited to certain subjects. In the latter case, what is most easily formalized in Mizar? And what least? Exercise 1.1.2 We mentioned the Pythagorean theorem which says that the 2 2 2 sides a, b and c of a square angled triangle satisfy a +b = c . Try to find this theorem in the MML. If it’s there, in what article does it occur and what is the theorem’s reference? If not, or if you don’t like the version that you find (exercise for when you finished this chapter): write an article that proves it. 1.2 Step 2: the empty Mizar article In order to write a Mizar article you need a working Mizar system and a file to put the Mizar article in. In fact, as you will find out, you will need two files: a .miz file for your article and a .voc file for its vocabulary. In this tutorial we follow the Windows conventions of naming files. For Mizar under Unix the backslashes should go the other way. So what is called text\my_mizar.mizhere, under Unix should be text/my_mizar.miz.1.2. STEP 2: THE EMPTY MIZAR ARTICLE 3 We will assume that you already have a properly installed Mizar system. For a description of how to install Mizar see the readme.txt file that is in the Mizar distribution (under Unix it is called README). To write your article, you need to be in a directory that has two subdirecto- ries called text and dict. If those directories don’t exist yet, make them. Put in the text directory an empty file called my_mizar.miz and put in the dict directory an empty file called my_mizar.voc. (Replace the my_mizar with a more appropriate name if you are writing an article of your own.) The smallest legal .voc file is empty but the smallest legal .miz file looks like this: environ begin Use your favorite text editor to put those two lines in the my_mizar.miz file. Then check it using the command: mizf text\my_mizar.miz It will both check syntax and mathematics of your article. If everything is well this command prints something like: Make Environment, Mizar Ver. 7.0.01 (Win32/FPC) Copyright (c) 1990,2004 Association of Mizar Users -Vocabularies-Constructors-Clusters-Notation Verifier, Mizar Ver. 7.0.01 (Win32/FPC) Copyright (c) 1990,2004 Association of Mizar Users Processing: text\my_mizar.miz Parser 2 0:00 Analyzer 0:00 Checker 1 0:00 Time of mizaring: 0:00 meaning that this ‘article’ contains no errors. (If you use the emacs editor with its Mizar mode you don’t need to type the mizf command. In that case all you need to do to check the file is hit C-c RET.) Apart from the my_mizar.mizfile, the textdirectorynow contains25other files. You never need to look inside them. They are only used internally by the Mizar system. The next step is to connect the .miz file to the .voc vocabulary. Add a vocabulariesdirective to your article: environ vocabularies MY_MIZAR; begin4 CHAPTER 1. WRITING A MIZAR ARTICLE IN NINE EASY STEPS (Important: the name of the vocabulary has to be written in capitals This is a remnant of Mizar’s DOS origins.) Now the article is ready to be written. For the moment add some line of text at the end of the file just to find out what happens if the article contains errors: environ vocabularies MY_MIZAR; begin hello Mizar After you run the mizf text\my_mizar.mizcommand again, Mizar will insert the error messages inside your file. It will put a with a number below any error. Also there will be an explanation of those error numbers at the end of the file. So after running the mizf command again your file looks like: environ vocabularies MY_MIZAR; begin hello Mizar :: 143,321 :: 143: No implicit qualification :: 321: Predicate symbol or "is" expected There is no need to try to understand those two error messages, because of course hello Mizaris not legalMizar. So removethis line, now that youhave seen what Mizar thinks of it. You don’t need to removethe error message lines. They vanish the next time you run mizf. The lines containing error messages can be recognized because they start with ::. Mizar only gives you error numbers. It never prints anything about why it thinks it is wrong. Sometimes this lack of explanation is frustrating but generally Mizar errors are quite obvious. Exercise 1.2.1 The minimal Mizar article that we showed is 2 lines long. What is the shortest article in the MML? What is the longest? What is the average number of lines in the articles in the MML? As a rule of thumb an article less than a 1000lines is considered too shortto be submitted to the MML. However several articles in the MML are less than a 1000 lines long since articles are shortened during revision of the MML. How many of the articles in the MML are currently shorter than a 1000 lines? Exercise 1.2.2 Copy an article from the MML to your private text direc- tory. Check that the Mizar checker mizf processes it without error messages. Experiment with making small modifications to it and see whether Mizar can detect where you tampered with it. Put one screen-full of non-Mizar text – for instance from a Pascal or C program – somewhere in the middle of the article. How many error messages1.3. STEP 3: THE STATEMENT 5 will you get? Can Mizar sufficiently recover from those errors to check the second half of the file reasonably well? 1.3 Step 3: the statement To start translating your mathematics to Mizar you need to write the theorem that you want to prove in Mizar syntax. Therearetwothings about Mizarsyntaxthat areimportant foryouto note: • TherearenospellingvariantsinMizar. AlthoughMizarresemblesnatural language a lot, it is a formal language and there are no possibilities to choose between phrasings. For example: and means something different from & not means something different from non such that means something different from st assume means something different from suppose NAT means something different from Nat means something different from natural So you should really pay attention to the exact keywords in the Mizar syntax. It’s not enough if it resembles it. The only exception to this rule is that be and being are alternative spellings. So although it’s more natural to write let X be set and for X being set holds ... you are also allowed to write let X being set and for X be set holds ... • There is no distinction in Mizar between ‘function notation’and ‘operator notation’. In most programming languages something like f(x,y) and x+y are syntactically different things. In Mizar this distinction doesn’t exist. In Mizar everything is an operator. If you write f(x,y) in Mizar then it really is a ‘operator symbol’ f with zero left arguments and two right arguments. Similarly predicate names and type names can be any string of characters that you might wish. You can mix letters, digits and any other character you might like in them. So for instance if you want to call a predicate \/-distributiveyou can do so in Mizar. And it will be one ‘symbol’. If you are not sure what characters go together as a symbol in a Mizar formula, you can go to the web pages of the MML abstracts. In those pages the symbols are hyperlinks that point to definitions. So just click on them to find out what symbol they are. TowriteMizaryouneed to knowhowto writetermsandhowto writeformulas. We tackle this in top-down fashion. First we describe how to translate formulas from predicate logic into Mizar. Then we describe how the syntax of Mizar terms works.6 CHAPTER 1. WRITING A MIZAR ARTICLE IN NINE EASY STEPS 1.3.1 Formulas Here is a table that shows all you want to know about how to write predicate logic in Mizar: ⊥ contradiction ¬φ not φ φ∧ψ φ & ψ φ∨ψ φ or ψ φ⇒ψ φ implies ψ φ⇔ψ φ iff ψ ∃x.ψ ex x st ψ ∀x.ψ for x holds ψ ∀x.(φ⇒ψ) for x st φ holds ψ Thereisnospecialwaytowrite⊤inMizar. Oneusuallywritesnotcontradic- tionforthis. Note that with the quantifiersit should be stand not such that. Also note that for x stφ holdsψ is just ‘syntactic sugar’ for for x holds (φ implies ψ). After the parser processed it, the rest of the system will not see any difference between those two formulas. Using this table you now can write logical formulas in Mizar. There is one more thing that you need to know to write Mizar formulas in practice. Mizar is a typed language. We will discuss Mizar types in detail in Section 1.3.4 below, but the types turn up in the predicate logic formulas too. All variables that you use in formulas need to have a type. There are two ways to give a variable a type: • Put the type in the formula using a being type attribution. For instance you can write an existential formula about natural numbersm andn as: ex m,n being Nat st ... • Give the type for the variable with a reserve statement. This doesn’t introduce a variable, it just introduces a notation convention. If you use a reserve statement you can leave out the type in the formula: reserve m,n for Nat; ex m,n st ... This way of typing variables in formulas is much more convenient than explicitely typing the variables and so it is the method that is generally used. Exercise 1.3.1 Translate the following Mizar formulas into predicate logic notation: φ iff not not φ not (φ & ψ) implies not φ or not ψ1.3. STEP 3: THE STATEMENT 7 ex x st φ implies ψ for x st for y st φ holds ψ holds χ To do this exercise you need to know the priorities of the logical operators in Mizar. They are the usual ones in predicate logic: ex/for implies/iff or & not This means that you should read not φ implies ψ as (not φ) implies ψ (because the not binds stronger), but that ex x stφ impliesψ means ex x st (φ impliesψ). Exercise 1.3.2 Translate the following predicate logic formulas into Mizar syntax: ¬φ⇔¬¬¬φ ¬(φ∨ψ)⇒ (¬φ∧¬ψ) ∃x.(φ∧ψ)   ∃x. ∃y.(φ⇒ψ) ⇒χ 1.3.2 Relations You still need to know how to write atomic formulas. In Mizar there are two ways to write those: • If R is a predicate symbol, write: x ,x ,...,x Rx ,...,x 1 2 m m+1 m+n Both m or n might be 0, in which case this becomes prefix or postfix notation. Note that postfix notation can have more than one argument, as for instance in x,y are_relative_prime. Please note that brackets around the arguments of the predicate are not allowed. • IfT is a type, or the adjectives part of a type, write: x is T For instance you can write x is prime. We will discuss types in Section 1.3.4 below. To find out what relations are available to you, you will need to browse the MML. Here is a short list of some of the most frequent used relations to get you started.8 CHAPTER 1. WRITING A MIZAR ARTICLE IN NINE EASY STEPS = = 6= ≤ = ∈ in ⊆ c= The first character in the Mizar representation of⊆ is the letter c. 1.3.3 Terms There are three ways to write Mizar terms: • If f is an operator symbol, which Mizar calls a functor, write: (x ,x ,...,x )f (x ,...,x ) 1 2 m m+1 m+n Again, m or n might be 0, in which case this becomes prefix or postfix notation. As an example of a postfix operator there is 2 for square. The bracketsaroundeither list of argumentscan be omitted if there is just one argument. • IfL andR are bracket symbols, write: Lx ,x ,...,x R 1 2 n In this case brackets ( and ) around the arguments are not necessary, since the symbols themselves are already brackets. An example of this kind of term is the ordered pair x,y. In that case n = 2,L is andR is . • Any natural number is a Mizar term. If you write natural numbers, you should add to your environ the line: requirements SUBSET, NUMERALS, ARITHM; because else they won’t behave like natural numbers. The word functor for function symbol or operator symbol is Mizar terminology. It has nothing to do with the notion of functor in category theory. It is used to distinguish a function symbol in the logic from a function object in the set theory (which is a set of pairs). Againtofindoutwhatoperatorsareavailabletoyou,youwillneedtobrowse the MML. Here is a short list of some of the most frequent used operators to get you started.1.3. STEP 3: THE STATEMENT 9 ∅ x x x,y x,y X∪Y X \/ Y X∩Y X /\ Y N NAT Z INT R REAL x+y x + y x−y x - y −x -x xy xy x/y x/y 2 x x2 y x x to_powery √ x sqrt x P(X) boolX (x,y) x,y X×Y :X,Y: X Y Funcs(X,Y) f(x) f.x hi D hxi x hx,yi x,y p·q pq Thedigit2ispartofthesymbolforthesquareoperator. Thelastfouroperators are used to build finite sequences over the set D. The .operationisfunction application inside the set theory. If f isasymbol in the language representing a functor with zero left arguments and one right argument then you write: f x or (you can always put a term in brackets): f(x) If f is a function in the set theory – a set of pairs – then f.x is the image of x under f, in other words it is the y such that x,y in f. Exercise 1.3.3 Translate the following Mizar formulas into mathematical notation: NAT c= REAL 1/0 = 010 CHAPTER 1. WRITING A MIZAR ARTICLE IN NINE EASY STEPS sqrt -1 in REAL sqrt(x2) x x /\ -x = x /\ 0 x,y = x,y,x p = p.1,p.2 Exercise 1.3.4 Translate the following mathematical formulas into Mizar syntax: √ x+y xy≤ 2 √ (−1, 2)∈Z×R X∩Y ⊆X∪Y X Y ∈P(P(X×Y)) hx,yi =hxi·hyi p·hi =p f(g(x)) = 6 g(f(x)) 1.3.4 Types: modes and attributes The one thing left for you to understand to write Mizar formulas is Mizar’s types. Although Mizar is based on ZF-style set theory – so the objects of Mizar are untyped – the terms of Mizar are typed. An example of a Mizar type is: non empty finite Subset of NAT This type should be parsed as: non empty finite Subset of NAT A Mizar type consists of an instance of a mode with in front a cluster of adjec- tives. The type without the adjectives is called the radix type. In this case the mode is Subset and its argument is NAT, the radix type is Subset of NAT, and the two adjectives are non empty and finite. To put this abstractly, a Mizar type is written: α α ... α M of x ,x ,...,x 1 2 m 1 2 n1.3. STEP 3: THE STATEMENT 11 where α , ... α are adjectives, M is a mode symbol and x , x , ..., x are 1 m 1 2 n terms. The keyword of binds the arguments of the mode to the mode. It’s like the brackets in a term. Thenumberofargumentsnispartofthedefinitionofthemode. Forinstance for set it is zero. You can’t write set of ..., because there does not exist a set mode that takes arguments. Modes are dependent types. To find out what modes are available to you, you will need to browse the MML. Here is a short list of some of the most frequent used modes to get you started. set number Element of X Subset of X Nat Integer Real Ordinal Relation Relation of X,Y Function Function of X,Y FinSequence of X NotethattherebotharemodesRelationandFunctionwithnoarguments,and morespecificmodesRelationofX,YandFunctionofX,Ywithtwoarguments. They share the mode symbol but they are different. Also note that the modes depend on terms. So there are no types represent- ingthefunctionsfromatypetoatype. TheFunctionmoderepresentsthefunc- tions from a set to a set. As an example the function space (X →Y)×X →Y corresponds to the Mizar type Function of :Funcs(X,Y),X:,Y Adjectives restrict a radix type to a subtype. They either are an attribute, or the negation of an attribute using the keyword non. Again, to find out what attributes are available to you, you will need to browse the MML. Here is a list of a few attributes. empty even odd prime natural integer real finite infinite countable12 CHAPTER 1. WRITING A MIZAR ARTICLE IN NINE EASY STEPS Maybe you now wonder about how types are used in Mizar. To clarify this take a look at three Mizar notions – NAT, Nat and natural – that all mean the same thing: the set of natural numbers. Here is a table that compares their uses: meaning declaration formula n∈N n in NAT n :N n be Nat n is Nat n :N n be natural number n is natural NAT is a term, Nat is a type and naturalis an adjective. be/beingare a typing in a declaration and go between a variable and a type. in is the ∈ relation of the set theory and goes between two terms. is goes between a term and a type or between a term and an adjective. Note that in Mizar you can have a ‘type judgement’ as a formula in the logic. The example We now give the statement of the theorem for the example. The statement that we will prove in this chapter is: reserve a,b,c,m,n for Nat; a2 + b2 = c2 & a,b are_relative_prime & a is odd implies ex m,n st m = n & a = n2 - m2 & b = 2mn & c = n2 + m2; So put this after the begin line of your my_mizar.miz file. We also could have made the quantification of the a, b and c explicit: for a,b,c st a2 + b2 = c2 & a,b are_relative_prime & a is odd holds ex m,n st m = n & a = n2 - m2 & b = 2mn & c = n2 + m2; but it is not necessary. Mizar automatically quantifies over free variables. We now analyze this statement in some detail. The formula has the struc- ture: φ & φ & φ implies ex m,n st φ & φ & φ & φ ; 1 2 3 4 5 6 7 The predicate logic formula that corresponds to this is: (φ ∧φ ∧φ )⇒∃m,n.(φ ∧φ ∧φ ∧φ ) 1 2 3 4 5 6 7 The first three atomic formulas in this are: φ ≡ a2 + b2 = c2 1 φ ≡ a,b are_relative_prime 2 φ ≡ a is odd 3 They have the structure: φ ≡ t = t 1 1 2 φ ≡ t ,t are relative prime 2 3 4 φ ≡ t is T 3 51.3. STEP 3: THE STATEMENT 13 In this = and are_relative_prime are predicate symbols. T is the adjective odd. So we here see both kinds of atomic formula: twice a relation between terms and once a typing. The first term t inφ is: 1 1 t ≡ a2 + b2 1 It has the structure: t ≡ u + u 1 1 2 u ≡ v 2 1 1 u ≡ v 2 2 2 v ≡ a 1 v ≡ b 2 In this + and 2 are functor symbols. Exercise 1.3.5 Find Mizar types for the following concepts: odd number that is not a prime number empty finite sequence of natural numbers uncountable set of reals element of the empty set non-empty subset of the empty set What is the problem with the last two concepts? Do you think they should be allowed in Mizar? Study this manual to find out whether they are. Exercise 1.3.6 Write the following statements as Mizar formulas: The only even prime number is 2. If a prime number divides a product it divides one of the factors. There is no biggest prime number. There are infinitely many prime twins. Every even number≥ 4 is the sum of two primes. Write these statements first using reserve statements. Then write them again but this time with the types in the formulas.14 CHAPTER 1. WRITING A MIZAR ARTICLE IN NINE EASY STEPS 1.4 Step 4: getting the environment right Add the statement that you wrote to your article. Then check it. You will get error messages: environ vocabularies MY_MIZAR; begin reserve a,b,c,m,n for Nat; :: 151 a2 + b2 = c2 & a,b are_relative_prime & a is odd implies ::,203 ex m,n st m = n & a = n2 - m2 & b = 2mn & c = n2 + m2; :: 151: Unknown mode format :: 203: Unknown token, maybe the forbidden underscore character used in an identifier That’sbecauseyoudidn’timportwhatyouusedfromtheMML.There’snothing wrong with the statement, there’s something wrong with the environment (it’s empty). To correct this, you need to add directives to the environ part of the article to import what you need. It is hard to get the environment of a Mizar article correct. In practice people often just copy the environment of an old article. However that doesn’t help much when it doesn’t work, and occasionally it doesn’t work. So you still will have to understand how the environment works, to get it right when you get environment related errors. Exercise 1.4.1 Try to use an environment of an existing article from the MML. Do the errors go away? If so, you might consider the rest of Step 4 for now, and just use this environment. 1.4.1 Vocabulary, notations, constructors The rule is quite simple. For everything you use – predicate, functor, mode or attribute – you have to add a relevant reference to three directives: • vocabularies • notations • constructors Thelistofreferencesfornotationsand constructorsisgenerallyalmostiden- tical. In fact, if you follow the algorithm from this section to get them right they will be identical. These directives are about:1.4. STEP 4: GETTING THE ENVIRONMENT RIGHT 15 • Lexical analysis. The tokens in a Mizar article come from lists called vo- cabularies. Mizar variables are identifiers with a fixed syntax, but the predicates, functors, types and attributes all are symbols which can con- tain any character. You need to indicate from what vocabularies you use symbols. • Parsing of expressions. To have an expression you need to list the ar- ticles that you use predicates, functors, types and attributes from. The notations directive is for the syntax of expressions. The constructors directive is for its meaning. Here is a list of what was use in the statement, what kind of thing it is, and what vocabularies and articles you need for it: symbol kind vocabulary article = pred HIDDEN = pred HIDDEN XXREAL_0 + func HIDDEN XCMPLX_0 func HIDDEN XCMPLX_0 - func ARYTM_1 XCMPLX_0 Nat mode HIDDEN NAT_1 are_relative_prime pred ARYTM_3 INT_2 2 func SQUARE_1 SQUARE_1 odd attr MATRIX_2 ABIAN You don’t need to refer to the HIDDEN vocabulary or the HIDDEN article but you need to list the others. The vocabularies should go in the vocabularies directive and the articles should go both in the notations and constructors directives. So your environment needs to be: environ vocabularies MY_MIZAR, ARYTM_1, ARYTM_3, SQUARE_1, MATRIX_2; notations XXREAL_0, XCMPLX_0, NAT_1, INT_2, SQUARE_1, ABIAN; constructors XXREAL_0, XCMPLX_0, NAT_1, INT_2, SQUARE_1, ABIAN; Here is the way to find out what the vocabulary and article a given symbol are: • To find the vocabulary use the command: findvoc -w ’symbol’ For instance the command: findvoc -w ’-’ gives:16 CHAPTER 1. WRITING A MIZAR ARTICLE IN NINE EASY STEPS FindVoc, Mizar Ver. 7.0.01 (Win32/FPC) Copyright (c) 1990,2003 Association of Mizar Users vocabulary: ARYTM_1 O- 32 The O means that this is a functor symbol, and 32 is the priority. • Tofindthearticle,theeasiestwayistogotothewebpagesoftheabstracts of the MML on the Mizar web site, find a use of the symbol somewhere, and click on it to go to the definition. Exercise 1.4.2 Find out what is in the HIDDEN vocabulary by typing: listvoc HIDDEN For each of the 25 symbols in this vocabulary, find an article that introduces a notation that uses it. 1.4.2 Redefinitions and clusters But now things get tough. It turns out that your environment still does not work The problem is that the types are wrong. If you check the article with the new environment you get: a2 + b2 = c2 & a,b are_relative_prime & a is odd implies :: 103 ex m,n st m = n & a = n2 - m2 & b = 2mn & c = n2 + m2; :: 102 103 103 103 :: 102: Unknown predicate :: 103: Unknown functor To get rid of this kind of typing problems is the most difficult part of writing a Mizar article. (In practice this kind of error often is caused because a cluster is missing. So if you are completely mystified by a Mizar typing error, start thinking ‘cluster’) The errors that you see here are indeed almost all caused by the fact that some clusters are not imported in the environment. This causes the expressions not to have the right types. For instance the first error is caused by the fact that a2 and b2 have type Element of REAL, while the + wants its arguments to have type complex number. We will show in detail why this is the case, and how to fix this by importing the right clusters. A Mizar expression doesn’t have just one type, it has a whole set of types. For instance, with the right environment the number 2 has the following types:1.4. STEP 4: GETTING THE ENVIRONMENT RIGHT 17 Nat natural number prime Nat Integer integer number even Integer Real real number Complex complex number Ordinal ordinal number set finite set non empty set ... There are two ways to influence the types of an expression. • To give a specific expression a more precise radix type, you use redefini- tions. A functor can have many redefinitions that cause it to get different types depending on the types of its arguments. Here is an example of a redefinition taken from PEPIN: definition let n be Nat; redefine func n2 - Nat; end; What this does is change the type of some of the terms that use the 2 operator. The original definition (of which this is a redefinition) is in SQUARE_1: definition let x be complex number; func x2 - set equals x x; end; In SQUARE_1 there already are two other redefinitions of 2: definition let x be Element of COMPLEX; redefine func x2 - Element of COMPLEX; end; definition let x be Element of REAL; redefine func x2 - Element of REAL; end; Now suppose that in your environment you have the directive:18 CHAPTER 1. WRITING A MIZAR ARTICLE IN NINE EASY STEPS notations ..., SQUARE_1, PEPIN, ...; Thenifyouwriteanexpressiont2,thetypeofthisexpressionwilldepend on the type of t. All definitions and redefinitions of 2 will be considered in the order that they are imported through the notations directive. So in this case the definition for complex number is first, then there is the redefinition for Element of COMPLEX, then the redefinition for Element of REAL, and finally (go to the next article, which is PEPIN) there is the redefinition for Nat. Nowtheruleisthatthe last redefinitionthatfitsthetypeofallarguments applies. So if t has type Nat then t2 has type Nat too, while if t does not have any of the types Element of COMPLEX or Element of REAL or Nat, then it will have type set. Note that since the the order of the articles in the notations directive is important for this • To generatemore adjectivesfor an expression, Mizarhas something called clusters. The process of adding adjectives according to these clusters is called the rounding up of clusters. Here are three examples of clusters, taken from FINSET_1. registration cluster empty - finite set; end; This means that every set that has adjective emptyalso will get adjective finite. registration let B be finite set; cluster - finite Subset of B; end; This means that every expression that has type Subset of B where B has type finite set also will get adjective finite. registration let X,Y be finite set; cluster X \/ Y - finite; end; This means that every expression of the shape X \/ Y where X and Y have type finite set also will get adjective finite. These examples show both kinds of cluster that add adjectives to the set of types of an expression. The first two do this based on the type of the expression (this is called ‘rounding up’ a type), and the third add adjectives based on the shape of the expression.1.4. STEP 4: GETTING THE ENVIRONMENT RIGHT 19 Tosummarize: redefinitionsarefornarrowingtheradixtypeandclustersarefor extending the set of adjectives. (There are also redefinitions that have nothing to do with typing – because they redefine something different from the type – and a third kind of cluster that has nothing to do with adding adjectives. You should not be confused by this.) You can alwaystest whether some typeT is in the set of types of an expres- sion t by changing it to (t qua T). You get an error if t didn’t have T in its set of types. In that case you might start looking for a redefinition or cluster that changes this situation. The example The first error in the example: a2 + b2 = c2 & a,b are_relative_prime & a is odd implies :: 103 ex m,n st m = n & a = n2 - m2 & b = 2mn & c = n2 + m2; :: 102 103 103 103 :: 102: Unknown predicate :: 103: Unknown functor is that the + in a2 + b2 is not well-typed. (The of the error message 103 indicates the position of the error. In this case it is below the + symbol.) The definition of 2 that is in effect here is from SQUARE_1: definition let x be Element of REAL; redefine func x2 - Element of REAL; end; and the definition of + is from XCMPLX_0: definition let x,y be complex number; func x+y means ... ... end; Sothisshowsthatyouwouldlikea2andb2whichhavetypeElementofREAL to also get type complex number. This means that you want these expressions to get an extra adjective – the adjective complex – and so you need a cluster. (Once again: for more adjectives you need clusters, while for a more precise radix type you need a redefinition.) It turns out that an appropriate cluster is in XCMPLX_0: registration cluster - complex Element of REAL; end; After you add registrations XCMPLX_0;20 CHAPTER 1. WRITING A MIZAR ARTICLE IN NINE EASY STEPS to the environment the first error indeed is gone and you only have two errors left: a2 + b2 = c2 & a,b are_relative_prime & a is odd implies ex m,n st m = n & a = n2 - m2 & b = 2mn & c = n2 + m2; :: 102 103 :: 102: Unknown predicate :: 103: Unknown functor The next error (the 102 below the =) is similar to the previous one. The = predicateexpects argumentsof type realnumber,but mand nhavetype Nat. If youstudy the MMLforsometime youwill find that Natisthe sameas Element of omega (the definition of Nat in NAT_1 and the synonym in NUMBERS.) Thereforethe followingtwoclustersgiveyouwhat youneed. FromARYTM_3: registration ... cluster - natural Element of omega; end; and from XREAL_0: registration cluster natural - real number; ... end; The cluster directive now has become: registrations XCMPLX_0, ARYTM_3, XREAL_0; With this directive in the environment the only error left is: a2 + b2 = c2 & a,b are_relative_prime & a is odd implies ex m,n st m = n & a = n2 - m2 & b = 2mn & c = n2 + m2; :: 103 :: 103: Unknown functor This erroris caused by the fact that Mizardoes not consider 2 to be a Nat. You will see below, after the discussion of the requirementdirective, how to get rid of this final error. 1.4.3 The other directives Here is a list of the eight kinds of directives in the environ and the kind of reference they take: