Bu ders, fonksiyonel programlamanın hem kuramsal hem de uygulamalı temellerini lambda kalkülüs çerçevesinde ele alır. Öğrencilerin; - Geleneksel programlama yaklaşımlarından farkları anlamaları, - Lambda kalkülüsün sözdizimi, β-indirgeme süreci, hesaplama kuralları, tip sistemleri ve sabit nokta fonksiyonları gibi kavramları kavramaları, - Church-Rosser Teoremi aracılığıyla tutarlılık ve deterministik hesaplama özelliklerini analiz etmeleri, - Fonksiyonel düşünme biçimiyle matematiksel ve algoritmik problemleri modellemeleri hedeflenmektedir. Öğrencilerin, Lean gibi bir formel doğrulama sistemini kullanarak seçtikleri bir problemin çözümünü fonksiyonel yaklaşımla sunmaları beklenmektedir.

Bu ders, fonksiyonel programlamanın kuramsal ve uygulamalı temellerini lambda kalkülüs çerçevesinde ele alır. İlk olarak, fonksiyonel programlamaya giriş yapılarak, geleneksel programlama yaklaşımlarından farkları tartışılır. Ardından, lambda kalkülüsün sözdizimi, hesaplama kuralları ve β-indirgeme gibi temel yapıları ayrıntılı biçimde incelenir. Tip sistemleri ve sabit nokta fonksiyonları üzerinden, tekrarlamalı yapılar ve hesaplama mantığı işlenir. Church-Rosser Teoremi gibi temel kuramlar sayesinde lambda kalkülüsün tutarlılığı ve deterministik davranışları tartışılır. Dersin ikinci yarısında, doğal sayı sistemlerinin formel sistemlerde temsil edilmesi ve ispat sistemlerine tanıtılması üzerinde durulur. Daha sonra, fonksiyonel programlama perspektifiyle bilgisayar dilindeki operatörler, tümevarım prensibi ve mantık sistemleri işlenir. Ders, öğrencilerin kendi seçtikleri bir matematiksel veya algoritmik problemin fonksiyonel bir yaklaşımla modellenip ispatlandığı bir proje sunumuyla tamamlanır. Bu kapsamda, Lean gibi bir formel ispat sisteminin kullanılması teşvik edilir.

Tahtada ders anlatımı ve sunum. Bilgisayarda uygulama.

Michaelson, G. - An Introduction to Functional Programming Through Lambda Calculus-Dover Publications (2011)