Ipc Teoria Dos Tipos 1

type theory from wikipedia, the free encyclopedia jump to: navigation, search this article is about type theory in computation. for other mathematical constructions, see intuitionistic type theory. at the broadest level, type theory is the branch of mathematics and logic that first creates a hierarchy of types, then assigns each mathematical (and possibly other) entity to a type. objects of a given type are built up from objects of the preceding type. types in this sense are related to the metaphysical notion of 'type'. bertrand russell invented type theory in response to his discovery that naive set theory was afflicted with russell's paradox. type theory features prominently in russell and whitehead's principia mathematica. "...[t]he property of being a perfect square can be significantly predicated of both cardinals and ratios of cardinals; but the property of being odd (or even) is not defined for the ratios. we are thus unable to answer the question whether 2/3 is odd or even." [1] --ernest nagel in programming language theory, a branch of computer science, type theory provides the formal basis for the design, analysis and study of type systems. indeed, many computer scientists use the term type theory to refer to the formal study of type systems for programming languages, although some limit it to the study of more abstract formalisms such as typed ?-calculi. contents [hide] 1 simple theory of types 2 history of type theory 3 practical impact of type theory 4 connections to constructive logic 5 relation to other topics 6 type system 7 see also 8 references 9 further reading 10 external links

[edit] simple theory of types the following system is mendelson's (1997: 289-93) st. the domain of quantification is partitioned into an ascending hierarchy of types, with all individuals assigned a type. quantified variables range over only one type; hence the underlying logic is first order logic. st is "simple" (relative to the type theory of principia mathematica) primarily because all members of the domain and codomain of any relation must be of the same type. there is a lowest type, whose individuals have no members and are members of the second lowest type. individuals of the lowest type correspond to the urelements of certain set theories. each type has a next higher type, analogous to the notion of successor in peano arithmetic. while st is silent as to whether there is a maximal type, a transfinite number of types poses no difficulty. these facts, reminiscent of the peano axioms, make it convenient and conventional to assign a natural number to each type, starting with 0 for the lowest type. but type theory does not require a prior definition of the naturals. the symbols peculiar to st are primed variables and infix ?. in any given formula, unprimed variables all have the same type, while primed variables (x�) range over the next higher type. the atomic formulas of st are of two forms, x=y (identity) and y?x �. the infix symbol ? suggests the intended interpretation, set

membership. all variables appearing in the definition of identity and in the axioms extensionality and comprehension, range over individuals of one of two consecutive types. only unprimed (primed) variables, ranging over the "lower" ("higher") type, can appear to the left (right) of '?'. the first order formulation of st rules out quantifying over types. hence each pair of consecutive types requires its own axiom of extensionality and of comprehension, which is possible if extensionality and comprehension below are taken as axiom schemata "ranging over" types. identity defined: x=y ? ?z� [x?z� ? y?z�]. extensionality: an axiom schema. ?x[x?y� ? x?z�] ? y�=z�. let f(x) denote any first order formula containing the free variable x. comprehension. an axiom schema. ?z�?x[x?z� ? f(x)]. remark: any collection of elements of the same type may form an object of the next higher type. comprehension is schematic with respect to f(x) as well as to types. infinity. there exists a nonempty binary relation r over the individuals of the lowest type, that is irreflexive, transitive, and strongly connected (?x, y [xry ? yrx]). remark. infinity is the only true axiom of st and is entirely mathematical in nature. it asserts that r is a strict total order, with a domain identical to its codomain. if 0 is assigned to the lowest type, the type of r is 3. infinity can be satisfied only if the (co)domain of r is infinite, thus forcing the existence of an infinite set. if relations are defined in terms of ordered pairs, this axiom requires a prior definition of ordered pair; the kuratowski definition, adapted to st, will do. the literature does not explain why the usual axiom of infinity (there exists an inductive set) of zfc of other set theories could not be married to st. st reveals how type theory can be made very similar to axiomatic set theory. moreover, the more elaborate ontology of st, grounded in what is now called the "iterative conception of set," makes for axiom (schemas) that are far simpler than those of conventional set theories, such as zfc, with simpler ontologies. set theories whose point of departure is type theory, but whose axioms, ontology, and terminology differ from the above, include new foundations and scott-potter set theory. [edit] history of type theory this section is a stub. you can help by expanding it. [edit] practical impact of type theory the most obvious application of type theory is in constructing type checking algorithms in semantic analysis phase of compilers for programming languages. type theory is also widely in use in theories of semantics of natural language. the most common construction takes the basic types e and t for individuals and truth-values, respectively, and defines the set of types recursively as follows:

