text:
Lecture Notes on the Lambda Calculus
- Winifred James
- 2 years ago
- Views:
1 Lecture Notes on the Lambda Calculus Peter Selinger Department of Mathematics and Statistics Dalhousie University, Halifax, Canada Abstract This is a set of lecture notes that developed out of courses on the lambda calculus that I taught at the University of Ottawa in 2001 and at Dalhousie University in 2007 and Topics covered in these notes include the untyped lambda calculus, the Church-Rosser theorem, combinatory algebras, the simply-typed lambda calculus, the Curry-Howard isomorphism, weak and strong normalization, polymorphism, type inference, denotational semantics, complete partial orders, and the language PCF. Contents 1 Introduction Extensional vs. intensional view of functions The lambda calculus Untyped vs. typed lambda-calculi Lambda calculus and computability Connections to computer science Connections to logic Connections to mathematics The untyped lambda calculus Syntax
2 2.2 Free and bound variables,α-equivalence Substitution Introduction toβ-reduction Formal definitions of β-reduction and β-equivalence Programming in the untyped lambda calculus Booleans Natural numbers Fixed points and recursive functions Other data types: pairs, tuples, lists, trees, etc The Church-Rosser Theorem Extensionality, η-equivalence, and η-reduction Statement of the Church-Rosser Theorem, and some consequences Preliminary remarks on the proof of the Church-Rosser Theorem Proof of the Church-Rosser Theorem Exercises Combinatory algebras Applicative structures Combinatory completeness Combinatory algebras The failure of soundness for combinatory algebras Lambda algebras Extensional combinatory algebras Simply-typed lambda calculus, propositional logic, and the Curry- Howard isomorphism Simple types and simply-typed terms Connections to propositional logic Propositional intuitionistic logic
3 6.4 An alternative presentation of natural deduction The Curry-Howard Isomorphism Reductions in the simply-typed lambda calculus A word on Church-Rosser Reduction as proof simplification Getting mileage out of the Curry-Howard isomorphism Disjunction and sum types Classical logic vs. intuitionistic logic Classical logic and the Curry-Howard isomorphism Weak and strong normalization Definitions Weak and strong normalization in typed lambda calculus Polymorphism Syntax of System F Reduction rules Examples Booleans Natural numbers Pairs Church-Rosser property and strong normalization The Curry-Howard isomorphism Supplying the missing logical connectives Normal forms and long normal forms The structure of closed normal forms Application: representation of arbitrary data in System F Type inference Principal types
4 9.2 Type templates and type substitutions Unifiers The unification algorithm The type inference algorithm Denotational semantics Set-theoretic interpretation Soundness Completeness The language PCF Syntax and typing rules Axiomatic equivalence Operational semantics Big-step semantics Operational equivalence Operational approximation Discussion of operational equivalence Operational equivalence and parallel or Complete partial orders Why are sets not enough, in general? Complete partial orders Properties of limits Continuous functions Pointed cpo s and strict functions Products and function spaces The interpretation of the simply-typed lambda calculus in complete partial orders Cpo s and fixed points
5 12.9 Example: Streams Denotational semantics of PCF Soundness and adequacy Full abstraction Acknowledgements Bibliography 120 5
6 1 Introduction 1.1 Extensional vs. intensional view of functions What is a function? In modern mathematics, the prevalent notion is that of functions as graphs : each function f has a fixed domain X and codomain Y, and a functionf : X Y is a set of pairsf X Y such that for eachx X, there exists exactly one y Y such that (x,y) f. Two functions f,g : X Y are considered equal if they yield the same output on each input, i.e.,f(x) = g(x) for all x X. This is called the extensional view of functions, because it specifies that the only thing observable about a function is how it maps inputs to outputs. However, before the 20th century, functions were rarely looked at in this way. An older notion of functions is that of functions as rules. In this view, to give a function means to give a rule for how the function is to be calculated. Often, such a rule can be given by a formula, for instance, the familiar f(x) = x 2 or g(x) = sin(e x ) from calculus. As before, two functions are extensionally equal if they have the same input-output behavior; but now we can also speak of another notion of equality: two functions are intensionally 1 equal if they are given by (essentially) the same formula. When we think of functions as given by formulas, it is not always necessary to know the domain and codomain of a function. Consider for instance the function f(x) = x. This is, of course, the identity function. We may regard it as a function f : X X for any set X. In most of mathematics, the functions as graphs paradigm is the most elegant and appropriate way of dealing with functions. Graphs define a more general class of functions, because it includes functions that are not necessarily given by a rule. Thus, when we prove a mathematical statement such as any differentiable function is continuous, we really mean this is true for all functions (in the mathematical sense), not just those functions for which a rule can be given. On the other hand, in computer science, the functions as rules paradigm is often more appropriate. Think of a computer program as defining a function that maps input to output. Most computer programmers (and users) do not only care about the extensional behavior of a program (which inputs are mapped to which outputs), but also about how the output is calculated: How much time does it take? How much memory and disk space is used in the process? How much communication bandwidth is used? These are intensional questions having to do with the 1 Note that this word is intentionally spelled intensionally. 6
7 particular way in which a function was defined. 1.2 The lambda calculus The lambda calculus is a theory of functions as formulas. It is a system for manipulating functions as expressions. Let us begin by looking at another well-known language of expressions, namely arithmetic. Arithmetic expressions are made up from variables (x, y, z...), numbers (1,2,3,...), and operators ( +,, etc.). An expression such asx+y stands for the result of an addition (as opposed to an instruction to add, or the statement that something is being added). The great advantage of this language is that expressions can be nested without any need to mention the intermediate results explicitly. So for instance, we write and not A = (x+y) z 2, letw = x+y, then letu = z 2, then let A = w u. The latter notation would be tiring and cumbersome to manipulate. The lambda calculus extends the idea of an expression language to include functions. Where we normally write Let f be the functionx x 2. Then considera = f(5), in the lambda calculus we just write A = (λx.x 2 )(5). The expressionλx.x 2 stands for the function that mapsxtox 2 (as opposed to the statement that x is being mapped to x 2 ). As in arithmetic, we use parentheses to group terms. It is understood that the variable x is a local variable in the term λx.x 2. Thus, it does not make any difference if we write λy.y 2 instead. A local variable is also called a bound variable. One advantage of the lambda notation is that it allows us to easily talk about higher-order functions, i.e., functions whose inputs and/or outputs are themselves functions. An example is the operation f f f in mathematics, which takes a 7
8 function f and maps it to f f, the composition of f with itself. In the lambda calculus,f f is written as λx.f(f(x)), and the operation that mapsf tof f is written as λf.λx.f(f(x)). The evaluation of higher-order functions can get somewhat complex; as an example, consider the following expression: ( (λf.λx.f(f(x)))(λy.y 2 ) ) (5) Convince yourself that this evaluates to 625. Another example is given in the following exercise: Exercise 1. Evaluate the lambda-expression ( ((λf.λx.f(f(f(x))))(λg.λy.g(g(y))) ) (λz.z +1) ) (0). We will soon introduce some conventions for reducing the number of parentheses in such expressions. 1.3 Untyped vs. typed lambda-calculi We have already mentioned that, when considering functions as rules, is not always necessary to know the domain and codomain of a function ahead of time. The simplest example is the identity functionf = λx.x, which can have any setx as its domain and codomain, as long as domain and codomain are equal. We say thatf has the typex X. Another example is the functiong = λf.λx.f(f(x)) that we encountered above. One can check that g maps any function f : X X to a functiong(f) : X X. In this case, we say that the type ofg is (X X) (X X). By being flexible about domains and codomains, we are able to manipulate functions in ways that would not be possible in ordinary mathematics. For instance, if f = λx.x is the identity function, then we havef(x) = x for anyx. In particular, we can takex = f, and we get f(f) = (λx.x)(f) = f. 8
9 Note that the equation f(f) = f never makes sense in ordinary mathematics, since it is not possible (for set-theoretic reasons) for a function to be included in its own domain. As another example, let ω = λx.x(x). Exercise 2. What isω(ω)? We have several options regarding types in the lambda calculus. Untyped lambda calculus. In the untyped lambda calculus, we never specify the type of any expression. Thus we never specify the domain or codomain of any function. This gives us maximal flexibility. It is also very unsafe, because we might run into situations where we try to apply a function to an argument that it does not understand. Simply-typed lambda calculus. In the simply-typed lambda calculus, we always completely specify the type of every expression. This is very similar to the situation in set theory. We never allow the application of a function to an argument unless the type of the argument is the same as the domain of the function. Thus, terms such asf(f) are ruled out, even iff is the identity function. Polymorphically typed lambda calculus. This is an intermediate situation, where we may specify, for instance, that a term has a type of the form X X for all X, without actually specifying X. As we will see, each of these alternatives has dramatically different properties from the others. 1.4 Lambda calculus and computability In the 1930 s, several people were interested in the question: what does it mean for a function f : N N to be computable? An informal definition of computability is that there should be a pencil-and-paper method allowing a trained person to calculate f(n), for any givenn. The concept of a pencil-and-paper method is not so easy to formalize. Three different researchers attempted to do so, resulting in the following definitions of computability: 1. Turing defined an idealized computer we now call a Turing machine, and postulated that a function is computable (in the intuitive sense) if and only if it can be computed by such a machine. 9
10 2. Gödel defined the class of general recursive functions as the smallest set of functions containing all the constant functions, the successor function, and closed under certain operations (such as compositions and recursion). He postulated that a function is computable (in the intuitive sense) if and only if it is general recursive. 3. Church defined an idealized programming language called the lambda calculus, and postulated that a function is computable (in the intuitive sense) if and only if it can be written as a lambda term. It was proved by Church, Kleene, Rosser, and Turing that all three computational models were equivalent to each other, i.e., each model defines the same class of computable functions. Whether or not they are equivalent to the intuitive notion of computability is a question that cannot be answered, because there is no formal definition of intuitive computability. The assertion that they are in fact equivalent to intuitive computability is known as the Church-Turing thesis. 1.5 Connections to computer science The lambda calculus is a very idealized programming language; arguably, it is the simplest possible programming language that is Turing complete. Because of its simplicity, it is a useful tool for defining and proving properties of programs. Many real-world programming languages can be regarded as extensions of the lambda calculus. This is true for all functional programming languages, a class that includes Lisp, Scheme, Haskell, and ML. Such languages combine the lambda calculus with additional features, such as data types, input/output, side effects, updatable memory, object orientated features, etc. The lambda calculus provides a vehicle for studying such extensions, in isolation and jointly, to see how they will affect each other, and to prove properties of programming language (such as: a well-formed program will not crash). The lambda calculus is also a tool used in compiler construction, see e.g. [8, 9]. 1.6 Connections to logic In the 19th and early 20th centuries, there was a philosophical dispute among mathematicians about what a proof is. The so-called constructivists, such as Brouwer and Heyting, believed that to prove that a mathematical object exists, one 10
11 must be able to construct it explicitly. Classical logicians, such as Hilbert, held that it is sufficient to derive a contradiction from the assumption that it doesn t exist. Ironically, one of the better-known examples of a proof that isn t constructive is Brouwer s proof of his own fixed point theorem, which states that every continuous function on the unit disk has a fixed point. The proof is by contradiction and does not give any information on the location of the fixed point. The connection between lambda calculus and constructive logics is via the proofsas-programs paradigm. To a constructivist, a proof (of an existence statement) must be a construction, i.e., a program. The lambda calculus is a notation for such programs, and it can also be used as a notion for (constructive) proofs. For the most part, constructivism has not prevailed as a philosophy in mainstream mathematics. However, there has been renewed interest in constructivism in the second half of the 20th century. The reason is that constructive proofs give more information than classical ones, and in particular, they allow one to compute solutions to problems (as opposed to merely knowing the existence of a solution). The resulting algorithms can be useful in computational mathematics, for instance in computer algebra systems. 1.7 Connections to mathematics One way to study the lambda calculus is to give mathematical models of it, i.e., to provide spaces in which lambda terms can be given meaning. Such models are constructed using methods from algebra, partially ordered sets, topology, category theory, and other areas of mathematics. 2 The untyped lambda calculus 2.1 Syntax The lambda calculus is a formal language. The expressions of the language are called lambda terms, and we will give rules for manipulating them. Definition. Assume given an infinite set V of variables, denoted by x,y,z etc. The set of lambda terms is given by the following Backus-Naur Form: Lambda terms: M,N ::= x (MN) (λx.m) 11
12 The above Backus-Naur Form (BNF) is a convenient abbreviation for the following equivalent, more traditionally mathematical definition: Definition. Assume given an infinite set V of variables. Let A be an alphabet consisting of the elements ofv, and the special symbols (, ), λ, and.. Let A be the set of strings (finite sequences) over the alphabeta. The set of lambda terms is the smallest subset Λ A such that: Wheneverx V thenx Λ. WheneverM,N Λ then(mn) Λ. Wheneverx V andm Λ then(λx.m) Λ. Comparing the two equivalent definitions, we see that the Backus-Naur Form is a convenient notation because: (1) the definition of the alphabet can be left implicit, (2) the use of distinct meta-symbols for different syntactic classes (x, y, z for variables and M, N for terms) eliminates the need to explicitly quantify over the setsv andλ. In the future, we will always present syntactic definitions in the BNF style. The following are some examples of lambda terms: (λx.x) ((λx.(xx))(λy.(yy))) (λf.(λx.(f(fx)))) Note that in the definition of lambda terms, we have built in enough mandatory parentheses to ensure that every term M Λ can be uniquely decomposed into subterms. This means, each term M Λ is of precisely one of the forms x, (M N), (λx.m). Terms of these three forms are called variables, applications, and lambda abstractions, respectively. We use the notation(mn), rather thanm(n), to denote the application of a function M to an argument N. Thus, in the lambda calculus, we write (fx) instead of the more traditionalf(x). This allows us to economize more efficiently on the use of parentheses. To avoid having to write an excessive number of parentheses, we establish the following conventions for writing lambda terms: Convention. We omit outermost parentheses. For instance, we write MN instead of(mn). Applications associate to the left; thus, MNP means (MN)P. This is convenient when applying a function to a number of arguments, as infxyz, which means((f x)y)z. 12
13 The body of a lambda abstraction (the part after the dot) extends as far to the right as possible. In particular, λx.mn means λx.(mn), and not (λx.m)n. Multiple lambda abstractions can be contracted; thus λxyz.m will abbreviateλx.λy.λz.m. It is important to note that this convention is only for notational convenience; it does not affect the official definition of lambda terms. Exercise 3. (a) Write the following terms with as few parenthesis as possible, without changing the meaning or structure of the terms: (i) (λx.(λy.(λz.((xz)(yz))))), (ii) (((ab)(cd))((ef)(gh))), (iii) (λx.((λy.(yx))(λv.v)z)u)(λw.w). (b) Restore all the dropped parentheses in the following terms, without changing the meaning or structure of the terms: (i) xxxx, (ii) λx.xλy.y, (iii) λx.(xλy.yxx)x. 2.2 Free and bound variables,α-equivalence In our informal discussion of lambda terms, we have already pointed out that the terms λx.x and λy.y, which differ only in the name of their bound variable, are essentially the same. We will say that such terms are α-equivalent, and we write M = α N. In the rare event that we want to say that two terms are precisely equal, symbol for symbol, we say thatm andn are identical and we writem N. We reserve = as a generic symbol used for different purposes. An occurrence of a variable x inside a term of the form λx.n is said to be bound. The corresponding λx is called a binder, and we say that the subterm N is the scope of the binder. A variable occurrence that is not bound is free. Thus, for example, in the term M (λx.xy)(λy.yz), x is bound, but z is free. The variable y has both a free and a bound occurrence. The set of free variables ofm is{y,z}. 13
14 More generally, the set of free variables of a termm is denotedfv(m), and it is defined formally as follows: FV(x) = {x}, FV(MN) = FV(M) FV(N), FV(λx.M) = FV(M)\{x}. This definition is an example of a definition by recursion on terms. In other words, in defining FV(M), we assume that we have already defined FV(N) for all subterms of M. We will often encounter such recursive definitions, as well as inductive proofs. Before we can formally define α-equivalence, we need to define what it means to rename a variable in a term. If x,y are variables, and M is a term, we write M{y/x} for the result of renamingxasy inm. Renaming is formally defined as follows: x{y/x} y, z{y/x} z, if x z, (MN){y/x} (M{y/x})(N{y/x}), (λx.m){y/x} λy.(m{y/x}), (λz.m){y/x} λz.(m{y/x}), if x z. Note that this kind of renaming replaces all occurrences of x by y, whether free, bound, or binding. We will only apply it in cases where y does not already occur inm. Finally, we are in a position to formally define what it means for two terms to be the same up to renaming of bound variables : Definition. We define α-equivalence to be the smallest congruence relation = α on lambda terms, such that for all termsm and all variablesy that do not occur in M, λx.m = α λy.(m{y/x}). Recall that a relation on lambda terms is an equivalence relation if it satisfies rules (refl), (symm), and (trans). It is a congruence if it also satisfies rules (cong) and (ξ). Thus, by definition, α-equivalence is the smallest relation on lambda terms satisfying the six rules in Table 1. It is easy to prove by induction that any lambda term is α-equivalent to another term in which the names of all bound variables are distinct from each other and from any free variables. Thus, when we manipulate lambda terms in theory and 14
15 (refl) (symm) (trans) M = M M = N N = M M = N N = P M = P (cong) (ξ) (α) M = M N = N MN = M N M = M λx.m = λx.m y M λx.m = λy.(m{y/x}) Table 1: The rules for alpha-equivalence in practice, we can (and will) always assume without loss of generality that bound variables have been renamed to be distinct. This convention is called Barendregt s variable convention. As a remark, the notions of free and bound variables and α-equivalence are of course not particular to the lambda calculus; they appear in many standard mathematical notations, as well as in computer science. Here are four examples where the variablex is bound. 1 0 x2 dx 10 x=1 1 x lim x e x int succ(int x) { return x+1; } 2.3 Substitution In the previous section, we defined a renaming operation, which allowed us to replace a variable by another variable in a lambda term. Now we turn to a less trivial operation, called substitution, which allows us to replace a variable by a lambda term. We will writem[n/x] for the result of replacingxbyn inm. The definition of substitution is complicated by two circumstances: 1. We should only replace free variables. This is because the names of bound variables are considered immaterial, and should not affect the result of a substitution. Thus, x(λxy.x)[n/x] is N(λxy.x), and not N(λxy.N). 15
16 2. We need to avoid unintended capture of free variables. Consider for example the term M λx.yx, and let N λz.xz. Note that x is free in N and bound in M. What should be the result of substituting N for y in M? If we do this naively, we get M[N/y] = (λx.yx)[n/y] = λx.nx = λx.(λz.xz)x. However, this is not what we intended, since the variable x was free in N, and during the substitution, it got bound. We need to account for the fact that the x that was bound in M was not the same x as the one that was free inn. The proper thing to do is to rename the bound variable before the substitution: M[N/y] = (λx.yx )[N/y] = λx.nx = λx.(λz.xz)x. Thus, the operation of substitution forces us to sometimes rename a bound variable. In this case, it is best to pick a variable fromv that has not been used yet as the new name of the bound variable. A variable that is currently unused is called fresh. The reason we stipulated that the set V is infinite was to make sure a fresh variable is always available when we need one. Definition. The (capture-avoiding) substitution of N for free occurrences of x in M, in symbolsm[n/x], is defined as follows: x[n/x] N, y[n/x] y, if x y, (MP)[N/x] (M[N/x])(P[N/x]), (λx.m)[n/x] λx.m, (λy.m)[n/x] λy.(m[n/x]), if x y andy FV(N), (λy.m)[n/x] λy.(m{y /y}[n/x]), if x y,y FV(N), andy fresh. This definition has one technical flaw: in the last clause, we did not specify which fresh variable to pick, and thus, technically, substitution is not well-defined. One way to solve this problem is to declare all lambda terms to be identified up to α-equivalence, and to prove that substitution is in fact well-defined modulo α- equivalence. Another way would be to specify which variable y to choose: for instance, assume that there is a well-ordering on the set V of variables, and stipulate that y should be chosen to be the least variable that does not occur in either M orn. 16
17 2.4 Introduction to β-reduction Convention. From now on, unless stated otherwise, we identify lambda terms up to α-equivalence. This means, when we speak of lambda terms being equal, we mean that they are α-equivalent. Formally, we regard lambda terms as equivalence classes modulo α-equivalence. We will often use the ordinary equality symbol M = N to denote α-equivalence. The process of evaluating lambda terms by plugging arguments into functions is called β-reduction. A term of the form (λx.m)n, which consists of a lambda abstraction applied to another term, is called a β-redex. We say that it reduces to M[N/x], and we call the latter term the reduct. We reduce lambda terms by finding a subterm that is a redex, and then replacing that redex by its reduct. We repeat this as many times as we like, or until there are no more redexes left to reduce. A lambda term without anyβ-redexes is said to be in β-normal form. For example, the lambda term(λx.y)((λz.zz)(λw.w)) can be reduced as follows. Here, we underline each redex just before reducing it: (λx.y)((λz.zz)(λw.w)) β (λx.y)((λw.w)(λw.w)) β (λx.y)(λw.w) β y. The last term, y, has no redexes and is thus in normal form. We could reduce the same term differently, by choosing the redexes in a different order: As we can see from this example: (λx.y)((λz.zz)(λw.w)) β y. - reducing a redex can create new redexes, - reducing a redex can delete some other redexes, - the number of steps that it takes to reach a normal form can vary, depending on the order in which the redexes are reduced. We can also see that the final result, y, does not seem to depend on the order in which the redexes are reduced. In fact, this is true in general, as we will prove later. If M and M are terms such that M β M, and if M is in normal form, then we say thatm evaluates tom. 17
18 Not every term evaluates to something; some terms can be reduced forever without reaching a normal form. The following is an example: (λx.xx)(λy.yyy) β (λy.yyy)(λy.yyy) β (λy.yyy)(λy.yyy)(λy.yyy) β... This example also shows that the size of a lambda term need not decrease during reduction; it can increase, or remain the same. The term (λx.xx)(λx.xx), which we encountered in Section 1, is another example of a lambda term that does not reach a normal form. 2.5 Formal definitions ofβ-reduction and β-equivalence The concept ofβ-reduction can be defined formally as follows: Definition. We define single-step β-reduction to be the smallest relation β on terms satisfying: (β) (cong 1 ) (cong 2 ) (ξ) (λx.m)n β M[N/x] M β M MN β M N N β N MN β MN M β M λx.m β λx.m Thus,M β M iffm is obtained fromm by reducing a singleβ-redex ofm. Definition. We write M β M if M reduces to M in zero or more steps. Formally, β is defined to be the reflexive transitive closure of β, i.e., the smallest reflexive transitive relation containing β. Finally, β-equivalence is obtained by allowing reduction steps as well as inverse reduction steps, i.e., by making β symmetric: Definition. We write M = β M if M can be transformed into M by zero or more reduction steps and/or inverse reduction steps. Formally, = β is defined to be the reflexive symmetric transitive closure of β, i.e., the smallest equivalence relation containing β. 18
19 Exercise 4. This definition of β-equivalence is slightly different from the one given in class. Prove that they are in fact the same. 3 Programming in the untyped lambda calculus One of the amazing facts about the untyped lambda calculus is that we can use it to encode data, such as booleans and natural numbers, as well as programs that operate on the data. This can be done purely within the lambda calculus, without adding any additional syntax or axioms. We will often have occasion to give names to particular lambda terms; we will usually use boldface letters for such names. 3.1 Booleans We begin by defining two lambda terms to encode the truth values true and false : T = λxy.x F = λxy.y Let and be the termλab.abf. Verify the following: and TT β and TF β and FT β and FF β T F F F Note that T and F are normal forms, so we can really say that a term such as and TT evaluates to T. We say that and encodes the boolean function and. It is understood that this coding is with respect to the particular coding of true and false. We don t claim that and M N evaluates to anything meaningful if M or N are terms other than T and F. Incidentally, there is nothing unique about the term λab.abf. It is one of many possible ways of encoding the and function. Another possibility isλab.bab. Exercise 5. Find lambda terms or and not that encode the boolean functions or and not. Can you find more than one term? 19
20 Moreover, we define the term if then else = λx.x. This term behaves like an if-then-else function specifically, we have if then else TMN β if then else FMN β M N for all lambda termsm,n. 3.2 Natural numbers If f and x are lambda terms, and n 0 a natural number, write f n x for the term f(f(...(fx)...)), wheref occursntimes. For each natural numbern, we define a lambda term n, called the nth Church numeral, as n = λfx.f n x. Here are the first few Church numerals: 0 = λfx.x 1 = λfx.fx 2 = λfx.f(fx) 3 = λfx.f(f(fx))... This particular way of encoding the natural numbers is due to Alonzo Church, who was also the inventor of the lambda calculus. Note that 0 is in fact the same term as F; thus, when interpreting a lambda term, we should know ahead of time whether to interpret the result as a boolean or a numeral. The successor function can be defined as follows: succ = λnf x.f(nf x). What does this term compute when applied to a numeral? succ n = (λnfx.f(nfx))(λfx.f n x) β λfx.f((λfx.f n x)fx) β λfx.f(f n x) = λfx.f n+1 x = n+1 Thus, we have proved that the term succ does indeed encode the successor function, when applied to a numeral. Here are possible definitions of addition and multiplication: add = λnmf x.nf(mf x) mult = λnmf.n(mf). 20
Summary Last Lecture. Automated Reasoning. Outline of the Lecture. Definition sequent calculus. Theorem (Normalisation and Strong Normalisation)
Summary Summary Last Lecture sequent calculus Automated Reasoning Georg Moser Institute of Computer Science @ UIBK Winter 013 (Normalisation and Strong Normalisation) let Π be a proof in minimal logicMore information
CMCS 312: Programming Languages Lecture 3: Lambda Calculus (Syntax, Substitution, Beta Reduction) Acar & Ahmed 17 January 2008
CMCS 312: Programming Languages Lecture 3: Lambda Calculus (Syntax, Substitution, Beta Reduction) Acar & Ahmed 17 January 2008 Contents 1 Announcements 1 2 Introduction 1 3 Abstract Syntax 1 4 Bound andMore information
WHAT ARE MATHEMATICAL PROOFS AND WHY THEY ARE IMPORTANT? introduction Many students seem to have trouble with the notion of a mathematical proof. People that come to a course like Math 216, who certainlyMore information
CHAPTER 7 GENERAL PROOF SYSTEMS 1 Introduction Proof systems are built to prove statements. They can be thought as an inference machine with special statements, called provable statements, or sometimesMore information
Mathematical Induction. Lecture 10-11
Mathematical Induction Lecture 10-11 Menu Mathematical Induction Strong Induction Recursive Definitions Structural Induction Climbing an Infinite Ladder Suppose we have an infinite ladder: 1. We can reachMore information
Mathematics for Computer Science/Software Engineering. Notes for the course MSM1F3 Dr. R. A. Wilson
Mathematics for Computer Science/Software Engineering Notes for the course MSM1F3 Dr. R. A. Wilson October 1996 Chapter 1 Logic Lecture no. 1. We introduce the concept of a proposition, which is a statementMore information
3. Mathematical Induction
3. MATHEMATICAL INDUCTION 83 3. Mathematical Induction 3.1. First Principle of Mathematical Induction. Let P (n) be a predicate with domain of discourse (over) the natural numbers N = {0, 1,,...}. If (1)More information
CS 3719 (Theory of Computation and Algorithms) Lecture 4
CS 3719 (Theory of Computation and Algorithms) Lecture 4 Antonina Kolokolova January 18, 2012 1 Undecidable languages 1.1 Church-Turing thesis Let s recap how it all started. In 1990, Hilbert stated aMore information
Induction. Margaret M. Fleck. 10 October These notes cover mathematical induction and recursive definition
Induction Margaret M. Fleck 10 October 011 These notes cover mathematical induction and recursive definition 1 Introduction to induction At the start of the term, we saw the following formula for computingMore information
Introducing Functions
Functions 1 Introducing Functions A function f from a set A to a set B, written f : A B, is a relation f A B such that every element of A is related to one element of B; in logical notation 1. (a, b 1More information
(LMCS, p. 317) V.1. First Order Logic. This is the most powerful, most expressive logic that we will examine.
(LMCS, p. 317) V.1 First Order Logic This is the most powerful, most expressive logic that we will examine. Our version of first-order logic will use the following symbols: variables connectives (,,,,More information
This chapter is all about cardinality of sets. At first this looks like a
CHAPTER Cardinality of Sets This chapter is all about cardinality of sets At first this looks like a very simple concept To find the cardinality of a set, just count its elements If A = { a, b, c, d },More information
Theory of Computation Lecture Notes
Theory of Computation Lecture Notes Abhijat Vichare August 2005 Contents 1 Introduction 2 What is Computation? 3 The λ Calculus 3.1 Conversions: 3.2 The calculus in use 3.3 Few Important Theorems 3.4 WorkedMore information
Basic Concepts of Point Set Topology Notes for OU course Math 4853 Spring 2011
Basic Concepts of Point Set Topology Notes for OU course Math 4853 Spring 2011 A. Miller 1. Introduction. The definitions of metric space and topological space were developed in the early 1900 s, largelyMore information
CARDINALITY, COUNTABLE AND UNCOUNTABLE SETS PART ONE With the notion of bijection at hand, it is easy to formalize the idea that two finite sets have the same number of elements: we just need to verifyMore information
Reading 13 : Finite State Automata and Regular Expressions
CS/Math 24: Introduction to Discrete Mathematics Fall 25 Reading 3 : Finite State Automata and Regular Expressions Instructors: Beck Hasti, Gautam Prakriya In this reading we study a mathematical modelMore information
Sets and Cardinality Notes for C. F. Miller
Sets and Cardinality Notes for 620-111 C. F. Miller Semester 1, 2000 Abstract These lecture notes were compiled in the Department of Mathematics and Statistics in the University of Melbourne for the useMore information
Elementary Number Theory We begin with a bit of elementary number theory, which is concerned
CONSTRUCTION OF THE FINITE FIELDS Z p S. R. DOTY Elementary Number Theory We begin with a bit of elementary number theory, which is concerned solely with questions about the set of integers Z = {0, ±1,More information
M.Sc. program in mathematics INTRODUCTORY SET THEORY Katalin Károlyi Department of Applied Analysis, Eötvös Loránd University H-1088 Budapest, Múzeum krt. 6-8. CONTENTS 1. SETS Set, equal sets, subset,More information
Parametric Domain-theoretic models of Linear Abadi & Plotkin Logic
Parametric Domain-theoretic models of Linear Abadi & Plotkin Logic Lars Birkedal Rasmus Ejlers Møgelberg Rasmus Lerchedahl Petersen IT University Technical Report Series TR-00-7 ISSN 600 600 February 00More information
[Refer Slide Time: 05:10]
Principles of Programming Languages Prof: S. Arun Kumar Department of Computer Science and Engineering Indian Institute of Technology Delhi Lecture no 7 Lecture Title: Syntactic Classes Welcome to lectureMore information
Mathematical Induction
Mathematical Induction In logic, we often want to prove that every member of an infinite set has some feature. E.g., we would like to show: N 1 : is a number 1 : has the feature Φ ( x)(n 1 x! 1 x) HowMore information
Chapter 7: Functional Programming Languages
Chapter 7: Functional Programming Languages Aarne Ranta Slides for the book Implementing Programming Languages. An Introduction to Compilers and Interpreters, College Publications, 2012. Fun: a languageMore information
Chapter 4, Arithmetic in F [x] Polynomial arithmetic and the division algorithm.
Chapter 4, Arithmetic in F [x] Polynomial arithmetic and the division algorithm. We begin by defining the ring of polynomials with coefficients in a ring R. After some preliminary results, we specializeMore information
Computability Theory
CSC 438F/2404F Notes (S. Cook and T. Pitassi) Fall, 2014 Computability Theory This section is partly inspired by the material in A Course in Mathematical Logic by Bell and Machover, Chap 6, sections 1-10.More information
You know from calculus that functions play a fundamental role in mathematics.
CHPTER 12 Functions You know from calculus that functions play a fundamental role in mathematics. You likely view a function as a kind of formula that describes a relationship between two (or more) quantities.More information
Lecture 16 : Relations and Functions DRAFT
CS/Math 240: Introduction to Discrete Mathematics 3/29/2011 Lecture 16 : Relations and Functions Instructor: Dieter van Melkebeek Scribe: Dalibor Zelený DRAFT In Lecture 3, we described a correspondenceMore information
2. Methods of Proof Types of Proofs. Suppose we wish to prove an implication p q. Here are some strategies we have available to try.
2. METHODS OF PROOF 69 2. Methods of Proof 2.1. Types of Proofs. Suppose we wish to prove an implication p q. Here are some strategies we have available to try. Trivial Proof: If we know q is true thenMore information
Finite Sets. Theorem 5.1. Two non-empty finite sets have the same cardinality if and only if they are equivalent.
MATH 337 Cardinality Dr. Neal, WKU We now shall prove that the rational numbers are a countable set while R is uncountable. This result shows that there are two different magnitudes of infinity. But weMore information
Notes on Complexity Theory Last updated: August, 2011. Lecture 1
Notes on Complexity Theory Last updated: August, 2011 Jonathan Katz Lecture 1 1 Turing Machines I assume that most students have encountered Turing machines before. (Students who have not may want to lookMore information
Introduction to computer science
Introduction to computer science Michael A. Nielsen University of Queensland Goals: 1. Introduce the notion of the computational complexity of a problem, and define the major computational complexity classes.More information
11 Ideals. 11.1 Revisiting Z
11 Ideals The presentation here is somewhat different than the text. In particular, the sections do not match up. We have seen issues with the failure of unique factorization already, e.g., Z[ 5] = O Q(More information
This asserts two sets are equal iff they have the same elements, that is, a set is determined by its elements.
3. Axioms of Set theory Before presenting the axioms of set theory, we first make a few basic comments about the relevant first order logic. We will give a somewhat more detailed discussion later, butMore information
In mathematics you don t understand things. You just get used to them. (Attributed to John von Neumann)
Chapter 1 Sets and Functions We understand a set to be any collection M of certain distinct objects of our thought or intuition (called the elements of M) into a whole. (Georg Cantor, 1895) In mathematicsMore information
THE TURING DEGREES AND THEIR LACK OF LINEAR ORDER JASPER DEANTONIO Abstract. This paper is a study of the Turing Degrees, which are levels of incomputability naturally arising from sets of natural numbers.More information
Mathematics Course 111: Algebra I Part IV: Vector Spaces
Mathematics Course 111: Algebra I Part IV: Vector Spaces D. R. Wilkins Academic Year 1996-7 9 Vector Spaces A vector space over some field K is an algebraic structure consisting of a set V on which areMore information
Catalan Numbers. Thomas A. Dowling, Department of Mathematics, Ohio State Uni- versity.
7 Catalan Numbers Thomas A. Dowling, Department of Mathematics, Ohio State Uni- Author: versity. Prerequisites: The prerequisites for this chapter are recursive definitions, basic counting principles,More information
13 Infinite Sets. 13.1 Injections, Surjections, and Bijections. mcs-ftl 2010/9/8 0:40 page 379 #385
mcs-ftl 2010/9/8 0:40 page 379 #385 13 Infinite Sets So you might be wondering how much is there to say about an infinite set other than, well, it has an infinite number of elements. Of course, an infiniteMore information
MA651 Topology. Lecture 6. Separation Axioms.
MA651 Topology. Lecture 6. Separation Axioms. This text is based on the following books: Fundamental concepts of topology by Peter O Neil Elements of Mathematics: General Topology by Nicolas Bourbaki CounterexamplesMore information
We give a basic overview of the mathematical background required for this course.
1 Background We give a basic overview of the mathematical background required for this course. 1.1 Set Theory We introduce some concepts from naive set theory (as opposed to axiomatic set theory). TheMore information
The Classes P and NP
The Classes P and NP We now shift gears slightly and restrict our attention to the examination of two families of problems which are very important to computer scientists. These families constitute theMore information
o-minimality and Uniformity in n 1 Graphs
o-minimality and Uniformity in n 1 Graphs Reid Dale July 10, 2013 Contents 1 Introduction 2 2 Languages and Structures 2 3 Definability and Tame Geometry 4 4 Applications to n 1 Graphs 6 5 Further DirectionsMore information
Correspondence analysis for strong three-valued logic
Correspondence analysis for strong three-valued logic A. Tamminga abstract. I apply Kooi and Tamminga s (2012) idea of correspondence analysis for many-valued logics to strong three-valued logic (K 3 ).More information
3. Equivalence Relations. Discussion
3. EQUIVALENCE RELATIONS 33 3. Equivalence Relations 3.1. Definition of an Equivalence Relations. Definition 3.1.1. A relation R on a set A is an equivalence relation if and only if R is reflexive, symmetric,More information
CHAPTER 3. Methods of Proofs. 1. Logical Arguments and Formal Proofs
CHAPTER 3 Methods of Proofs 1. Logical Arguments and Formal Proofs 1.1. Basic Terminology. An axiom is a statement that is given to be true. A rule of inference is a logical rule that is used to deduceMore information
CHAPTER II THE LIMIT OF A SEQUENCE OF NUMBERS DEFINITION OF THE NUMBER e.
CHAPTER II THE LIMIT OF A SEQUENCE OF NUMBERS DEFINITION OF THE NUMBER e. This chapter contains the beginnings of the most important, and probably the most subtle, notion in mathematical analysis, i.e.,More information
Cartesian Products and Relations
Cartesian Products and Relations Definition (Cartesian product) If A and B are sets, the Cartesian product of A and B is the set A B = {(a, b) :(a A) and (b B)}. The following points are worth specialMore information
1.1 Logical Form and Logical Equivalence 1
Contents Chapter I The Logic of Compound Statements 1.1 Logical Form and Logical Equivalence 1 Identifying logical form; Statements; Logical connectives: not, and, and or; Translation to and from symbolicMore information
Mathematical Induction
Mathematical Induction (Handout March 8, 01) The Principle of Mathematical Induction provides a means to prove infinitely many statements all at once The principle is logical rather than strictly mathematical,More information
Revised Version of Chapter 23. We learned long ago how to solve linear congruences. ax c (mod m)
Chapter 23 Squares Modulo p Revised Version of Chapter 23 We learned long ago how to solve linear congruences ax c (mod m) (see Chapter 8). It s now time to take the plunge and move on to quadratic equations.More information
PART I. THE REAL NUMBERS This material assumes that you are already familiar with the real number system and the representation of the real numbers as points on the real line. I.1. THE NATURAL NUMBERSMore information
OPERATIONAL TYPE THEORY by Adam Petcher Prepared under the direction of Professor Aaron Stump A thesis presented to the School of Engineering of
WASHINGTON NIVERSITY SCHOOL OF ENGINEERING AND APPLIED SCIENCE DEPARTMENT OF COMPTER SCIENCE AND ENGINEERING DECIDING JOINABILITY MODLO GROND EQATIONS IN OPERATIONAL TYPE THEORY by Adam Petcher PreparedMore information
Partitioning edge-coloured complete graphs into monochromatic cycles and paths
arxiv:1205.5492v1 [math.co] 24 May 2012 Partitioning edge-coloured complete graphs into monochromatic cycles and paths Alexey Pokrovskiy Departement of Mathematics, London School of Economics and PoliticalMore information
Functional Programming. Functional Programming Languages. Chapter 14. Introduction
Functional Programming Languages Chapter 14 Introduction Functional programming paradigm History Features and concepts Examples: Lisp ML 1 2 Functional Programming Functional Programming Languages TheMore information
INCIDENCE-BETWEENNESS GEOMETRY MATH 410, CSUSM. SPRING 2008. PROFESSOR AITKEN This document covers the geometry that can be developed with just the axioms related to incidence and betweenness. The fullMore information
Dedekind s forgotten axiom and why we should teach it (and why we shouldn t teach mathematical induction in our calculus classes)
Dedekind s forgotten axiom and why we should teach it (and why we shouldn t teach mathematical induction in our calculus classes) by Jim Propp (UMass Lowell) March 14, 2010 1 / 29 Completeness Three commonMore information
C H A P T E R Regular Expressions regular expression
7 CHAPTER Regular Expressions Most programmers and other power-users of computer systems have used tools that match text patterns. You may have used a Web search engine with a pattern like travel cancunMore information
Some Polynomial Theorems. John Kennedy Mathematics Department Santa Monica College 1900 Pico Blvd. Santa Monica, CA 90405 email@example.com.
Some Polynomial Theorems by John Kennedy Mathematics Department Santa Monica College 1900 Pico Blvd. Santa Monica, CA 90405 firstname.lastname@example.com This paper contains a collection of 31 theorems, lemmas,More information
Formal Languages and Automata Theory - Regular Expressions and Finite Automata -
Formal Languages and Automata Theory - Regular Expressions and Finite Automata - Samarjit Chakraborty Computer Engineering and Networks Laboratory Swiss Federal Institute of Technology (ETH) Zürich MarchMore information
4. CLASSES OF RINGS 4.1. Classes of Rings class operator A-closed Example 1: product Example 2:
4. CLASSES OF RINGS 4.1. Classes of Rings Normally we associate, with any property, a set of objects that satisfy that property. But problems can arise when we allow sets to be elements of larger setsMore information
Simulation-Based Security with Inexhaustible Interactive Turing Machines
Simulation-Based Security with Inexhaustible Interactive Turing Machines Ralf Küsters Institut für Informatik Christian-Albrechts-Universität zu Kiel 24098 Kiel, Germany firstname.lastname@example.com information
Taylor Polynomials and Taylor Series Math 126
Taylor Polynomials and Taylor Series Math 26 In many problems in science and engineering we have a function f(x) which is too complicated to answer the questions we d like to ask. In this chapter, we willMore information
Tree-representation of set families and applications to combinatorial decompositions
Tree-representation of set families and applications to combinatorial decompositions Binh-Minh Bui-Xuan a, Michel Habib b Michaël Rao c a Department of Informatics, University of Bergen, Norway. email@example.com information
Notes on Factoring. MA 206 Kurt Bryan
The General Approach Notes on Factoring MA 26 Kurt Bryan Suppose I hand you n, a 2 digit integer and tell you that n is composite, with smallest prime factor around 5 digits. Finding a nontrivial factorMore information
The Foundations: Logic and Proofs. Chapter 1, Part III: Proofs
The Foundations: Logic and Proofs Chapter 1, Part III: Proofs Rules of Inference Section 1.6 Section Summary Valid Arguments Inference Rules for Propositional Logic Using Rules of Inference to Build ArgumentsMore information
A Propositional Dynamic Logic for CCS Programs
A Propositional Dynamic Logic for CCS Programs Mario R. F. Benevides and L. Menasché Schechter {mario,firstname.lastname@example.com Abstract This work presents a Propositional Dynamic Logic in which the programs areMore information
1 if 1 x 0 1 if 0 x 1
Chapter 3 Continuity In this chapter we begin by defining the fundamental notion of continuity for real valued functions of a single real variable. When trying to decide whether a given function is orMore information
x if x 0, x if x < 0.
Chapter 3 Sequences In this chapter, we discuss sequences. We say what it means for a sequence to converge, and define the limit of a convergent sequence. We begin with some preliminary results about theMore information
Foundations of Logic and Mathematics
Yves Nievergelt Foundations of Logic and Mathematics Applications to Computer Science and Cryptography Birkhäuser Boston Basel Berlin Contents Preface Outline xiii xv A Theory 1 0 Boolean Algebraic LogicMore information
Discrete Mathematics and Probability Theory Fall 2009 Satish Rao, David Tse Note 2
CS 70 Discrete Mathematics and Probability Theory Fall 2009 Satish Rao, David Tse Note 2 Proofs Intuitively, the concept of proof should already be familiar We all like to assert things, and few of usMore information
Chapter 7. Functions and onto. 7.1 Functions
Chapter 7 Functions and onto This chapter covers functions, including function composition and what it means for a function to be onto. In the process, we ll see what happens when two dissimilar quantifiersMore information
CONTINUED FRACTIONS AND FACTORING. Niels Lauritzen
CONTINUED FRACTIONS AND FACTORING Niels Lauritzen ii NIELS LAURITZEN DEPARTMENT OF MATHEMATICAL SCIENCES UNIVERSITY OF AARHUS, DENMARK EMAIL: firstname.lastname@example.com URL: http://home.imf.au.dk/niels/ ContentsMore information
1 Sets and Set Notation.
LINEAR ALGEBRA MATH 27.6 SPRING 23 (COHEN) LECTURE NOTES Sets and Set Notation. Definition (Naive Definition of a Set). A set is any collection of objects, called the elements of that set. We will mostMore information
An Innocent Investigation
An Innocent Investigation D. Joyce, Clark University January 2006 The beginning. Have you ever wondered why every number is either even or odd? I don t mean to ask if you ever wondered whether every numberMore information
6.3 Conditional Probability and Independence
222 CHAPTER 6. PROBABILITY 6.3 Conditional Probability and Independence Conditional Probability Two cubical dice each have a triangle painted on one side, a circle painted on two sides and a square paintedMore information
Regular Languages and Finite Automata
Regular Languages and Finite Automata 1 Introduction Hing Leung Department of Computer Science New Mexico State University Sep 16, 2010 In 1943, McCulloch and Pitts [4] published a pioneering work on aMore information
Chapter 3. Cartesian Products and Relations. 3.1 Cartesian Products
Chapter 3 Cartesian Products and Relations The material in this chapter is the first real encounter with abstraction. Relations are very general thing they are a special type of subset. After introducingMore information
So let us begin our quest to find the holy grail of real analysis.
1 Section 5.2 The Complete Ordered Field: Purpose of Section We present an axiomatic description of the real numbers as a complete ordered field. The axioms which describe the arithmetic of the real numbersMore information
Quotient Rings and Field Extensions
Chapter 5 Quotient Rings and Field Extensions In this chapter we describe a method for producing field extension of a given field. If F is a field, then a field extension is a field K that contains F.More information
PUTNAM TRAINING POLYNOMIALS. Exercises 1. Find a polynomial with integral coefficients whose zeros include 2 + 5.
PUTNAM TRAINING POLYNOMIALS (Last updated: November 17, 2015) Remark. This is a list of exercises on polynomials. Miguel A. Lerma Exercises 1. Find a polynomial with integral coefficients whose zeros includeMore information
Rigorous Software Development CSCI-GA 3033-009
Rigorous Software Development CSCI-GA 3033-009 Instructor: Thomas Wies Spring 2013 Lecture 11 Semantics of Programming Languages Denotational Semantics Meaning of a program is defined as the mathematicalMore information
Factoring & Primality
Factoring & Primality Lecturer: Dimitris Papadopoulos In this lecture we will discuss the problem of integer factorization and primality testing, two problems that have been the focus of a great amountMore information
CS510 Software Engineering
CS510 Software Engineering Propositional Logic Asst. Prof. Mathias Payer Department of Computer Science Purdue University TA: Scott A. Carr Slides inspired by Xiangyu Zhang http://nebelwelt.net/teaching/15-cs510-seMore information
CHAPTER 2 American mathematician Paul Halmos (1916 2006), who in 1942 published the first modern linear algebra book. The title of Halmos s book was the same as the title of this chapter. Finite-DimensionalMore information
Introduction to Type Theory
Introduction to Type Theory Herman Geuvers Radboud University Nijmegen, The Netherlands Technical University Eindhoven, The Netherlands 1 Overview These notes comprise the lecture Introduction to TypeMore information
INTERPOLATION. Interpolation is a process of finding a formula (often a polynomial) whose graph will pass through a given set of points (x, y).
INTERPOLATION Interpolation is a process of finding a formula (often a polynomial) whose graph will pass through a given set of points (x, y). As an example, consider defining and x 0 =0, x 1 = π 4, xMore information
THE SEARCH FOR NATURAL DEFINABILITY IN THE TURING DEGREES ANDREW E.M. LEWIS 1. Introduction This will be a course on the Turing degrees. We shall assume very little background knowledge: familiarity withMore information
3(vi) B. Answer: False. 3(vii) B. Answer: True
Mathematics 0N1 Solutions 1 1. Write the following sets in list form. 1(i) The set of letters in the word banana. {a, b, n}. 1(ii) {x : x 2 + 3x 10 = 0}. 3(iv) C A. True 3(v) B = {e, e, f, c}. True 3(vi)More information
Continued Fractions and the Euclidean Algorithm
Continued Fractions and the Euclidean Algorithm Lecture notes prepared for MATH 326, Spring 997 Department of Mathematics and Statistics University at Albany William F Hammond Table of Contents IntroductionMore information
Understanding Basic Calculus
Understanding Basic Calculus S.K. Chung Dedicated to all the people who have helped me in my life. i Preface This book is a revised and expanded version of the lecture notes for Basic Calculus and otherMore information
Mathematics for Computer Science
Mathematics for Computer Science Lecture 2: Functions and equinumerous sets Areces, Blackburn and Figueira TALARIS team INRIA Nancy Grand Est Contact: email@example.com Course website: http://www.loria.fr/~blackbur/courses/mathMore information
Prime Numbers and Irreducible Polynomials
Prime Numbers and Irreducible Polynomials M. Ram Murty The similarity between prime numbers and irreducible polynomials has been a dominant theme in the development of number theory and algebraic geometry.More information
Introduction to Algebraic Geometry. Bézout s Theorem and Inflection Points
Introduction to Algebraic Geometry Bézout s Theorem and Inflection Points 1. The resultant. Let K be a field. Then the polynomial ring K[x] is a unique factorisation domain (UFD). Another example of aMore information
S(A) X α for all α Λ. Consequently, S(A) X, by the definition of intersection. Therefore, X is inductive.
MA 274: Exam 2 Study Guide (1) Know the precise definitions of the terms requested for your journal. (2) Review proofs by induction. (3) Be able to prove that something is or isn t an equivalence relation.More information
Linear Algebra I. Ronald van Luijk, 2012
Linear Algebra I Ronald van Luijk, 2012 With many parts from Linear Algebra I by Michael Stoll, 2007 Contents 1. Vector spaces 3 1.1. Examples 3 1.2. Fields 4 1.3. The field of complex numbers. 6 1.4.More information
Predicate Logic Review
Predicate Logic Review UC Berkeley, Philosophy 142, Spring 2016 John MacFarlane 1 Grammar A term is an individual constant or a variable. An individual constant is a lowercase letter from the beginningMore information
ECS 120 Lesson 17 Church s Thesis, The Universal Turing Machine
ECS 120 Lesson 17 Church s Thesis, The Universal Turing Machine Oliver Kreylos Monday, May 7th, 2001 In the last lecture, we looked at the computation of Turing Machines, and also at some variants of TuringMore information
Lecture 17 : Equivalence and Order Relations DRAFT
CS/Math 240: Introduction to Discrete Mathematics 3/31/2011 Lecture 17 : Equivalence and Order Relations Instructor: Dieter van Melkebeek Scribe: Dalibor Zelený DRAFT Last lecture we introduced the notionMore information
Fixed-Point Logics and Computation
1 Fixed-Point Logics and Computation Symposium on the Unusual Effectiveness of Logic in Computer Science University of Cambridge 2 Mathematical Logic Mathematical logic seeks to formalise the process ofMore information
Ultraproducts and Applications I
Ultraproducts and Applications I Brent Cody Virginia Commonwealth University September 2, 2013 Outline Background of the Hyperreals Filters and Ultrafilters Construction of the Hyperreals The TransferMore information


text:
Quantitative trait loci affecting reproductive phenology in peach
Genetics and crop biotechnology
The reproductive phenology of perennial plants in temperate climates is largely conditioned by the duration of bud dormancy, and fruit developmental processes. Bud dormancy release and bud break depends on the perception of cumulative chilling and heat during the bud development. The objective of this work was to identify new quantitative trait loci (QTLs) associated to temperature requirements for bud dormancy release and flowering and to fruit harvest date, in a segregating population of peach.
We have identified QTLs for nine traits related to bud dormancy, flowering and fruit harvest in an intraspecific hybrid population of peach in two locations differing in chilling time accumulation. QTLs were located in a genetic linkage map of peach based on single nucleotide polymorphism (SNP) markers for eight linkage groups (LGs) of the peach genome sequence. QTLs for chilling requirements for dormancy release and blooming clustered in seven different genomic regions that partially coincided with loci identified in previous works. The most significant QTL for chilling requirements mapped to LG1, close to the
We identified QTLs associated to nine traits related to the reproductive phenology in peach. A search of candidate genes for these QTLs rendered different genes related to flowering regulation, chromatin modification and hormone signalling. A better understanding of the genetic factors affecting crop phenology might help scientists and breeders to predict changes in genotype performance in a context of global climate change.
The timing of reproductive events of perennial plants in temperate climates is largely conditioned by dormancy, a period of cyclic quiescence during the low temperatures of autumn and winter, which protects meristems within buds from the detrimental effects of cold and water stress. The pioneering work by Lang
The quantitative perception of environmental chilling is the major and best-known factor favouring the release of bud dormancy
Recently researchers have increased their interest on the effects of global climate warming on plant phenology
Plant species cope with changing climate conditions by shifting their geographical distribution, with a plastic response of plant phenology to environmental changes, or alternatively through the natural selection of populations with dormancy, flowering and fruit maturation traits adapted to the new conditions
The objective of this work was to identify new QTLs and candidate genes associated to chilling and heat requirements in a
Phenotypic assessment and correlation between traits
Traits evaluated in the 'V6' x 'Granada' progeny are listed in Table
Figure 1
Chilling accumulation in AA and EJ locations along the cold season
Chilling accumulation in AA and EJ locations along the cold season. Chilling accumulation in AA (circles) and EJ (triangles) locations, according to Weinberger (white symbols) and Utah (black symbols) models. The discontinuous line is to interpolate the date with a chilling accumulation value of 500 CH/CU.
Variables CRW-AA, CRW-EJ, CRU-EJ, CRD-EJ, HRB-AA, EcD-AA, BD-AA, PEnB-AA and HD-2012-AA departed from normality due to altered standardized skewness or kurtosis of their frequency distribution (Figure
Figure 2
Frequency distribution of traits measured in the 'V6' x 'Granada' progeny
Frequency distribution of traits measured in the 'V6' x 'Granada' progeny. Chilling requirement (CRW, CRU and CRD) and heat requirement (HREc and HRB) variables are represented in A. The values for the 'V6' (V6), 'Granada' (G), 'Red Candem' (RC) and 'Maruja' (M) parents are indicated by arrows. Endodormancy release date (EnD; black bars), ecodormancy release date (EcD; grey bars), and blooming date (BD; white bars) are represented in B. The arrows indicating date values of parents are black for EnD, grey for EcD and white for BD. The panel C includes the endodormancy-ecodormancy (PEnEc) and endodormancy-blooming (PEnB) time periods. Harvest date (HD) trait is represented in panel D.
The parental cultivars of 'V6' selection, 'Maruja' and 'Red Candem', had the highest and lowest range values of chilling requirement distributions (CRW, CRU and CRD) and date variables (EnD, EcD, BD and HD) respectively. 'Maruja' and 'Red Candem' data were not available for variables HD-2011-EJ and HD-2012-AA. However traits related to heat/time requirements for ecodormancy release and blooming (HREc, HRB, PEnEc and PEnB) showed a more variable location of parental genotypes within the range, and numerous transgressive segregants exceeded the parent values (Figure
The Pearson correlation coefficients between variables are shown in Table
Map construction
Genotyping was performed using the International Peach SNP Consortium (IPSC) peach 9 K Infinium® II array
QTL analysis of chilling requirement and flowering time
The analysis of co-segregation between SNPs and phenotypic data led to the identification of QTLs for all the investigated traits. For every variable, the LOD threshold for
Figure 3
Location of quantitative trait loci (QTLs) in the 'V6' x 'Granada' genetic map
Location of quantitative trait loci (QTLs) in the 'V6' x 'Granada' genetic map. QTLs are labelled by boxes (two-LOD confidence interval). Boxes are black for chilling requirement and blooming variables (CRW, CRU, CRD, EnD, EcD and BD), white for heat requirement variables (HREc, HRB, PEnEc and PEnB) and grey for harvest date (HD). 'V6' and 'Granada' genetic maps are vertical white bars showing single nucleotide polymorphisms (SNP) markers. Genome scaffolds are represented as vertical black bars placed between their respective 'V6' and 'Granada' maps. The positions of SNP markers flanking the confidence intervals of QTLs are labelled in bold on genome scaffolds, limiting a genomic region named with a number (for the scaffold) and a letter (for the order of the region along the scaffold), which was used to identify putative candidate genes. Within each genomic region, QTLs of the same variable corresponding to different locations are fused in a single box. Scale bars for genetic maps and scaffolds are shown in the upper left part of the figure.
Another cluster of QTLs was identified in the LG7 of 'Granada' map. The LOD plots showed two close linked peaks, suggesting the possibility that two linked QTLs were present in this genomic region (Table
QTL analysis of heat requirement and ecodormancy release
Traits describing processes following endodormancy release were HREc and HRB, which use the Anderson model to estimate the heat requirements for ecodormancy release and blooming respectively. Two additional traits, PEnEc and PEnB, estimate the time in days required for the fulfilment of HREc and HRB values respectively, starting from the endodormancy release date. A QTL cluster for HREc and PEnB traits with consistent major effects in both locations (R2 = 15-39%) was detected in LG1 of 'V6' map, overlapping with QTLs for chilling requirement and flowering time described above. Additional QTLs with minor effects but not consistent across locations were also detected in LG3, LG4, LG5, LG6 and LG7 (Table
QTL analysis of fruit harvest date
QTLs for HD were detected in four genomic regions of LG1, LG4, LG6 and LG7 of the 'V6' map (Table
Search of candidate genes
QTL regions 1b, 3a, 4b, 6a, 6b and 7b, containing multiple QTLs and QTLs with high significance, relevance and consistent effects among trials were searched for the presence of plausible candidate genes. The QTL regions limited by the genome coordinates shown in Additional file
Additional file 1
Name and genomic position of SNPs flanking the QTL regions.
Click here for file
An alternative approach for the identification of candidate genes has been performed by reciprocal blast analysis of known genes involved in chromatin modification and flowering. Reciprocal blast analysis allowed the identification of putative orthologs of these genes in peach located within the genomic regions outlined by QTL analysis. Peach putative orthologs of genes coding for subunits of the Polycomb Repressive Complex 1 and 2 (PRC1, PRC2), Trithorax group proteins
In this work we have studied nine traits related to bud dormancy, flowering and fruit harvest in a hybrid population of peach. The high level of correlation between traits and the clustering of QTLs in certain map positions argue for a considerable degree of redundancy that recommends the joint analysis of traits in three major groups. Chilling requirement (CRW, CRU and CRD), dormancy release (EnD and EcD), and blooming date (BD) variables constitute a first group with high correlation values and similar QTLs. Additionally, the fact that a significant QTL for fruit harvest date also co-localizes with the major QTL for chilling requirement in LG1 indicates that chilling requirement is a primary determinant of the reproductive phenology in peach. Heat requirement HREc and HRB, and PEnEc and PEnB form a second group of traits with common features. Finally, HD trait deserves a separate discussion due to the particular contribution of fruit developmental programs to this trait, in spite of its significant correlation with chilling requirement trait.
Candidate genes for chilling requirement, dormancy release and blooming time
QTLs for this first group of traits clustered in seven different map zones that corresponded to seven genomic regions defined by SNPs (1b, 3a, 3b, 4a, 6b, 6c and 7b). Some of these regions were identified in previous QTL works in
The availability of the peach genome sequence
Recent studies in apricot, peach and almond proposed
Other candidates to be the major determinant of bud phenology located in genomic region 1b are listed in Table
Other candidate genes in region 1b are putative components of the ABA signalling pathway, such as ppa003748m coding for a protein phosphatase 2C (PP2C) similar to HYPERSENSITIVE TO ABA1 (HAB1), and ppa006503m and ppa024363m coding for proteins similar to ABA-RESPONSIVE ELEMENT BINDING PROTEIN 1 (AREB1) and AREB3
In region 1b we have also identified putative flowering-related genes, such as ppa013757m similar to
Genomic regions 3a, 6b and 7b were also considered important for the chilling requirement trait. Among the candidate genes present in these regions, we found other chromatin-related factors, such as ppa001213m, the peach ortholog of
Further histone acetyltransferases and deacetylases are localized in regions 3a, 6b and 7b. Among them, ppa009583m and ppa009356m show similarity to
Candidate genes for heat requirement
In contrast to the well-established genetic component of chilling requirements and the close relationship between flowering time and chilling requirements described so far, the genetic control of heat requirements in
We found 13 significant QTLs for HREc, HRB, PEnEc and PEnB, located in nine different genomic regions (Table
In addition to candidate genes proposed for genomic regions containing chilling requirement QTLs, commented in the previous section, a reciprocal blast analysis for the search of peach genes orthologous to chromatin and flowering genes from
Candidate genes for fruit harvest date
The analysis of the harvest date trait resulted in a major QTL in region 4b showing numerous precedents in related works in peach and apricot
On the same region 4b, the gene ppa022739m codes for a putative transcription factor containing the Squamosa-Promoter Binding Protein (SBP) domain, present in the tomato fruit ripening factor COLORLESS NON-RIPENING (CNR)
However, recent fine mapping of a locus controlling maturity date in two segregating populations of peach limited the search to a 220 kb stretch within region 4b. The maturity date locus co-segregated with an indel into the gene ppa008301m coding for a NAC type transcription factor, which points to this gene as a firm candidate for controlling ripening time in peach
In region 6a we should emphasize the presence of ppa003113m gene, with similarity to
This work was aimed at the identification of genetic factors conditioning the phenological behaviour of peach. We have identified QTLs for nine traits related to bud dormancy, flowering and fruit harvest in a hybrid population of peach in two different locations. QTLs were located in a SNP-based genetic linkage map. A search of candidate genes for these QTLs rendered different genes related to flowering regulation, chromatin modification and hormone signalling. Additional studies including the characterization of proposed candidate genes in germplasm collections and functional approaches are required to identify the genes involved in dormancy, blooming and fruit maturation among these lists of candidate genes. The characterization of natural alleles of these genes might offer molecular tools to predict the potential performance of different
Plant material
The plant material used in the study was a progeny of 107 individuals derived from a cross carried out during 2008 between the F1 selection 'V6' (named MxR_01 in
Phenotypic assessment
Chilling requirements, heat requirements and blooming dates were evaluated in the winter and spring of 2012; fruit harvest dates were measured in the spring of 2011 and 2012. To assess chilling requirements for endodormancy release, nine one-year old shoots per genotype with a length of 20-25 cm were picked weekly. Groups of three shoots were placed in bottles containing distilled water with 3% sucrose, and incubated in a growth chamber subject to 12 h photoperiod at 22°C. The basal end of shoots was cut and the water renewed once per week. We considered that endodormancy was completed when the percentage of buds that reached the green stage (stage C) according to the Baggiolini code
To evaluate ecodormancy release and blooming time, the main phenological stages
Heat requirements were calculated as the growing degree hours (GDH) accumulated from the release of endodormancy to the ecodormancy release and blooming dates following the Anderson model
Statistical analyses
Statistical analyses were performed using the Statgraphics 5.1 package (Statpoint Technologies, Warrenton, VA, USA). All correlations between traits were calculated using the Pearson coefficient. Correlations between traits in the EJ and AA locations employed exclusively those genotypes present in both locations. Departure from the normal distribution of traits was assessed by the calculation of skewness and kurtosis of frequency distributions.
SNP genotyping and map construction
DNA from the parentals and progeny were extracted from 50 mg of leaf tissue following the method of Doyle & Doyle
QTL analysis
In order to facilitate computer analysis, the genetic linkage was condensed, eliminating SNPs that mapped in the same position or very close (i.e. less than 2 cM). The maps from each parent were analyzed independently and coded as two independent backcross populations. QTL analysis was performed with WinQTLcartographer 2.5
Candidate gene selection
By using the BioMart tool in the phytozome web-page
Additional file 2
Annotation of genes within the QTL regions.
Click here for file
In order to identify putative orthologs in peach of
Competing interests
The authors declare that they have no competing interests.
Authors' contributions
JFR carried out the genetic studies and helped to draft the manuscript. AJM carried out the linkage map construction and QTL analysis. GS participated in the linkage map construction and QTL analysis. AG participated in the design and coordination of the study. JGB participated in the design and coordination of the study. MLB conceived the study, and participated in its design and coordination. GR carried out the candidate gene search and drafted the manuscript. All authors read and approved the final manuscript.
We thank Matilde González for technical assistance. This work was supported by the Instituto Nacional de Investigación y Tecnología Agraria y Alimentaria (INIA)-FEDER (grant no. RTA2007-00060), and the Ministry of Science and Innovation of Spain (grant no. AGL2010-20595).
Dormancy: a new universal terminology
Plant dormancy in the perennial context
The dynamic nature of bud dormancy in trees: environmental control and molecular mechanisms
The influence of cold in stimulating the growth of plants
Why does phenology drive species distribution?
Tree seasonality in a warming climate
Winter and spring warming result in delayed spring phenology on the Tibetan Plateau
Plant phenotypic plasticity in a changing climate
Quantitative trait loci and candidate gene mapping of bud set and bud flush in
Bud set in poplar - genetic dissection of a complex trait in natural and hybrid populations
Phenotypic plasticity, QTL mapping and genomic characterization of bud set in black poplar
Deciphering the genetic determinism of bud phenology in apple progenies: a new insight into chilling and heat requirement effects on flowering dates and positional candidate genes
Mapping QTL controlling fruit quality in peach (
Genetic mapping of a major gene delaying blooming time in almond
QTL analysis of agronomic traits in a BC1 peach population
QTL analysis of quality traits in an advanced backcross between
Mapping major genes and quantitative trait loci controlling agronomic traits in almond
Inheritance of flowering time in apricot (
QTL analysis of fruit quality traits in two peach intraspecific populations and importance of maturity date pleiotropic effect
Comparison of the genetic determinism of two key phenological traits, flowering and maturity dates, in three
Mapping architectural, phenological, and fruit quality QTLs in apricot
Genetic linkage mapping for molecular dissection of chilling requirement and budbreak in apricot (
Mapping quantitative trait loci associated with chilling requirement, heat requirement and bloom date in peach (
Inheritance of chilling and heat requirements for flowering in almond and QTL analysis
Sequencing and annotation of the
Identification of genes associated with growth cessation and bud dormancy entrance using a dormancy-incapable tree mutant
Development and evaluation of a 9 K SNP array for peach by internationally coordinated SNP detection and validation in breeding germplasm
PhD Thesis
Identification of genes associated with bud dormancy release in
Histone modifications and expression of
Gene expression analysis of chilling requirements for flower bud break in peach
Polycomb group complexes mediate developmental transitions in plants
Analysis of histone acetyltransferase and histone deacetylase families of
The high-quality draft genome of peach (
Phylogenetic analysis and molecular evolution of the dormancy associated MADS-box genes from peach
Dormancy-associated MADS genes from the EVG locus of peach (
Expression analysis of
Gene expression of
Expressional regulation of
Chilling-dependent release of seed and bud dormancy in peach associates to common changes in gene expression
Characterization, expression and function of
Functional and expressional analyses of
Common mechanisms regulate flowering and dormancy
Make hay when the sun shines: the role of MADS-box genes in temperature-dependent seasonal flowering responses
Chromatin regulation of flowering
Acetylated H4 histone and genomic DNA methylation patterns during bud set and bud burst in
Transcriptome analysis of chestnut (
Abscisic acid: emergence of a core signaling network
Modulation of drought resistance by the abscisic acid receptor PYL5 through inhibition of clade A PP2Cs
Induction and release of bud dormancy in woody perennials: a science comes of age
Knowing when to grow: signals regulating bud dormancy
A molecular timetable for apical bud formation and dormancy induction in poplar
Silencing by plant Polycomb-group genes requires dispersed trimethylation of histone H3 at lysine 27
PhD Thesis
PhD Thesis
Identification of
Influence of prolonged exposure to chilling temperatures on bud break and heat requirement for bloom of several fruit species
Chilling and heat requirements of apricot cultivars for flowering
The Plant Homeo Domain finger protein, VIN3-LIKE 2, is necessary for photoperiod-mediated epigenetic regulation of the floral repressor, MAF5
HISTONE DEACETYLASE6 interacts with FLOWERING LOCUS D and regulates flowering in
A microarray approach to identify genes involved in seed-pericarp cross-talk and development in peach
MdERFs, two ethylene-response factors involved in apple fruit ripening
A naturally occurring epigenetic mutation in a gene encoding an SBP-box transcription factor inhibits tomato fruit ripening
Fine mapping and identification of a candidate gene for a major locus controlling maturity date in peach
Genetics and epigenetics of fruit development and ripening
A non-targeted approach unravels the volatile network in peach fruit
Stades reperes de la Abricotier- Stades Reperes de la Pecher. Stades Reperes du Ceresier - Stades reperes du Prunier
Chilling requirements of peach varieties
A model for estimating the completition of rest for "Redheaven" and "Elberta" peach
The temperature dependence of dormancy breaking in plants - mathematical-analysis of a 2- step model involving a cooperative transition
The temperature dependence of dormancy breaking in plants - computer-simulation of processes studied under controlled temperatures
SIAM station
Validation of chill unit and flower bud phenology models for "Montmorency" sour cherry
A rapid isolation procedure for small quantities of fresh leaf tissue
Genetic-linkage maps of
Construction of integrated genetic-linkage maps by means of a new computer package—Joinmap
MAPMAKER: an interactive computer package for constructing primary genetic linkage maps of experimental and natural populations
MapChart: software for the graphical presentation of linkage maps and QTLs
Windows QTL cartographer 2.5
Empirical threshold values for quantitative trait mapping

subset: commoncrawl


text:
Shop Leather
Shop Baer's Best
Shop New Arrivals
Entertain Guests In Style
Beach House Furniture
Pan Asian Furniture
Sleep Health & Habits
Adjustable Base Buying Guide
Mattress Size Guide
How To Shop For A Mattress
Shop Tommy Bahama
Insider Tips For Outdoor Living
Outdoor Chaise Lounges
As the hallmarks of fine bourbon and whiskey are dependent on select ingredients and aging, the Whiskey Oak collection relies on the finest knotty white oak veneers and radiata solids, along with Barrel Oak and Weathered Black color finishes, to create a sense of timeworn comfort. Distinct design characteristics abound, the bed collection features three-unique rustic traits which include deep-cut molding frame-and-panel, beautifully tailored button-tufted leather upholstery, and random-planked sleigh design, all thoughtfully updated for today's home. Further enhancing Whiskey Oak's rustic charm are other diverse styles which feature rare slat-back paneled chairs with removable cushions, impressive trestle and pedestal table bases, and subtle "pillowed" drawer-front dressers. Honed marble, hand-hammered copper, graphic nail-head décor, and finely tailored raw linen or top-grain leather upholstery are the perfect finishing touch for this robust collection.
Browse other items in the Kennedy Walnut collection from Baer's Furniture in the Ft. Lauderdale, Ft. Myers, Orlando, Naples, Miami, Florida area.
Nothing on this page may be copied or reproduced without explicit permission.


text:
Im so lookin forward to havin a ported siri on my verizon iPhone 4 i just hope they fully ported and fully workin very soon it would be fun to have siri and a very useful app, plz dev team bring it out quickly
Unfortunately, it will not be supported on the original iPhone 4, at least in the beta stage. The following footnote is on the Siri information page at apple.com:
Siri is available in Beta only on iPhone 4S and requires Internet access. But we can still hope the development team works on this pretty soon.
iPhone 3G, iPhone 4, iPad2, Travel International Motorola (At&t,T-Mobile and SmartFree Quattro SIM) iSip from InTouch SmartCards


text:
Protect your business name or app by Trademarking it
Registering a 'Pty Ltd' company or business name with ASIC does not stop other people from using it. You need to register your business name, brand or logo as a Trademark with IP Australia to make sure it belongs to you and can't be used by anyone else.
Note: Use the ™ symbol when you plan to Trademark your brand. Use the ® symbol when your Trademark is registered.
Our Trademarking experience makes it easy for you
Registering a Trademark with IP Australia is not straightforward. If you're trying to do it yourself, you may make mistakes and it is time consuming. Here at Legal123, we have years of experience in registering Trademarks. So save yourself the trouble and let us take care of this for you.
Your protection starts as soon as your application is lodged
In total, the whole Trademarking process can take 6+ months. However, the initial searches will give you a good idea of your Trademark application success – and your business name protection starts as soon as your application is lodged and acknowledged by IP Australia. The approximate timings for getting through the process are shown here.
And don't forget there are government fees too
The Legal123 fee is for carrying out your Trademark searches, advising on Trademark classes, filing your Trademark application and following up with IP Australia. In addition to our fees, the new IP Australia charge is:
- $250 application fee per Class (the additional $300 final registration fee per Class approved has been removed)
Note: Goods and services are divided in 45 Classes (e.g. clothing & footwear or training & education). Generally, most Trademark applications are for 1-2 Classes.
Is the Trademark registration service right for me?
That is not enough to protect your business name, logo or tagline. Someone can Trademark your business name and prevent you from using it to sell similar goods and services. So register your Trademark!
I want to sell my business …
This is one of the best reasons to Trademark your business name and logo. An acquirer will look to see that your business is fully protected and a Trademark is a valuable business asset.
Then Trademarking your brand is essential! This is the best way to gain the right to license use of your business name, brand, logo and tagline to another person or business.
I want to Trademark my brand overseas …
If you're doing business in Australia, you must register your Trademark here first. After that, each country has their own individual registration fees, that vary widely. Contact us for more information.
The service includes
- Trademark Searches – We check the business name, plus variations, on the IP Australia, ASIC and website domain name databases.
- Advice on Application – We suggest the Classes for registration of your business name, logo or tagline. We also advise you if we believe there may be any problems with your Trademark registration. We usually have a telephone conversation with you to discuss our advice and answer any questions you may have.
- Lodge Trademark Application – We complete and lodge your Trademark application with IP Australia.
- Amendments to Application – If IP Australia rejects your Trademark application, we will liaise with IP Australia and advise you of any changes required.
- Objections to Application – If, when your Trademark is advertised, you receive any formal objections from other businesses, we will liaise with IP Australia and advise you of any changes required. If a formal defence is required, this may incur additional fees.
- Registered Trademark – We will notify you as soon as your Trademark is formally registered.
We offer a full money back guarantee if our templates are not suitable for your circumstances or a technical difficulty prevents you from using them. If you have questions about buying online, check out the FAQs.


text:
It's a classic tale, the girls who want to make it big as a singing group and the forces that come to bear upon their relationships as fame takes its toll. What sets this film apart is the quality music from Whitney Houston, Jordin Sparks and Ceelo Green.
Expect sleazy managers, tiny dresses and a whole lotta lungs in this chart-topping show business blockbuster.
Jordin Sparks as Sparkle
Whitney Houston as Emma
Derek Luke as Stix
Mike Epps as Satin
Carmen Ejogo as Sister
Tika Sumpter as Dolores
Omari Hardwick as Levi
CeeLo Green as Black


text:
May He Poop? (an Indian music video translation) MP3
My translation of an Indian music video. This is what I think the words sound like. www.bugben.com.
"Genitalia" starring the Indian Tony Danza (very funny Indian music translation) MP3
I phonetically subtitled this video. This song pops into my head a lot as if these are the real lyrics. I never want to know what they are really saying.
Indian Nipple Song MP3
An Indian song "translated" into English. (Dilbar Dilbar by Susmita Sen). Thanks to Susmita for making the song :)
Funny indian music video - With English Subtitles! (Not actual translation) MP3
My first Indian music video to be Jenaissanced! Khuda Jaane INSPIRED BY THE ONE AND ONLY, ORIGINAL BUFFALAX, maker of the insanely popular ...
Really Funny and Crazy Indian Video Translation Spoof MP3
Really Funny Looney and Insanely Crazy Indian Video "Translation"!!! This is just a spoof! Not a real translation! Funny as hell!
Crazy Indian Music Video - Kalluri Vaanil: Lyrics & Translation MP3
If you want detailed information about the song, the translation, the spelling or something else, check out the video of mmanoba: The song is called "Kalluri ...
Crazy Indian Music - Kalluri Vaanil: Lyrics & Translation MP3
Well, on seeing the popularity of "Kalluri Vaanil", I decided to provide the lyrics and a detailed translation for the song. MP3 song download: ...
May He Poop (an Indian music video translation) MP3
The new Cherokee morning song with translation MP3
Thanks for watching! Remember, we can not exist without the sun, so protect the world where you live. You're only a guest on''''mother nature! Dear watchers ...
8 Hour Study Focus Music: Concentration Music, Better Learning, Alpha Waves ☯375 MP3
Body Mind Zone is home to the most effective Relaxing Music. We have music playlists for Meditation Music, Sleep Music, Study Music, Healing & Wellness ...
Rahat Fateh Ali Khan - Zaroori Tha MP3
Music video by Rahat Fateh Ali Khan performing Zaroori Tha. (C) 2014 Universal Music India Pvt. Ltd. iTunes: http://bit.ly/1mv2vT3 Saavn: ...
Mary Jane (an Indian music video translation) MP3
This has been one of my favorite song for years. Freshman year me and a few of my friends came up with the awful English translations. Love ya Emily and ...
Jeene Laga Hoon Bollywood Sing Along - Ramaiya Vastavaiya - Girish Kumar, Shruti Haasan MP3
Jeene Laga Hoon has turned out to be biggest romantic song of all time. Presenting to you full song video with lyrics. Now sing along this magical track. Credits ...
Daler Mehndi - Tunak Tunak Tun Video MP3
Presenting 'Tunak Tunak Tun' music video sung by the talented Daler Mehndi Song Name - Tunak Tunak Tun Album - Tunak Tunak Tun Singer - Daler Mehndi ...
Funny Indian snake dance (an Indian music video translation) May he poop version MP3
may he poop like version.
(Lets see your vagina) Indian music translation MP3
Mashbang karaoke Sing along.. lol.
NSPA: PATANGA | PRATYUL JOSHI - street performer/Indian folk music MP3
Lyrics and its literal translation below Song is in haryanvi Ib k puchhe Ib k jaane ( now what do you ask /want to know ) jindadi re ghaagh se ( life cheated you...
Indian Bollywood Music Video (Phonetic Translation) MP3
Original Title: "Dekhon tujeh to payar aaye" But we all know that to be untrue.
Indian - Do me, Superman (Translation) MP3
Finally trying my own indian music video translation :D Copyright Disclaimer Under Section 107 of the Copyright Act 1976, allowance is made for "fair use" for ...
"Tum Hi Ho" Lyrics & English Translation- "Aashiqui 2" (2013) MP3
I think I should put this out there, Aditya's nose is plain gorgeous. Oye Frooj! It was fun hearing you cry, let's do it again sometime. And Amnom ...
Ambarsariya-Fukrey full song english poetic translation with hindi subtitles MP3
Original Music copyright: T-Series music गली में मारे फेरे पास आने को मेरे (जे2) कभी परखता नैन मेरे तू...
Panjabi MC - Mundian To Bach Ke (The Dictator Soundtrack) MP3
Panjabi MC - Mundian To Bach Ke from the album Beware Translation: (AS YOU ARE GROWING UP PEOPLE ARE BECOMING AWARE OF YOUR GOOD ...
kabira sad- full song English translation with hindi subtitles MP3
Original Music copyright: T-Series music ीसैक तेरी खुदगर्ज़ी ना धूप चुने ना छाओं कैसी तेरी खुदगर्ज़...
Re: May He Poop? (an Indian music video translation) MP3
Video Cam Direct Upload.
Dard Dilo Ke-Xpose 2014 Hindi movie song lyrics with english translation MP3
Song-Dard Dilo Ke Movie-Xpose 2014 Singer-Mohammed Irfan Music label-Tseries.
Eat The Tuna ! (an Indian music video translation - English Subtitles) MP3
My translation of an Indian music video singing. This is what I think the words sound like. Eat The Tuna!
Re: May He Poop? (an Indian music video translation) MP3
Video Cam Direct Upload.
Radha - SOTY | Alia Bhatt | Sidharth Malhotra | Varun Dhawan MP3
'Radha' from 'Student of the Year' is a perky and bubbly number featuring Shreya Ghoshal's charming vocals. The song will urge you to put on your disco heels ...
Saree ke fall se- Rambo Rajkumar English poetic translation with Hindi subtitles MP3
Music copyright: sony music This is a lovely song sung by a guy who is enchanted to a girl wearing an ornamental sari. He addresses his compatibility with the ...