lambda

Lambda Calculus with Elementary Type Theory martin Mon, 08/23/2021 - 11:24
Topic
8/23/21

The Lambda Calculus  that we have been looking at in Lambda Calculus and Combinatory Logic  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.

Let Polymorphism in Mini ML martin Mon, 06/28/2021 - 19:58
Topic
9/2/21

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 martin Thu, 05/20/2021 - 16:36
Topic
8/29/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

Polymorphism, Annotation, and Decidable Type Inference martin Fri, 11/29/2019 - 17:46
Topic
7/8/21

[In this section, we will sometimes use annotated abstractions, and sometimes use unannotated abstractions. This is just to be flexible in discussing their respective merits.]

There certainly is an unusual feature possessed by the annotated STLC that we have thus far. Consider two abstractions with annotations

λx:I.x

and

λx:B.x

Simply Typed Lambda Calculus martin Tue, 09/24/2019 - 11:45
Topic
8/23/21

Types and Values

Types are collections or sets of values. For our purposes, to produce an illustrative example, we can get by with just two basic Types, one with a finite number of values, and the other with an infinite number of values. 

The Type Boolean, or Bool, or just 'B' is a type with the two values: True, and False.

The Type Integer, or Int, or just 'I', is a type with the values 0,1,2,3... etc

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