Відмінності між версіями «Лямбда-числення»

вікіфікація
(вікіфікація)
== Визначення лямбда-виразів ==
 
Множину λ-виразів можна{{кому}} визначити індуктивно таким чином <ref> M.H. Sorensen and P. Urzyczyn "«Lectures on the Curry-Howard Isomorphism"» (2006) </ref>:
 
* будь-яка ''змінна'' &nbsp;— це λ-вираз;
 
* <math> \lambda </math>-''абстракція'' <math> \lambda x.M </math> &nbsp;— це λ-вираз, якщо ''x'' &nbsp;— це змінна, а <math> M </math> &nbsp;— λ-вираз;
 
* ''аплікація'' <math> MN </math> &nbsp;— це λ-вираз, якщо <math> M </math> та <math> N </math> &nbsp; λ-вирази.
 
Інтуїтивно, абстракції відповідають функціям, а аплікації їх застосуванню. Особливістю лямбда-числення є те, що аргументи "«функцій"», визначених таким чином, &nbsp;— це теж функції. Наприклад, <math> \lambda x.x </math> &nbsp;— це λ-вираз, що відповідає функції ідентичності, а <math> \lambda x.x M </math> &nbsp;— це аплікація цієї функції до <math> M </math>, у випадку коли <math> M </math> &nbsp;— це теж λ-вираз.
 
На цій множині ми визначаємо відношення <math> \rightarrow_\beta </math>, що називається ''бета-редукція'':
 
<math> (\lambda x M)N \rightarrow_\beta M[x:=N] </math>,
 
де <math> M[x:=N] </math> означає, що вираз <math> N </math> підставляється всюди замість змінної x у виразі <math> M </math>.
 
Тоді, у попередньому прикладі матимемо: <math> (\lambda x.x) M \rightarrow_\beta x [x:=M] = M </math>. Як і очікувано, застосування функції ідентичності до певного виразу повертає цей вираз.
{{reflist}}
 
== Література ==
== Джерела інформації ==
 
* Achim Jung, ''[http://www.cs.bham.ac.uk/~axj/pub/papers/lambda-calculus.pdf A Short Introduction to the Lambda Calculus]''-([[Portable Document Format|PDF]])
* Henk Barendregt, The Bulletin of Symbolic Logic, Volume 3, Number 2, June 1997. The Impact of the Lambda Calculus in Logic and Computer Science
* {{cite book|назва=Abstract Computing Machines, The Lambda Calculus perspective|автор=W. Kluge|видавництво=Springer Verlag|рік=2005|isbn=3-540-21146-2}}
* Raúl Rojas, ''[http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf A Tutorial Introduction to the Lambda Calculus]''{{ref-en}} -([[Portable Document Format|PDF]])
* Wolfengagen, V.E. '' Combinatory logic in programming. Computations with objects through examples and exercises''.&nbsp;— 2-nd ed.&nbsp;— M.: «Center JurInfoR» Ltd., 2003.&nbsp;— x+337 с. ISBN 5-89158-101-9.
 
== Див. також ==
 
* [[Типізоване лямбда-числення]]
* [[ФункціональнеФункційне програмування]]
* [[Пі-числення]]
* [[Машина Тюринга]]
* [[Підстановка]]
 
=== Посилання ===
* Raúl Rojas, ''[http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf A Tutorial Introduction to the Lambda Calculus]''{{ref-en}} -([[Portable Document Format|PDF]])
* Wolfengagen, V.E. '' Combinatory logic in programming. Computations with objects through examples and exercises''.&nbsp;— 2-nd ed.&nbsp;— M.: «Center JurInfoR» Ltd., 2003.&nbsp;— x+337 с. ISBN 5-89158-101-9.
 
{{comp-stub}}