MY own Glossary




Arrow (morphism, map) :  [Category Theory] an abstraction derived from structure-preserving mappings between two mathematical structures.

For each arrow f there are given objects: dom(f) cod(f). If we call dom(f) by A and cod(f) by B, then we write f : AB



Category :  [Category Theory] a category is an algebraic structure consisting of :

                    Objects  : A, B, C, ...

                    Arrows :  f, g, h, ...

                    Composite : o

                    Identity arrow : 1A for Object A

Closed :

    closed set : [Math] a set is said to be closed under some operation if performance of that operation on members of the set always produces a unique member of the set.

For example, the real numbers are closed under subtraction, but the natural numbers are not: 3 and 8 are both natural numbers, but the result of 3 − 8 is not.

    closed term : A term with no free variables.

Composite : [Category Theory] given arrows f : AB and g : BC, there is a given arrow

h = g o f, h : A → C is called the composite of f and g.

Consistency : [Logic] a consistent theory is one that does not contain a contradiction.[1]

A set of formulas Φ in first-order logic is consistent (written Con Φ) if and only if there is no formula φ such that Φ ⊢ φ and Φ ⊢ ¬ φ. Otherwise Φ is inconsistent and is written Inc Φ.


Definitional equality : a ≡ b. It is intensional. e.g. there is no definitional equality of n and n + 0.

Denotational semantics : [Me] what it means in other system. [Wikipedia] In computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects (called denotations) which describe the meanings of expressions from the languages. Broadly speaking, denotational semantics is concerned with finding mathematical objects called domains that represent what programs do.


Endo- : [prefix] within ~.

    endomap : map from A -> A

Extension : [Logic] the range of a term or concept as measured by the objects that it denotes or contains, as opposed to its internal content. Often contrasted with intension . [Dic]

Extensional type theory : [Type Theory]

Extensional property : [Linguistics] property revealed outside of certain thing (e.g. function + for natural numbers), describing how it behaves. [Me]


First-order : "without self-reference", as in first-order logic and other logic uses, where it is contrasted with "allowing some self-reference" (higher-order logic).

first order logic :You can quantify over variables but not predicate. [Christian]

Free variable : [Math] is a notation that specifies places in an expression where substitution may take place. The idea is related to a placeholder (a symbol that will later be replaced by some literal string), or a wildcard character that stands for an unspecified symbol.

[CS] a free variable is a variable referred to in a function that is not a local variable or an argument of that function.[1] An upvalue is a free variable that has been bound (closed over) with a closure. Note that variable "freeness" only applies in lexical scoping. There's no distinction when using dynamic scope. That's also why there are no closures in dynamic scope.

Function space : [Math] In mathematics, a function space is a set of functions of a given kind from a set X to a set Y. It is called a space because in many applications it is a topological space, a vector space, or both.

Functor : [Category Theory] F : C1C2 between categories C1 and C2 is a mapping of objects and arrows to arrows, in such a way that :

  1. (a)F( f : A → B ) = F( f ) : F(A) → F(B) ---------- mapping arrows

  2. (b)F( g o f ) = F( g ) o F( f ) ------------------------ mapping composition

  3. (c)F(1A) = 1F(A) -------------------------------------- mapping identity arrows


Ground term : [Math] a ground term of a formal system is a term that does not contain any variables at all.

Group : In mathematics, a group is an algebraic structure consisting of a set together with an operation that combines any two of its elements to form a third element. [monoid + inversere    ]



Identity arrow : 1A called the identity morphism for Object A (unique endomap)

                            | ∀ A, ∃ 1A : AA, ∀ f : a → b, 1b o f = f = f o 1a. [Awodey]

Intension : [Logic] the internal content of a concept. Often contrasted with extension. [Dic]

Intensional property : [Linguistics] property concerning about the definition of certain thing, describing how it is defined. [Me]

    Example : ‘morning star’ and ‘evening star’ both refers to Venus. They are interchangeable

                        in “morning star is the second planet from the Sun”, but not in “morning

                        star appears the name given to the planet Venus when it appears in the   

                        East (morning sky) before sunrise” [Thorsten]

Isomorphism : [Category Theory] In any Category C, an arrow f : A → B is called an isomorphism if there is an arrow g : B → A in C such that

g o f = 1A

f o g = 1B

A B : A is isomorphic to B





Monoid : In abstract algebra, a branch of mathematics, a monoid is an algebraic structure with a single associative binary operation and an identity element. (Semigroup + identity element)



Operational semantics : [Me] how it operates in this system, what does it mean, explained in terms of existed rules in this system. [Wikipedia] In computer science, operational semantics is a way to give meaning to computer programs in a mathematically rigorous way. The operational semantics for a programming language describes how a valid program is interpreted as sequences of computational steps. These sequences then are the meaning of the program.


Poset (Partially ordered set) : [mathematics] [order theory] it formalizes the intuitive concept of an ordering of the elements of a set.

A poset consists of a set together with a binary relation that indicates that, for certain pairs of elements in the set, one of the elements precedes the other.

These relations are called partial orders to reflect the fact that not every pair of elements of a poset need be related: for some pairs, it may be that neither element precedes the other in the poset.

Propositionally equality : p ∈ a = b, it is extensional, i.e. two objects are equal, if

all observations about them agree.




Saturated Expression: [philosophy] [Logic] saturated expression refers to an object or argument and has a complete sense in itself, while an unsaturated expression refers to a concept or function and does not have a complete sense. For example, in the sentence “Socrates is the teacher of Plato,” “Socrates” and “Plato” are proper names and are saturated, while “… is the teacher of …” is unsaturated, for it has empty spaces that must be filled with saturated expressions before it gains a complete sense.

Semigroup : is an algebraic structure consisting of a set S together with an associative binary operation.


Term : [Math] A term is a mathematical expression which may form a separable part of an equation, a series, or another expression.