Fixed-point combinator

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.

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés (13)

Cours associés (7)

Séances de cours associées (22)

Définitions récursives imbriquées CS-210: Functional programming

Explore les définitions récursives imbriquées en utilisant des environnements et la levée de fonctions binaires pour travailler sur des valeurs.

Récursivité : comprendre les fonctions récursives CS-550: Formal verification

Explore la récursion, les points de fixation et les procédures en profondeur, en mettant l'accent sur la compréhension des fonctions récursives.

Régression polynôme et descente progressive ENG-209: Data science for engineers with Python

Couvre la régression polynôme, la descente en gradient, le surajustement, le sous-ajustement, la régularisation et la mise à l'échelle des caractéristiques dans les algorithmes d'optimisation.

CS-210: Functional programming

Understanding of the principles and applications of functional programming, the fundamental models of program execution, application of fundamental methods of program composition, meta-programming thr

CS-452: Foundations of software

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

CS-101: Advanced information, computation, communication I

Discrete mathematics is a discipline with applications to almost all areas of study. It provides a set of indispensable tools to computer science in particular. This course reviews (familiar) topics a

Fixed-point combinator

Simply typed lambda calculus

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).

Church encoding

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.