This is not a Wikipedia article: It is an individual user's work-in-progress page, and may be incomplete and/or unreliable. For guidance on developing this draft, see Wikipedia:So you made a userspace draft.  Find sources:  Google ( books · news · scholar · free images · WP refs) · FENS · JSTOR · TWL Easy tools: Citation bot ( help) | Advanced: Fix bare URLs This page was last edited by Cydebot ( talk | contribs) 5 years ago. ( Update timer) Finished writing a draft article? Are you ready to request an experienced editor review it for possible inclusion in Wikipedia?     Submit your draft for review!

The let-set calculus is a variant of the lambda calculus where two reserved words are defined: let and set. Any other word can be used as a variable. The terms are built from let, set and variables from application.

Reserved words and substitution metaoperation

Let

let is a function taking three arguments, A, B and C, that returns (Ax := C) (Bx := C).

Set

set is a function taking three arguments, A, B and C, that returns (CA := B)

Substitution metaoperation

The substitution metaoperation is similar to the β-reduction in the lambda calculus and is represented as termvar := value.

1. (A B)var := value → (Avar := value B var := value)
2. varvar := value → value
3. othervarvar := value → othervar
4. (let A B)x := value → let A B
5. let[var := value → let
6. set[var := value → set

Converting lambda terms to let-set

The algorithm has two steps: lambda cleanup and abstraction elimination.

Lambda cleanup

x is used as a special name in let, so it cannot appear in the lambda term. For that, α-conversion should be used.

Abstraction elimination

Abstraction elimination is defined as a metaoperation T[term] with a helper metaoperation C[var, term]

1. T[(t1 t2)] → T[t1] T[t2]
2. T[λv.E] → let (set v x) T[E]
3. T[λv.λu.E] → T[λv.T[λu.E]]
4. T[E] → E (if E has no abstractions)

A practical example

The term (λy.λf.f y) in let-set calculus is (let (set y x) (let (set f x) (f y))).

• T[λy.λf.f y]
• T[λy.T[λf.f y]] (by rule 3)
• T[λy.let (set f x) T[f y]] (by rule 2)
• T[λy.let (set f x) (f y)] (by rule 4)
• let (set y x) T[let (set f x) (f y)] (by rule 2)
• let (set y x) (let (set f x) (f y)) (by rule 4)

When this term is applied to two terms A and B (substitutions done in one step):

• let (set y x) (let (set f x) (f y)) A B
• set y A (let (set f x) (f y)) B
• let (set f x) (f A) B
• set f B (f A)
• (B A)

The Y combinator

The Y combinator transforms into let (set f x) ((let (set g x) (g g)) (let (set s x) (f (s s)))).

When applied to a function F:

• let (set f x) ((let (set g x) (g g)) (let (set s x) (f (s s)))) F
• set f F ((let (set g x) (g g)) (let (set s x) (f (s s))))
• let (set g x) (g g) (let (set s x) (F (s s)))
• set g (let (set s x) (F (s s))) (g g)
• let (set s x) (F (s s)) (let (set s x) (F (s s))) [reduced form of (Y F)]
• set s (let (set s x) (F (s s))) (let (set s x) (F (s s)))
• F (let (set s x) (F (s s)) (let (set s x) (F (s s)))) [equals F(Y F), therefore proving the equality]

References

External links