In mathematics, an initial algebra is an initial object in the of F-algebras for a given endofunctor F. This initiality provides a general framework for induction and recursion.
Consider the endofunctor F : Set → Set sending X to 1 + X, where 1 is the one-point (singleton) set, the terminal object in the category. An algebra for this endofunctor is a set X (called the carrier of the algebra) together with a function f : (1 + X) → X. Defining such a function amounts to defining a point and a function X → X.
Define
and
Then the set N of natural numbers together with the function [zero,succ]: 1 + N → N is an initial F-algebra. The initiality (the universal property for this case) is not hard to establish; the unique homomorphism to an arbitrary F-algebra (A, [e, f]), for e: 1 → A an element of A and f: A → A a function on A, is the function sending the natural number n to fn(e), that is, f(f(...(f(e))...)), the n-fold application of f to e.
The set of natural numbers is the carrier of an initial algebra for this functor: the point is zero and the function is the successor function.
For a second example, consider the endofunctor 1 + N × (−) on the category of sets, where N is the set of natural numbers. An algebra for this endofunctor is a set X together with a function 1 + N × X → X. To define such a function, we need a point and a function N × X → X. The set of finite lists of natural numbers is an initial algebra for this functor. The point is the empty list, and the function is cons, taking a number and a finite list, and returning a new finite list with the number at the head.
In categories with binary coproducts, the definitions just given are equivalent to the usual definitions of a natural number object and a list object, respectively.
Dually, a final coalgebra is a terminal object in the category of F-coalgebras. The finality provides a general framework for coinduction and corecursion.
For example, using the same functor 1 + (−) as before, a coalgebra is defined as a set X together with a function f : X → (1 + X).
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.
In mathematics, specifically in , F-algebras generalize the notion of algebraic structure. Rewriting the algebraic laws in terms of morphisms eliminates all references to quantified elements from the axioms, and these algebraic laws may then be glued together in terms of a single functor F, the signature. F-algebras can also be used to represent data structures used in programming, such as lists and trees. The main related concepts are initial F-algebras which may serve to encapsulate the induction principle, and the construction F-coalgebras.
In computer programming, an anamorphism is a function that generates a sequence by repeated application of the function to its previous result. You begin with some value A and apply a function f to it to get B. Then you apply f to B to get C, and so on until some terminating condition is reached. The anamorphism is the function that generates the list of A, B, C, etc. You can think of the anamorphism as unfolding the initial value into a sequence.
In computer science, coinduction is a technique for defining and proving properties of systems of concurrent interacting objects. Coinduction is the mathematical to structural induction. Coinductively defined types are known as codata and are typically infinite data structures, such as streams. As a definition or specification, coinduction describes how an object may be "observed", "broken down" or "destructed" into simpler objects. As a proof technique, it may be used to show that an equation is satisfied by all possible implementations of such a specification.
Explores object-oriented programming concepts in C++ focusing on constructors, destructors, initialization lists, and constructor design in Cartesian and polar coordinates.
The structural transition between two alternate conformations of bistable RNAs has been characterized by time-resolved NMR spectroscopy. The mechanism, kinetics, and thermodynamics underlying the global structural transition of bistable RNAs were delineate ...
2007
, ,
Synthesis from examples enables non-expert users to generate programs by specifying examples of their behavior. A domain-specific form of such synthesis has been recently deployed in a widely used spreadsheet software product. In this paper we contribute t ...