lambda

Let Polymorphism and a Mini ML Type System II martin Mon, 06/28/2021 - 19:58
Topic
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

Let Polymorphism and a Mini-ML type system I martin Thu, 05/20/2021 - 16:36
Topic
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.

Normal Order Reductions in Simply Typed Lambda Calculus Widget martin Tue, 01/28/2020 - 12:39
Topic
1/28/2020

The Lambda Verbose Parse Widget martin Sun, 01/26/2020 - 13:20
Topic
1/24/2020

Simply Typed Lambda Calculus martin Tue, 09/24/2019 - 11:45
Topic
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.

The Lambda Reduction Widget martin Sat, 03/02/2013 - 14:29
Topic
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.

Lambda Applet martin Sat, 03/02/2013 - 14:22
Topic

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.

Roll your own [Lambda Calculus] martin Sat, 02/16/2013 - 22:59
Topic
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'.

Supplement martin Sat, 02/16/2013 - 13:37
Topic
Combinators III: Recursion and the Fixpoint Combinator (alternate using Java applets martin Fri, 02/15/2013 - 17:06
Topic

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).