CushionTheBlow (구 BluemoonSoft)

Proof-theoretic semantics is an approach to the semantics of logic that attempts to locate the meaning of propositions and logical connectives not in terms of interpretations, as in Tarskian approaches to semantics, but in the role that the proposition or logical connective plays within the system of inference.

Gerhard Gentzen is the founder of proof-theoretic semantics, providing the formal basis for it in his account of cut-elimination for the sequent calculus, and some provocative philosophical remarks about locating the meaning of logical connectives in their introduction rules within natural deduction. It is not a great exaggeration that the history of proof-theoretic semantics since then has been devoted to exploring the consequences of these ideas.

Dag Prawitz extended Gentzen's notion of analytic proof to natural deduction, and suggested that the value of a proof in natural deduction may be understood as its normal form. This idea lies at the basis of the Curry-Howard isomorphism, and of intuitionistic type theory. His inversion principle lies at the heart of most modern accounts of proof-theoretic semantics.

Michael Dummett introduced the very fundamental idea of logical harmony, building on a suggestion of Nuel Belnap. In brief, a language, which is understood to be associated with certain patterns of inference, has logical harmony if it is always possible to recover analytic proofs from arbitrary demonstrations, as can be shown for the sequent calculus by means of cut-elimination theorems and for natural deduction by means of normalisation theorems. A language that lacks logical harmony will suffer from the existence of incoherent forms of inference: it will likely be inconsistent.

Reference:
http://en.wikipedia.org/wiki/Proof-theoretic_semantics

In computing, Internationalization and localization (also spelled internationalisation and localisation, see spelling differences) are means of adapting computer software for non-native environments, especially other nations and cultures. Internationalization is the process of designing a software application so that it can be adapted to various languages and regions without engineering changes. Localization is the process of adapting software for a specific region or language by adding locale-specific components and translating text.

Due to their length, the terms are frequently abbreviated to i18n (where 18 stands for the number of letters between the i and the n in internationalization, a usage coined at DEC in the 1970s or 80s) and L10n respectively. The capital L on L10n helps to distinguish it from the lowercase i in i18n.

Reference:
http://en.wikipedia.org/wiki/I18n#Alternative_names

In software engineering, the singleton pattern is a design pattern that is used to restrict instantiation of a class to one object. This is useful when exactly one object is needed to coordinate actions across the system. Sometimes it is generalized to systems that operate more efficiently when only one or a few objects exist. It is also considered an anti-pattern since it is often used as a euphemism for global variable.

Common uses
The Abstract Factory, Builder, and Prototype patterns can use Singletons in their implementation.
Façade objects are often Singletons because only one Façade object is required.
State objects are often Singletons.
Singletons are often preferred to global variables because:
- They don't pollute the global namespace (or, in languages with namespaces, their containing namespace) with unnecessary variables.
- They permit lazy allocation and initialization, where global variables in many languages will always consume resources.
Singletons behave differently depending on the lifetime of the virtual machine. While a software development kit may start a new virtual machine for every run which results in a new instance of the singleton being created, calls to a singleton e.g. within the virtual machine of an application server behave differently. There the virtual machine remains alive, therefore the instance of the singleton remains as well. Running the code again therefore can retrieve the "old" instance of the singleton which then may be contaminated with values in local fields which are the result of the first run.

Class diagram

Singleton

- singleton : Singleton

- Singleton()
+ getInstance() : Singleton

Implementation
The singleton pattern is implemented by creating a class with a method that creates a new instance of the class if one does not exist. If an instance already exists, it simply returns a reference to that object. To make sure that the object cannot be instantiated any other way, the constructor is made either private or protected. Note the distinction between a simple static instance of a class and a singleton: although a singleton can be implemented as a static instance, it can also be lazily constructed, requiring no memory or resources until needed. Another notable difference is that static member classes cannot implement an interface, unless that interface is simply a marker. So if the class has to realize a contract expressed by an interface, you really have to make it a singleton.

The singleton pattern must be carefully constructed in multi-threaded applications. If two threads are to execute the creation method at the same time when a singleton does not yet exist, they both must check for an instance of the singleton and then only one should create the new one. If the programming language has concurrent processing capabilities the method should be constructed to execute as a mutually exclusive operation.

The classic solution to this problem is to use mutual exclusion on the class that indicates that the object is being instantiated.

Reference:
http://en.wikipedia.org/wiki/Singleton_pattern

In software engineering, a design pattern is a general reusable solution to a commonly occurring problem in software design. A design pattern is not a finished design that can be transformed directly into code. It is a description or template for how to solve a problem that can be used in many different situations. Object-oriented design patterns typically show relationships and interactions between classes or objects, without specifying the final application classes or objects that are involved. Algorithms are not thought of as design patterns, since they solve computational problems rather than design problems.

