Till KTH:s startsida Till KTH:s startsida

Lambda calculus

This is a formal description of a small functional language (that looks a bit like Elixir). We will build it from the ground up, starting with the basic data structures and then define how expressions are evaluated. Even if the language is very small we will have some points in the design were we need to do a choice; depending on our choices our language will have different properties.

Lambda calculus

All functional programming languages have their roots in lambda calculus. You should have a basic understanding of this calculus since many of the properties of our language example is described in terms of lambda expressions and how they are evaluated. Read the following tutorial and do the programming exercises in order to better understand what we are talking about. 

The operational semantics

We use a simplified functional programming language to describe properties of different alternatives. I've summarized the lectures that presents the operational semantics.

Going further

In this very limited description we have omitted a few things. If you want to know more how functional programming languages are defined you can look at the following two references:

  • The Implementation of Functional Programming Languages by Simon L. Peyton Jones. This is the classical book in the area. You don't have to read the whole book but do take a look at the first set of chapters. You will see how the approach is very close to how we have worked. In the book a functional programming language, Miranda, is defined in terms of lambda calculus. Lambda expressions are then given an operational semantics by being expressed as abstract machine instructions.
  • Teaching Creative Computer Science , Simon Peyton Jones at TEDx: 

Lärare Johan Montelius skapade sidan 19 januari 2015

Lärare Johan Montelius ändrade rättigheterna 21 januari 2015

Kan därmed läsas av alla och ändras av lärare.
Johan Montelius redigerade 23 januari 2015

En formell beskrivning av ett funktionellt språk som påminner väldigt mycket om Erlang. Vi bygger upp det från grunden för att förstå vilka egenskaper språket har och vid vilka tillfällen vi har ett val att göra som bestämmer hur vårt språk skall definieras.

Innan föreläsningen skall ni ha kommit igång med Erlang så at ni kan börja experimentera med dess topp-loop och skriva mycket enkla funktioner.  Ni skall ha läst igenom kapitel 1 och 2 i kursboken.


* evaluation.pdf 
* functions.pdf
Observera att föreläsningen inte går igenom Erlang från en praktiskt aspekt, den kunskapen får ni från kursboken. 

Efter föreläsningen Ta och börja på den första inlämningsuppgiften - det gäller att starta i tid. Se till så att ni kommit så långt att övningstillfället nästa vecka blir väl utnyttjat för att få till de sista pusselbitarna.

För den vetgirige Den presentation som ges under föreläsningen kan tyckas vara formell och inkludera det mesta men vi har faktiskt utelämnat en del saker. För den som vill läsa lite mer om hur man kan definiera funktionella språk i termer av lambdakalkyl och se ge en operationell semantik till sitt språk kan titta på följande referenser:¶


* The Implementation of Functional Programming Languages, Simon L. Peyton Jones är en klassisk bok i sammanhanget. Man behöver inte läsa hela men man kan titta igenom de första kapitlen och se att väldigt mycket följer vårt angreppssätt. I boken ges ett apråk "Miranda" en beskrivning genom att det översätts till lambdakalkyl. Uttryck i lambdakalkylen ges sen en betydelse genom att översättas till operationer i en abstrakt maskin.  
* Simon Peyton Jones är väl värd att lyssna på, här ett framträdande på TEDx: Teaching Creative Computer Science.
Hur fuskade vi Jag nämnde att vi utelämnat en del saker och vi har faktiskt varit lite otydliga. I vår beskrivning av språket har vi egentligen inte govet en fullständig operationell semantik. Vi har varit lite yviga när vi sagt "den hör regeln får vi tillämpa om ..."  eller "först evaluerar vi det hör och sen ..". Om vi skulle gen en korrekt operationell semantik så skulle vi inte ha lämnat sådan luckor i beskrivningen. Det vi egentligen har gjort är att vi beskrivit vad som kallas en "denationell semantik". När vi sedna implementerar vår interpretator så måste vi ta ta i problem som i vilken ordning och exakt detta skall ske.¶

Johan Montelius redigerade 1 mars 2017

This is a formal description of a small functional language (that looks a bit like Erlang). We will build it from the ground up, starting with the basic data structures and then define how expressions are evaluated. Even if the language is very small we will have some points in the design were we need to do a choice; depending on our choices our language will have different properties. 

Before this lecture you should be up and running in Erlang to the level that you can run small tests in the Erlang shell. You should also have read chapter 1 and 2 in the course book.


* evaluation.pdf 
* functions.pdf
Note - again, the lectures will not describe how to work with Erlang and the programming environment, this is something that you should learn by reading the course book and following the online material.

The operational semantics We use a simplified functional programming language to describe properties of different alternatives. I've summarised the lectures that presents the operational semantics (it's not following the slides exactly so don't be confused).


* operational.pdf 
Before the lecture You should have an Erlang system up and running and should have started to write smaller functions. You should have seen the Erlang Express lectures on:


* Erlang Data Types
* Variables and Pattern Matching
After the lecture Start with the first assignment. Make sure that you start early so that you can make best use of the scheduled hours where teaching assistants will help you.

Go through the next lecture in Erlang Express:


* Functions and Modules
* The Erlang Shell
* The Erlang Shell in Practice
Going further In this very limited description we have omitted a few things. If you want to know more how functional programming languages are defined you can look at the following two references:


* The Implementation of Functional Programming Languages by Simon L. Peyton Jones. This is the classical book in the area. You don't have to read the whole book but do take a look at the first set of chapters. You will see how the approach is very close to how we have worked. In the book a functional programming language, Miranda, is defined in terms of lambda calculus. Lambda expressions are then given an operational semantics by being expressed as abstract machine instructions.
* Teaching Creative Computer Science , Simon Peyton Jones at TEDx: 
How did we cheat? We have done some hand waving in our description. It's not a complete operational semantics since we are a bit informal when we say things like "this rule is applied if...". In a proper description we would have to describe exactly how we find out if a rule is to be applied. We would for sure have to introduce a computational stack in order to evaluate sub-expressions etc.  If we would define a complete operational semantic we would not leave this undefined.If we do not have a precise operational semantics then how can we say anything about the run-time complexity of programs.

Nor have we described how functions should be represented or how higher order functions should work but this will actually be only smaller extensions to the given description.