| dbpprop:abstract
|
- In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. It was introduced by Alonzo Church in 1932 as part of an investigation into the foundations of mathematics
- 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.
- El càlcul lambda és un sistema formal dissenyat per investigar la definició de funció, la noció d'aplicacions de funcions i la recursió. Fou introduït per Alonzo Church i Stephen Kleene a la dècada de 1930; Church va usar el càlcul lambda al 1936 per resoldre el Entscheidungsproblem. Pot ser usat per definir de manera neta i precisa què és una "funció computable". Church va resoldre negativament el Entscheidungsproblem: va provar que no hi ha algorisme que pugui ser considerat com una "solució" al Entscheidungsproblem. El càlcul lambda ha influït enormement en el disseny de llenguatges de programació funcionals, especialment LISP. Es pot considerar al càlcul lambda com el més petit llenguatge universal de programació. Consisteix en una regla de transformació simple i un esquema simple per definir funcions. El càlcul lambda és universal perquè qualsevol funció computable pot ser expressada i avaluada mitjançant ell. Per tant, és equivalent a les màquines de Turing. Tot i això, el càlcul lambda no fa èmfasi en l'ús de regles de transformació i no considera les màquines reals que puguin implementar-lo. Es tracta doncs d'una proposta més propera al programari que al maquinari.
- Lambda kalkul je formální systém a výpočetní model používaný v teoretické informatice a matematice pro studium funkcí a rekurze. Jeho autory jsou Alonzo Church a Stephen Cole Kleene. Lambda kalkul je teoretickým základem funkcionálního programování a příslušných programovacích jazyků, obzvláště Lispu. Lambda kalkul analyzuje funkce nikoli z hlediska původního matematického smyslu zobrazení z množiny do množiny, ale jako metodu výpočtu. Dá se chápat jako nejjednodušší univerzální programovací jazyk. Je univerzální, neboť libovolnou rekurzivně spočetnou funkci lze vyjádřit a vyčíslit pomocí tohoto formalismu, lambda kalkul je tedy výpočetní silou ekvivalentní Turingovu stroji. Tento článek se bude zaobírat netypovým lambda kalkulem. Existuje totiž rozšíření zvané typový lambda kalkul.
- El cálculo lambda es un sistema formal diseñado para investigar la definición de función, la noción de aplicación de funciones y la recursión. Fue introducido por Alonzo Church y Stephen Kleene en la década de 1930; Church usó el cálculo lambda en 1936 para resolver el Entscheidungsproblem. Puede ser usado para definir de manera limpia y precisa qué es una "función computable". El interrogante de si dos expresiones del cálculo lambda son equivalentes no puede ser resuelto por un algoritmo general. Esta fue la primera pregunta, incluso antes que el problema de la parada, para el cual la indecidibilidad fue probada. El cálculo lambda tiene una gran influencia sobre los lenguajes funcionales, como Lisp, ML y Haskell. Se puede considerar al cálculo lambda como el más pequeño lenguaje universal de programación. Consiste en una regla de transformación simple y un esquema simple para definir funciones. El cálculo lambda es universal porque cualquier función computable puede ser expresada y evaluada a través de él. Por lo tanto, es equivalente a las máquinas de Turing. Sin embargo, el cálculo lambda no hace énfasis en el uso de reglas de transformación y no considera las máquinas reales que pueden implementarlo. Se trata de una propuesta más cercana al software que al hardware. Este artículo se enfocará sobre el cálculo lambda sin tipos, como fue diseñado originalmente por Church. Desde entonces, algunos cálculo lambda tipados fueron creados.
- Le lambda-calcul (ou λ-calcul) est un système formel inventé par Alonzo Church dans les années 1930, qui fonde les concepts de fonction et d'application. Il a été le premier formalisme utilisé pour définir et caractériser les fonctions récursives et donc il a une grande importance dans la théorie de la calculabilité, à l'égal des machines de Turing et du modèle de Herbrand-Gödel. Il a depuis été appliqué comme langage de programmation théorique et comme métalangage pour la démonstration formelle assistée par ordinateur. Le lambda-calcul peut être ou non typé. Le lambda-calcul est apparenté à la logique combinatoire de Haskell Curry.
- A lambda-kalkulus (vagy λ-kalkulus) egy formális rendszer, amit eredetileg matematikai függvények tulajdonságainak vizsgálatára vezettek be. Az elmélet kidolgozói Alonzo Church és Stephen Cole Kleene voltak az 1930-as években. Church, 1936-ban, a λ-kalkulus segítségével bizonyította, hogy nem létezik algoritmus a híres Entscheidungsproblem (döntési probléma) megoldására. A λ-kalkulus lehetővé teszi, hogy pontosan (formálisan) definiáljuk, mit is értünk kiszámítható függvény alatt. A λ-kalkulust nyugodtan nevezhetjük a legegyszerűbb általános célú programozási nyelvnek. Csak egyfajta értéket ismer: a függvényt (absztrakciót), és csak egyfajta művelet van benne: a függvény alkalmazás (változó-behelyettesítés). Ezen látszólagos egyszerűsége ellenére valószínű (eddig nem sikerült formálisan bizonyítani) hogy minden algoritmus, ami Turing-gépen megvalósítható, az megvalósítható tisztán a λ-kalkulusban is. Ez a feltételezett azonosság a λ-kalkulus és a Turing-gép kifejező ereje (expressive power) között adja egyébként a Church-Turing-tézis alapját. Míg korábban a λ-kalkulus elsősorban a kiszámíthatóságelmélet (Theory of Computation) miatt volt érdekes, napjainkban ez már kevésbé hangsúlyos, és sokkal inkább a funkcionális programozási nyelvek elméleti és gyakorlati megalapozásában játszott jelentős, mondhatni központi szerepe került előtérbe. A szócikk tárgya a λ-kalkulus, eredeti, típus-nélküli változata. A λ-kalkulus bevezetése óta számos típusos lambda-kalkulus került kifejlesztésre, és valójában ezek a típusos változatok adják a mai funkcionális programozási nyelvek alapját.
- Il lambda calcolo è un sistema di riscrittura definito formalmente dal matematico Alonzo Church. È stato sviluppato per analizzare formalmente le definizioni di funzioni, le loro applicazioni ed è uno strumento interessante per studiare anche fenomeni di ricorsione. In quanto sistema di riscrittura, esso dà una descrizione dei termini ben formati, che sono le sequenze di simboli riconosciute dal sistema e in grado di essere riscritti da esso. Il lambda calcolo, infatti, definisce un insieme di regole di riscrittura che determinano in maniera precisa come i termini stessi possano essere riscritti. In questo modo, il processo di riscrittura diventa un vero e proprio calcolo. Per tale ragione, nel corso di questa descrizione ci si riferirà al lambda calcolo come il calcolo, quando non ci sarà pericolo di ambiguità. Il lambda calcolo affonda le proprie radici nel concetto di funzione. In matematica si definiscono funzioni particolari associazioni fra gli elementi di un insieme e gli elementi di un altro insieme. Ad esempio, se chiamiamo quadrato la funzione che dato un numero restituisca il suo quadrato, scriviamo: quadrato : <math>\mathbb{R} \to \mathbb{R}</math>. per indicare che quadrato mappa elementi dell'insieme dei numeri reali su altri elementi dello stesso insieme. Se una funzione è in grado di associare un risultato ad un certo argomento che le viene passato, diremo che tale funzione è definita per quel valore passato come argomento. Se una funzione è definita su ogni elemento del dominio, essa è detta totale; in caso contrario, diremo che si tratta di una funzione parziale. La notazione insiemistica non fornisce informazioni a proposito di come effettivamente si possa passare dagli argomenti ricevuti al risultato ad essi associato. In altre parole, non si descrive come calcolare il risultato della funzione stessa, a partire dai suoi argomenti . Il lambda calcolo, così come la Teoria delle Funzioni Ricorsive e la Macchina di Turing, è un formalismo che consente di definire il lato meccanico delle funzioni, ovvero proprio quelle procedure che consentono di produrre dei valori in uscita a partire da certi valori in ingresso. Di seguito vedremo una descrizione della sintassi del lambda calcolo che procederà per gradi: dopo aver definito come sono fatti i termini del lambda calcolo, introdurremo le regole di riscrittura del calcolo stesso; dopodiché vedremo alcune strategie di riscrittura, le quali definiscono un ordine con cui applicare le regole di riscrittura, e come la scelta di una regola piuttosto che un'altra garantisca (o inibisca) determinate proprietà del calcolo.
- ラムダ計算（lambda calculus）は、理論計算機科学や数理論理学における、関数の定義と実行を抽象化した計算体系である。ラムダ算法とも言う。
- De lambdacalculus, soms ook als λ-calculus geschreven, is een formeel systeem dat in de wiskunde en theoretische informatica gebruikt wordt om het definiëren en uitvoeren van berekenbare functies te onderzoeken. Hij werd in 1936 door Alonzo Church en Stephen Kleene geïntroduceerd als onderdeel van hun onderzoek naar de grondbeginselen van de wiskunde, maar wordt tegenwoordig vooral gebruikt bij het onderzoeken van berekenbaarheid en recursietheorie. De lambdacalculus kan gezien worden als een soort minimale programmeertaal die in staat is elk algoritme te beschrijven (de lambdacalculus is Turing-volledig), en vormt de basis van het functionele programmeerparadigma. De rest van dit artikel gaat over de (oorspronkelijke) ongetypeerde lambdacalculus. De meeste toepassingen gebruiken getypeerde varianten daarvan.
- Rachunek lambda to system formalny używany do badania zagadnień związanych z podstawami matematyki jak rekurencja, definiowalność funkcji, obliczalność, podstawy matematyki np. definicja liczb naturalnych, wartości logicznych, itd. Rachunek lambda został wprowadzony przez Alonzo Churcha i Stephen Cole Kleene w 1930 roku. Rachunek lambda jest przydatny do badania algorytmów. Wszystkie algorytmy, które dadzą się zapisać w rachunku lambda, dadzą się zaimplementować na maszynie Turinga i odwrotnie. Istnieje wiele rodzajów rachunku lambda, z czego najprostszym jest rachunek lambda bez typów. Rachunek lambda z typami jest podstawą funkcyjnych języków programowania.
- Cálculo lambda foi desenvolvido na década de 30 por Alonzo Church como parte de um sistema para lógicas de ordem superior e teoria das funções. O cálculo lambda pode ser considerado como uma linguagem de programação abstrata, isto é, as maneiras como funções podem ser combinadas para formar outras funções, é uma linguagem pura, sem efeitos colaterais, e sem complicações sintáticas. A principal característica do cálculo lambda são as entidades que podem ser utilizadas como argumentos e retornadas como valores de outras funções. Formalmente, começamos com números infinitos de identificadores: {a, b, c... , x, y, z, x1, x2...}. O jogo de todas as expressões do lambda pode então ser descrito pela seguinte Gramática livre de contexto na Forma Normal de Backus: <expr> ::= (λ <identifier>. <expr>)
- Ля́мбда-исчисле́ние (λ-исчисление, лямбда-исчисление) — формальная система, разработанная американским математиком Алонзо Чёрчем, для формализации и анализа понятия вычислимости. λ-исчисление может рассматриваться как семейство прототипных языков программирования. Их основная особенность состоит в том, что они являются языками высших порядков. Тем самым обеспечивается систематический подход к исследованию операторов, аргументами которых могут быть другие операторы, а значением также может быть оператор. Языки в этом семействе являются функциональными, поскольку они основаны на представлении о функции или операторе, включая функциональную аппликацию и функциональную абстракцию. λ-исчисление реализовано Джоном Маккарти в языке Лисп. В начале реализация идей λ-исчисления была весьма громоздкой. Но по мере развития Лисп-технологии (прошедшей этап аппаратной реализации в виде Лисп-машины) идеи получили ясную и четкую реализацию.
- Lambdakalkyl (λ-kalkyl) är i ett formellt system som skapades för att undersöka funktioner och rekursion. Lambdakalkylen utvecklades på 1920-talet av Alonzo Church. På 1960-talet förstod man att lambdakalkylen kunde användas för att förstå programspråk. Det har därför blivit den matematiska grunden för funktionella programspråk. Objekten i lambdakalkyl är termer (som ibland kallas lambdatermer). Det finns tre typer av termer Variabler, x, y, z, ... abstraktion, <math>\lambda x. t</math> där t är en term applikation, <math>t_1\ t_2</math> där <math>t_1</math> och <math>t_2</math> är termer Abstraktion kan ses som definition av en funktion och applikation motsvarar tillämpning av en funktion. På termerna använder man olika typer av reduktioner för att visa satser om lambdakalkylen. Lite förenklat är reduktionerna: α-reduktion - namnen på variblerna kan bytas β-reduktion - en term <math>(\lambda x. t_1)\ s</math> reduceras till termen <math>t_2</math> som är termen <math>t_1</math> med alla x utbytta mot s η-konvertering - termen <math>\lambda x. f\ x</math> konverteras till termen f
- Ля́мбда-чи́слення, або λ-числення — формальна система, що використовується в теоретичній кібернетиці для дослідження визначення функції, застосування функції, та рекурсії. Це числення було запропоноване Алонсо Черчем та Стівеном Кліні в 1930-ті роки, як частина більшої спроби розробити базис математики на основі функцій а не множин (задля уникнення таких перешкод, як Парадокс Рассела). Однак, Парадокс Кліні-Россера демонструє, що лямбда числення не здатне уникнути множинно-теоретичний парадоксів. Не дивлячись на це, лямбда числення виявилось зручним інструментом в дослідженні обчислюваності функцій, та лягло в основу парадигми функціонального програмування. Лямбда числення може розглядатись як ідеалізована, мінімалістича мова програмування, в цьому сенсі лямбда числення подібне до машини Тюринга, іншої мінімалістичної абстракції, здатної визначати будь-який алгоритм. Відмінність між ними полягає в тому, що лямбда числення відповідає функціональній парадигмі визначення алгоритмів, а машина Тюринга, натомість — імперативній. Тобто, машина Тюринга має певний «стан» — перелік символів, що можуть змінюватись із кожною наступною інструкцією. На відміну від цього, лямбда числення уникає станів, воно має справу з функціями, котрі отримують значення параметрів та повертають результати обчислень (можливо, інші функції), але не спричиняють до зміни вхідних даних. Ядро λ-числення грунтується трохи більше ніж на визначені змінних, області видимості змінних та впорядкованому заміщенні змінних виразами. λ-числення є замкненою мовою, тобто, семантика мови може бути визначена на основі еквівалентності виразів (або термів) самої мови.
- λ演算（lambda calculus）是一套用于研究函数定义、函数应用和递归的形式系统。它由丘奇（Alonzo Church）和他的學生克莱尼（Stephen Cole Kleene）在20世纪30年代引入。Church 运用λ演算在1936年给出判定性问题（Entscheidungsproblem）的一个否定的答案。这种演算可以用来清晰地定义什么是一个可计算函数。关于两个 lambda 演算表达式是否等价的命题无法通过一个“通用的算法”来解决，这是不可判定性能够证明的头一个问题，甚至还在停机问题之先。Lambda 演算对函数式编程语言有巨大的影响，比如 Lisp 语言、ML 语言和 Haskell 语言。 Lambda 演算可以被称为最小的通用程序设计语言。它包括一条变换规则（变量替换）和一条函数定义方式，Lambda 演算之通用在于，任何一个可计算函数都能用这种形式来表达和求值。因而，它是等价于图灵机的。尽管如此，Lambda 演算强调的是变换规则的运用，而非实现它们的具体机器。可以认为这是一种更接近软件而非硬件的方式。 本文讨论的是 Church 的“无类型 lambda 演算”，此后，已经研究出来了一些有类型 lambda 演算。
|
| rdfs:comment
|
- In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. It was introduced by Alonzo Church in 1932 as part of an investigation into the foundations of mathematics
- 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.
- El càlcul lambda és un sistema formal dissenyat per investigar la definició de funció, la noció d'aplicacions de funcions i la recursió. Fou introduït per Alonzo Church i Stephen Kleene a la dècada de 1930; Church va usar el càlcul lambda al 1936 per resoldre el Entscheidungsproblem. Pot ser usat per definir de manera neta i precisa què és una "funció computable".
- Lambda kalkul je formální systém a výpočetní model používaný v teoretické informatice a matematice pro studium funkcí a rekurze. Jeho autory jsou Alonzo Church a Stephen Cole Kleene. Lambda kalkul je teoretickým základem funkcionálního programování a příslušných programovacích jazyků, obzvláště Lispu. Lambda kalkul analyzuje funkce nikoli z hlediska původního matematického smyslu zobrazení z množiny do množiny, ale jako metodu výpočtu.
- El cálculo lambda es un sistema formal diseñado para investigar la definición de función, la noción de aplicación de funciones y la recursión. Fue introducido por Alonzo Church y Stephen Kleene en la década de 1930; Church usó el cálculo lambda en 1936 para resolver el Entscheidungsproblem. Puede ser usado para definir de manera limpia y precisa qué es una "función computable".
- Le lambda-calcul (ou λ-calcul) est un système formel inventé par Alonzo Church dans les années 1930, qui fonde les concepts de fonction et d'application. Il a été le premier formalisme utilisé pour définir et caractériser les fonctions récursives et donc il a une grande importance dans la théorie de la calculabilité, à l'égal des machines de Turing et du modèle de Herbrand-Gödel.
- A lambda-kalkulus (vagy λ-kalkulus) egy formális rendszer, amit eredetileg matematikai függvények tulajdonságainak vizsgálatára vezettek be. Az elmélet kidolgozói Alonzo Church és Stephen Cole Kleene voltak az 1930-as években. Church, 1936-ban, a λ-kalkulus segítségével bizonyította, hogy nem létezik algoritmus a híres Entscheidungsproblem (döntési probléma) megoldására.
- Il lambda calcolo è un sistema di riscrittura definito formalmente dal matematico Alonzo Church. È stato sviluppato per analizzare formalmente le definizioni di funzioni, le loro applicazioni ed è uno strumento interessante per studiare anche fenomeni di ricorsione. In quanto sistema di riscrittura, esso dà una descrizione dei termini ben formati, che sono le sequenze di simboli riconosciute dal sistema e in grado di essere riscritti da esso.
- ラムダ計算（lambda calculus）は、理論計算機科学や数理論理学における、関数の定義と実行を抽象化した計算体系である。ラムダ算法とも言う。
- De lambdacalculus, soms ook als λ-calculus geschreven, is een formeel systeem dat in de wiskunde en theoretische informatica gebruikt wordt om het definiëren en uitvoeren van berekenbare functies te onderzoeken. Hij werd in 1936 door Alonzo Church en Stephen Kleene geïntroduceerd als onderdeel van hun onderzoek naar de grondbeginselen van de wiskunde, maar wordt tegenwoordig vooral gebruikt bij het onderzoeken van berekenbaarheid en recursietheorie.
- Rachunek lambda to system formalny używany do badania zagadnień związanych z podstawami matematyki jak rekurencja, definiowalność funkcji, obliczalność, podstawy matematyki np. definicja liczb naturalnych, wartości logicznych, itd. Rachunek lambda został wprowadzony przez Alonzo Churcha i Stephen Cole Kleene w 1930 roku. Rachunek lambda jest przydatny do badania algorytmów.
- Cálculo lambda foi desenvolvido na década de 30 por Alonzo Church como parte de um sistema para lógicas de ordem superior e teoria das funções. O cálculo lambda pode ser considerado como uma linguagem de programação abstrata, isto é, as maneiras como funções podem ser combinadas para formar outras funções, é uma linguagem pura, sem efeitos colaterais, e sem complicações sintáticas.
- Ля́мбда-исчисле́ние (λ-исчисление, лямбда-исчисление) — формальная система, разработанная американским математиком Алонзо Чёрчем, для формализации и анализа понятия вычислимости.
- Lambdakalkyl (λ-kalkyl) är i ett formellt system som skapades för att undersöka funktioner och rekursion. Lambdakalkylen utvecklades på 1920-talet av Alonzo Church. På 1960-talet förstod man att lambdakalkylen kunde användas för att förstå programspråk. Det har därför blivit den matematiska grunden för funktionella programspråk. Objekten i lambdakalkyl är termer (som ibland kallas lambdatermer). Det finns tre typer av termer Variabler, x, y, z, ...
- Ля́мбда-чи́слення, або λ-числення — формальна система, що використовується в теоретичній кібернетиці для дослідження визначення функції, застосування функції, та рекурсії.
|
![[RDF Data]](/statics/sw-cube.png)