Not all software patterns are design patterns. Design patterns deal specifically with problems at the level of software design. Other kinds of patterns, such as architectural patterns, describe problems and solutions that have alternative scopes.

Uses
Design patterns can speed up the development process by providing tested, proven development paradigms. Effective software design requires considering issues that may not become visible until later in the implementation. Reusing design patterns helps to prevent subtle issues that can cause major problems, and it also improves code readability for coders and architects who are familiar with the patterns.

Often, people only understand how to apply certain software design techniques to certain problems. These techniques are difficult to apply to a broader range of problems. Design patterns provide general solutions, documented in a format that doesn't require specifics tied to a particular problem.

Design patterns are composed of several sections (see Documentation below). Of particular interest are the Structure, Participants, and Collaboration sections. These sections describe a design motif: a prototypical micro-architecture that developers copy and adapt to their particular designs to solve the recurrent problem described by the design pattern. A micro-architecture is a set of program constituents (e.g., classes, methods...) and their relationships. Developers use the design pattern by introducing in their designs this prototypical micro-architecture, which means that micro-architectures in their designs will have structure and organization similar to the chosen design motif.

In addition, patterns allow developers to communicate using well-known, well understood names for software interactions. Common design patterns can be improved over time, making them more robust than ad-hoc designs.

Domain specific patterns
Efforts have also been made to codify design patterns in particular domains, including use of existing design patterns as well as domain specific design patterns. Examples include User Interface design patterns, Information Visualization and web design.

The Pattern Languages Of Programming Conference(annual,1994->) proceedings includes many examples of domain specific patterns.

Reference:
http://en.wikipedia.org/wiki/Design_pattern_%28computer_science%29

In mathematics, axiomatic set theory is a reformulation of set theory as a rigorous axiomatic first order theory. The intention was to create a set theory free of the antinomies (paradoxes) that afflicted naive set theory. Axiomatic set theory has since become the canonical approach to the foundation of mathematics, and an active research area in its own right, albeit by relatively few mathematicians.

The undefined concepts of set theory are "set" and "set membership." A set is any collection of objects, called the members (or elements) of the set. An object can be anything physical or abstract of interest to humans; in particular, an object can be (and often) is itself a set. In mathematics, the members of sets are mathematical constructions. Thus one speaks of the set N of natural numbers { 0, 1, 2, 3, 4, ... }, the set R of real numbers, and the set of functions from the natural numbers to the natural numbers; but also, for example, of the set { 0, 2, N}, whose members are 0, 2 and the set N.
Initially controversial, set theory has since become the main foundational theory of modern mathematics. (There is active research in foundational theories other than set theory.) The mathematical objects (numbers, functions, etc.,) of algebra, analysis, topology, etc., are now normally defined as particular sets having particular properties. It is commonly thought (but not empirically demonstrated or logically demonstrable) that most or all of contemporary mathematics consists of theorems that can be proved using axiomatic set theory.

Reference:
http://en.wikipedia.org/wiki/Axiomatic_set_theory

In mathematical logic, a definable set is an n-ary relation on the domain of a structure whose elements are precisely those elements satisfying some formula in the structure. A set can be defined with or without parameters, which are elements of the domain that can be referenced in the formula defining a set. Note that a unary relation on the domain of a structure is simply a subset of the domain, and when we refer to the definable sets in a structure we often mean the definable subsets of the domain. Formally,

For a given first-order language L, let M be an L-structure with domain M and X ⊆ M. We say that A ⊆ M^m is definable in M with parameters from X if and only if there exists a formula p(x_1, ..., x_m, y_1, ..., y_n) and elements b_1, ..., b_n ∈ X such that for all a_1, ..., a_m ∈ M,

(a_1, ..., a_m) ∈ A if and only if M |= p[a_1, ..., a_m, b_1, ..., b_n]

(Note that the bracket notation above indicates the semantic evaluation of the free variables in the formula.) We say that A is definable in M without parameters if and only if it is definable in M with parameters from the empty set.

Reference:
http://en.wikipedia.org/wiki/Definable_set

In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a mathematical object to prove that it exists. When one assumes that an object does not exist and derives a contradiction from that assumption, one still has not found the object and therefore not proved its existence, according to constructivists. See constructive proof.

Constructivism is often confused with intuitionism, but in fact, intuitionism is only one kind of constructivism. Intuitionism maintains that the foundations of mathematics lie in the individual mathematician's intuition, thereby making mathematics into an intrinsically subjective activity. Constructivism does not, and is entirely consonant with an objective view of mathematics.

Reference:
http://en.wikipedia.org/wiki/Constructivism_%28mathematics%29