Subjects

Your browser does not support JavaScript, or its support is disabled. Some features may not be available.

Lambda Calculus and Functional Programming I - NAIX078

Title:	Lambda-kalkulus a funkcionální programování I
Guaranteed by:	Student Affairs Department (32-STUD)
Faculty:	Faculty of Mathematics and Physics
Actual:	from 2022
Semester:	winter
E-Credits:	5
Hours per week, examination:	winter s.:2/1, C+Ex [HT]
Capacity:	unlimited
Min. number of students:	unlimited
4EU+:	no
Virtual mobility / capacity:	no
State of the course:	taught
Language:	Czech
Teaching methods:	full-time
Teaching methods:	full-time
Is provided by:	NAIL078

Guarantor:	RNDr. Jan Hric
Class:	Informatika Mgr. - Teoretická informatika
Classification:	Informatics > Programming, Theoretical Computer Science
Pre-requisite :	{NXXX038, NXXX039, NXXX040, NXXX067, NXXX069}
Incompatibility :	NAIL078
Interchangeability :	NAIL078

Opinion survey results Examination dates WS schedule Noticeboard

Annotation -

Last update: T_KTI (14.05.2015)

Combinatorial calculi and lambda calculi, untyped calculi, representability of recursive functions, Church Rosser property and consistency of lambda calculus, typed lambda calculi, functional programming constructs

Aim of the course -

Last update: RNDr. Jan Hric (07.06.2019)

To learn the theory of lambda-calculus, combinatory logic and explainn connections to functional programming.

Course completion requirements -

Last update: RNDr. Jan Hric (07.06.2019)

Oral exam on topics from lecture. Homeworks and selected examples for credits.

Literature -

Last update: T_KTI (14.05.2015)

Henk Barendregt, Erik Barensen: Introduction to Lambda Calculus, 1998, rev. 2000, 53 s. http://www.cs.ru.nl/E.Barendsen/onderwijs/T3/materiaal/lambda.pdf

Hendrik Pieter Barendregt: The Lambda Calculus: Its Syntax and Semantics. Elsevier, Amstredam, 1984. Rev. ed. 1998, 621 s. 0-444-86748-1

Henk Barendregt, Wil Dekkers, Richard Statman: Lambda Calculus with Types. Cambridge University Press, Cambridge, 2010. 682 s. (rev. 2013, 978-0-521-76614-2)

J. Roger Hindley, Jonathan P. Seldin: Lambda-Calculus and Combinators, an Introduction. Cambridge University Press, Cambridge, 2. vyd., 2008, 360 s. 978-0-521-89885-0 (1986. 359 s. 0-521-31839-4)

Katalin Bimbó: Combinatory Logic, The Stanford Encyclopedia of Philosophy (Spring 2013 Edition), Edward N. Zalta (ed.), http://plato.stanford.edu/archives/spr2013/entries/logic-combinatory/#4

Syllabus -

Last update: RNDr. Jan Hric (28.04.2018)

Introduction. Schoenfinkel combinatorial calculus. Combinatorial objects as

representants of single-parameter functions. Representation of multiple-parameter

functions. Abstraction of variables and unknowns. Combinatorial completeness of

calculus. Calculus consistency. Church-Rosser property.

Lambda calculus, informal description. Variables, free and bound, abstraction

bounded and unbounded. Lambda objects in normal form. Church-Rosser property

and uniformity of lambda objects in normal form.

Lambda calculi. Syntactic description of lambda objects, free and bound variables,

alpha and beta reduction. Extensions of lambda calculus, extensionality, delta rule.

Conversion, application, abstraction. Lambda terms, combinators. Fixed-point theorems.

Representation of computable functions. Numerals, boolean constants, tuples.

Representability of (total) recursive functions by lambda terms.

Consistency of combinatorial calculi and lambda calculi. Church-Rosser property

and calculi consistency. Objects without normal form. Paradoxes. Combinatorial

logic and predicate logic: Curry paradox.

Functional programming and lambda calculus. Computational model of functional

language, reduction, normal forms and functional programming, controlling of

computation in functional programming. Strict functions.

Typed lambda calculus. Extension of lambda calculus language with object types.

Motivation for introduction of types: partial correctness of programs, effectivity of computations. Type

variables and value assignment to type variables. Curry and Church type systems.