if a and b are types, then so is . nothing except the basic types, and what can be constructed from them by means of the previous clause are types. a complex type is the type of functions from entities of type a to entities of type b. thus one has types like which are interpreted as elements of the set of functions from entities to truth-values, i.e. characteristic functions of sets if entities. an expression of type is a function from sets of entities to truthvalues, i.e. a (characteristic function of a) set of sets. this latter type is standardly taken to be the type of natural language quantifiers, like every boy or nobody (montague 1973, barwise and cooper 1981). this section is a stub. you can help by expanding it. [edit] connections to constructive logic main article: curry-howard this section is a stub. you can help by expanding it. [edit] relation to other topics this section is a stub. you can help by expanding it. [edit] type system main article: type system definitions of type system vary, but the following one due to benjamin c. pierce roughly corresponds to the current consensus in the programming language theory community: [a type system is a] tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute. (pierce, 2002) in other words, a type system divides program values into sets called types (this is called a "type assignment"), and makes certain program behaviors illegal on the basis of the types that are thus assigned. for example, a type system may classify the value "hello" as a string and the value 5 as a number, and prohibit the programmer from adding "hello" to 5 based on that type assignment. in this type system, the program "hello" + 5 would be illegal. hence, any program permitted by the type system would be provably free from the erroneous behavior of adding strings and numbers. the design and implementation of type systems is a topic nearly as broad as the topic of programming languages itself. in fact, type theory proponents commonly proclaim that the design of type systems is the very essence of programming language design: "design the type system correctly, and the language will design itself." [edit] see also intuitionistic type theory. another mathematical type theory. type system for a more practical discussion of type systems for programming languages duck typing for a trivial solution to typing in some programming languages data type for concrete types of data in programming domain theory

category theory typed lambda calculus bertrand russell [edit] references ^ ernest nagel (1951),"causal character of modern physical theory", freedom and reason, the free press, editors: salo w. baron, ernest nagel and koppel b. pinson. pp.244-268, as reprinted on page 759, the world of physics, editor: jefferson hane weaver, isbn 0-671-49931-9 [edit] further reading barwise, jon and robin cooper, 1981. generalized quantifiers in english. linguistics and philosophy 4:159-219. andrews, peter b., 2002. an introduction to mathematical logic and type theory: to truth through proof, 2nd ed. kluwer academic publishers. cardelli, luca, 1997, "type systems," in allen b. tucker, ed., the computer science and engineering handbook. crc press: 2208-2236. mendelson, elliot, 1997. introduction to mathematical logic, 4th ed. chapman & hall. montague, richard,1973. the proper treatment of quantification in english. in hintikka, k. et al., editor, approaches to natural language, pages 221--242. pierce, benjamin, 2002. types and programming languages. mit press. isbn 0-26216209-1) thompson, simon, 1991. type theory and functional programming. addison-wesley. isbn 0-201-41667-0. winskel, glynn, 1993. the formal semantics of programming languages, an introduction. mit press. isbn 0-262-23169-7. wittgenstein, ludwig, 1922. tractatus logico-philosophicus. new york, ny: routledge, 2005. isbn 0-415-25562-7 [edit] external links stanford encyclopedia of philosophy: type theory" -- by thierry coquand. national institute of standards and technology: abstract data type a summary paper on the formal basis of adts, relationship to category theory, and list of good references. pages 3-4 appear relevant. reference number [6] looks good, but it may not be available online. constable, robert l., 2002, "na�ve computational type theory," in h. schwichtenberg and r. steinbruggen (eds.), proof and system-reliability: 213-259. the nuprl book: "introduction to type theory."