Church-Numeral

Church-Numeral

Unter Church-Kodierung versteht man die Einbettung von Daten und Operatoren in das Lambda-Kalkül. Die bekannteste Form sind die Church-Numerale, welche die natürlichen Zahlen repräsentieren. Benannt sind sie nach Alonzo Church, der Daten als Erster auf diese Weise modellierte.

Inhaltsverzeichnis

Church-Numerale

Definition

Die Grundidee zur Kodierung beruht auf den Peano-Axiomen, wonach die natürlichen Zahlen durch einen Startwert - die 0 - und einer Nachfolger-Funktion definiert sind. Demnach sind die Church-Numerale wie folgt definiert:

0λf.λx. x
1λf.λx. f x
2λf.λx. f (f x)
3λf.λx. f (f (f x))
...
nλf.λx. fn x

Rechnen mit Church-Numeralen

Im Lambda-Kalkül sind numerische Funktionen durch korrespondierende Funktionen über Church-Numerale darstellbar. Diese Funktionen können in funktionalen Programmiersprachen direkt durch übertragen der Lambda-Ausdrücke implementiert werden.

Die Nachfolger-Funktion wird wie folgt definiert:

succλn.λf.λx.n f (f x)

Die Addition zweier Zahlen n und m ist die m-malige Anwendung der Nachfolger-Funktion auf n:

plusλm.λn.λf.λx. m f (n f x)

Die Multiplikation zweier Zahlen n und m ist die m-malige Anwendung der Addition (+n) auf n:

multλm.λn.λf. n (m f)

Die Vorgänger-Funktion:

predλn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)

Boolesche Ausdrücke

Analog zu den natürlichen Zahlen lassen sich auch (zweiwertige) Wahrheitswerte im Lambda-Kalkül modellieren.

trueλx.λy. x
falseλx.λy. y

Daraus lässt sich auch eine einfache Kontrollstruktur (IF THEN ELSE) ableiten:

ifthenelseλb.λx.λy.b x y

Dabei ist die Variable b als Bedingung zu verstehen, x als "THEN" und y als "ELSE".


Wikimedia Foundation.

Игры ⚽ Нужна курсовая?

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Church encoding — In mathematics, Church encoding is a means of embedding data and operators into the lambda calculus, the most familiar form being the Church numerals, a representation of the natural numbers using lambda notation. The method is named for Alonzo… …   Wikipedia

  • Church Universal and Triumphant — Formation 1975 Type New Religious Movement (Ascended Master Teachings religion) Founder Elizabeth Clare Prophet Church Universal and Triumphant is an international New Age religious organization founded in 1975 by …   Wikipedia

  • Unary numeral system — The unary numeral system is the bijective base 1 numeral system. It is the simplest numeral system to represent natural numbers: in order to represent a number N , an arbitrarily chosen symbol representing 1 is repeated N times. For example,… …   Wikipedia

  • Lambda calculus — In mathematical logic and computer science, lambda calculus, also written as λ calculus, is a formal system designed to investigate function definition, function application and recursion. It was introduced by Alonzo Church and Stephen Cole… …   Wikipedia

  • System F — System F, also known as the polymorphic lambda calculus or the second order lambda calculus, is a typed lambda calculus. It was discovered independently by the logician Jean Yves Girard and the computer scientist John C. Reynolds. System F… …   Wikipedia

  • OCaml — Paradigm(s) multi paradigm: imperative, functional, object oriented Appeared in 1996 Developer INRIA Stable release 3.12.1 (July 4, 2011; 4 months ago ( …   Wikipedia

  • Objective Caml — Infobox programming language name = Objective Caml paradigm = multi paradigm: imperative, functional, object oriented developer = INRIA latest release version = 3.10.2 latest release date = Release date and age|2008|02|29 operating system = Cross …   Wikipedia

  • Fixed-point combinator — Y combinator redirects here. For the technology venture capital firm, see Y Combinator (company). In computer science, a fixed point combinator (or fixpoint combinator[1] ) is a higher order function that computes a fixed point of other functions …   Wikipedia

  • Simply typed lambda calculus — The simply typed lambda calculus (lambda^ o) is a typed interpretation of the lambda calculus with only one type combinator: o (function type). It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus… …   Wikipedia

  • Alpha-Konversion — Der Lambda Kalkül ist eine formale Sprache zur Untersuchung von Funktionen, die Funktionsdefinitionen, das Definieren formaler, sowie das Auswerten und Einsetzen aktueller Parameter regelt. Inhaltsverzeichnis 1 Geschichte 2 Der untypisierte… …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”