232 lines
12 KiB
Markdown
232 lines
12 KiB
Markdown
---
|
|
title: λ-Calculus
|
|
TARGET DECK: Obsidian::STEM
|
|
FILE TAGS: λ-calculus
|
|
tags:
|
|
- λ-calculus
|
|
---
|
|
|
|
## Overview
|
|
|
|
Assume that there is given an infinite sequence of expressions called **variables** and a finite or infinite sequence of expressions called **atomic constants**, different from the variables. The set of expressions called $\lambda$-terms is defined inductively as follows:
|
|
|
|
* all variables and atomic constants are $\lambda$-terms (called **atoms**)
|
|
* if $M$ and $N$ are $\lambda$-terms, then $(MN)$ is a $\lambda$-term (called **application**)
|
|
* if $M$ is a $\lambda$-term and $x$ is a variable, then $(\lambda x. M)$ is a $\lambda$-term (called **abstraction**)
|
|
|
|
If the sequence of atomic constants is empty, the system is called **pure**. Otherwise it is called **applied**.
|
|
|
|
%%ANKI
|
|
Basic
|
|
What does a "higher-order function" refer to?
|
|
Back: A function that acts on other functions.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526287-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
How is $f(x) = x - y$ written using $\lambda$-calculus?
|
|
Back: $\lambda x. x - y$
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526290-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
How is $f(x, y) = x - y$ written using (uncurried) $\lambda$-calculus?
|
|
Back: $\lambda x y. x - y$
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526293-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
How do you curry expression $\lambda x y. x - y$?
|
|
Back: $\lambda x. \lambda y. x - y$
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526297-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
How do you uncurry expression $\lambda x. \lambda y. x - y$?
|
|
Back: $\lambda x y. x - y$
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526300-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
What does $(\lambda x. x - y)(0)$ evaluate to?
|
|
Back: $0 - y$
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526303-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
How many variables exist in a $\lambda$-calculus formal system?
|
|
Back: An infinite number.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526306-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
How many atomic constants exist in a $\lambda$-calculus formal system?
|
|
Back: Zero or more.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526309-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
What distinguishes variables and atomic constants?
|
|
Back: The latter is meant to refer to constants outside the formal system.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526312-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
What two classes of expressions does an "atom" potentially refer to?
|
|
Back: Variables and atomic constants.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526316-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
What general term describes both variables and atomic constants?
|
|
Back: Atoms.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526319-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
Why are variables and atomic constants called "atoms"?
|
|
Back: They are not composed of smaller $\lambda$-terms.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526322-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
When is a $\lambda$-calculus considered pure?
|
|
Back: When there exist no atomic constants in the system.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526325-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
When is a $\lambda$-calculus considered applied?
|
|
Back: When there exists at least one atomic constant in the system.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526328-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Cloze
|
|
A $\lambda$-calculus is either {pure} or {applied}.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526331-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
What term refers to the base case of the $\lambda$-term definition?
|
|
Back: The atoms.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526334-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
What term refers to the inductive cases of the $\lambda$-term definition?
|
|
Back: Application and abstraction.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526337-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Cloze
|
|
Given $\lambda$-terms $M$ and $N$, {$(MN)$} is referred to as {application}.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526340-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Cloze
|
|
Given $\lambda$-term $M$ and variable $x$, {$(\lambda x. M)$} is referred to as {abstraction}.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526343-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
Consider term $(\lambda x. x)(0)$. Is our $\lambda$-calculus pure or applied?
|
|
Back: Applied.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526346-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
Consider term $(\lambda x. x)(y)$. Is our $\lambda$-calculus pure or applied?
|
|
Back: Indeterminate.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526349-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
What three terms categorize all $\lambda$-terms?
|
|
Back: Atoms, applications, and abstractions.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716494526352-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
How is a constant function returning $y$ denoted in $\lambda$-calculus?
|
|
Back: $\lambda x. y$
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716498992500-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
How is expression $MNPQ$ written with parentheses reintroduced?
|
|
Back: $(((MN)P)Q)$
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716498992520-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Cloze
|
|
By convention, parentheses in $\lambda$-calculus are {left}-associative.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716498992525-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Basic
|
|
How is expression $\lambda x. \lambda y. MN$ written with parentheses reintroduced?
|
|
Back: $(\lambda x. (\lambda y. (MN)))$
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716498992530-->
|
|
END%%
|
|
|
|
%%ANKI
|
|
Cloze
|
|
Expression $(MN)$ is interpreted as applying {$M$} to {$N$}.
|
|
Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
|
|
<!--ID: 1716498992534-->
|
|
END%%
|
|
|
|
## Bibliography
|
|
|
|
* Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf). |