# lambda

###### 7/8/21

DRAFT

### Let polymorphism

We would like to have polymorphism in certain circumstances. For example, we would like to have the same identity function λx:x that could be used on Booleans and Integers, without having to have two separate identity functions, one of type B->B and the other of type I->I .

The usual way to do this, in this setting, is via a 'let' construction. Most functional programming languages have an expression form similar to

###### 7/8/21

### Introduction

We wish to extend what we have beyond STLC to what is sometimes called a Mini-ML type system. Clarity will be needed here. Imagine for one moment the lambda calculus without types. The well formed expressions or formulas all have values. The word for this is that they are '**terms**'. They may or may not have a normal form, a terminating reduction etc., but they are terms. If types are added, they are to provide a '**type**' for the individual terms. They do not affect the values the terms have.

###### 1/28/2020

###### 1/24/2020

###### 5/5/21

## Introduction

The Lambda Calculus that we have been looking at thus far has been the *untyped* Lambda Calculus. It is plenty interesting for sure, being able to provide a foundation for computability, programming languages, and many areas of linguistics and philosophy. But untyped Lambda calculus also has some features to be wary of; for example, some reduction sequences go on forever and never reduce the expression to a normal form.

###### 1/25/2020

Example

#### Alpha conversion (Rewrite of bound variables):-

Any abstraction λ<variable1>.<expr> can be converted to λ<variable2>.<expr>/.<variable1> -><variable2> provided the substitution <expr> /. <variable1> -> <variable2> is sound.

Example

2013

#### Alpha conversion (Rewrite of bound variables):-

Any abstraction λ<variable1>.<expr> can be converted to λ<variable2>.<expr>/.<variable1> -><variable2> provided the substitution <expr> /. <variable1> -> <variable2> is sound.

###### 9/18/19

You can try your own exercises here. Type in, or edit, in the lower panel then select and press 'Start from selection'.

10 Software

Now we can attempt to write a recursive function. Let us try for a length of list function. Something like

length(list) = df. If (list is empty) then 0 else succ(length(tail(list)))

we can do all this with the materials we have apart from the fact that the name 'length' appears in the body of the function and in lambda calculus there are no names.

This obstacle is overcome by what is known as a fix-point combinator (and the next little piece is something with intellectual content).