Next:
Notation used in Conversion
Up:
The Lambda Calculus
Previous:
Syntax of Lambda Expressions
Contents
Start
Basic Rules for Lambda Conversions
Subsections
Notation used in Conversion Rules
Notation used to specify conversion of lambda expressions
Notation used to specifiy substitution
Alpha Conversion
Bound and Free Variables
Rules of Alpha Conversion
Beta Conversion
Rule of
-Conversion
-Reduction
Reducible Expression `redex'
Rule of
-Reduction
-Abstraction
Rule of
-Abstraction
Examples:
Remark:
Eta Conversion
-Reduction
-Abstraction
Rules of Associativity
Rule of Associativity for Abstraction
Example:
Rule of Associativity for Application
Example:
Example for both rules:
Y-Combinator
Definition
Basic Usage of Y-Combinator
Fixpoint of a Function
Generation of fixpoint using Y-combinator
Fixpoint expansion by
-reduction
Using the Y-Combinator to implement recursion
Introduction
Steps to Eliminate Implicit Recursion
Example of Step by Step Evaluation
Georg P. Loczewski 2004-03-05
Impressum und Datenschutz
-Conversion
-Reduction
-reduction