In mathematics and computer science in general, a fixed point of a function is a value that is mapped to itself by the function.
In combinatory logic for computer science, a fixed-point combinator (or fixpoint combinator) is a higher-order function that returns some fixed point of its argument function, if one exists.
Formally, if the function f has one or more fixed points, then
and hence, by repeated application,
In the classical untyped lambda calculus, every function has a fixed point.
A particular implementation of fix is Curry's paradoxical combinator Y, represented by
In functional programming, the Y combinator can be used to formally define recursive functions in a programming language that does not support recursion.
This combinator may be used in implementing Curry's paradox. The heart of Curry's paradox is that untyped lambda calculus is unsound as a deductive system, and the Y combinator demonstrates this by allowing an anonymous expression to represent zero, or even many values. This is inconsistent in mathematical logic.
Applied to a function with one variable, the Y combinator usually does not terminate. More interesting results are obtained by applying the Y combinator to functions of two or more variables. The additional variables may be used as a counter, or index. The resulting function behaves like a while or a for loop in an imperative language.
Used in this way, the Y combinator implements simple recursion. In the lambda calculus, it is not possible to refer to the definition of a function inside its own body by name. Recursion though may be achieved by obtaining the same function passed in as an argument, and then using that argument to make the recursive call, instead of using the function's own name, as is done in languages which do support recursion natively. The Y combinator demonstrates this style of programming.
An example implementation of Y combinator in two languages is presented below.
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.
Learn how to design and implement reliable, maintainable, and efficient software using a mix of programming skills (declarative style, higher-order functions, inductive types, parallelism) and
fundam
A hands-on introduction to interactive theorem proving, proofs as programs, dependent types, and to the Coq proof assistant. Come learn how to write bug-free code!
The course introduces the foundations on which programs and programming languages are built. It introduces syntax, types and semantics as building blocks that together define the properties of a progr
Curry's paradox is a paradox in which an arbitrary claim F is proved from the mere existence of a sentence C that says of itself "If C, then F", requiring only a few apparently innocuous logical deduction rules. Since F is arbitrary, any logic having these rules allows one to prove everything. The paradox may be expressed in natural language and in various logics, including certain forms of set theory, lambda calculus, and combinatory logic. The paradox is named after the logician Haskell Curry.
The simply typed lambda calculus (), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor () that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical use of the untyped lambda calculus. The term simple type is also used to refer extensions of the simply typed lambda calculus such as products, coproducts or natural numbers (System T) or even full recursion (like PCF).
In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded data in the lambda calculus this way. Terms that are usually considered primitive in other notations (such as integers, booleans, pairs, lists, and tagged unions) are mapped to higher-order functions under Church encoding.
The Lasp programming language provides combinator functions such as Union and Intersection for combining set CRDTs. When designing a CRDT combinator, care must be taken to ensure that the combinator is monotone separately in each of its arguments, so that ...
2017
, ,
We introduce a technique for the analysis of general spatially coupled systems that are governed by scalar recursions. Such systems can be expressed in variational form in terms of a potential function. We show, under mild conditions, that the potential fu ...
We study the scaling dimension Delta(phi n) of the operator phi(n) where phi is the fundamental complex field of the U(1) model at the Wilson-Fisher fixed point in d = 4 - epsilon. Even for a perturbatively small fixed point coupling lambda*, standard pert ...