|
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127 |
- # An Idiot's Guide to Lambda Calculus
-
- clarification: this is not a guide to lambda calculus for idiots, this is a guide to lambda calculus written by an idiot.
-
- imagine for a second you need to explain our numbering system without ***any*** background. any at all, think about that for a second.
-
- * you have no idea what the number symbols mean
- * you have no idea what plus minus or anything mean
- * you have no idea of anything
-
- and this isn't limited to just numbering, because almost anything we do on a computer is based around maths, imagine the same for pretty much literally anything.
-
- what you would need is....
-
- **is**...
-
- ***is***...
-
- ## a way to describe computability
-
- and one way of doing that is with lambda calculus. to define lambda calculus we need just a few rules - variables, abstraction, application.
-
- these concepts aren't too difficult, so awayyyy we go.
-
- ### variables
-
- variables are simply a name, most of the time we use letters. there are two catches here, if you're used to variables in maths or other languages:
-
- * unlike pretty much every other language, lambda calc variables don't have a value, only a name. this is because we don't have any concept of what a value is.
-
- * unlike any language worth using, variables in lambda calculus do not have a *type*. again this is because we don't have a concept of what type is.
-
- this guide is gonna use lowercase letters for the most part, so the examples are `a b c d e f` etc etc
-
- ### abstraction
-
- abstractions are the functions of lambda calc, and take the form off:
-
- ```
- (λx.M)
- ```
-
- where `λ` denotes that this is a function
- `x` is an argument name (that is local to this function)
- and `M` is a list of variables that will form the function body
-
- a quick example of an abstraction is the identity function:
-
- ```
- (λx.x)
- ```
-
- we'll get onto more to do with fuctions in a bit, but next
-
- ### application
-
- application is what we pretentious people call "actually using a function" and it takes the form of:
-
- ```
- (M N)
- ```
-
- where `M` is an abstraction, and `N` is any lambda term at all. i will refer to `M` as an abstraction and `N` as the application body
-
- to do the application we just use `N` as the argument for `M`, and then do a find and replace based on the abstraction definition.
-
- for example, lets do an easy one using the identity function, which is a function that returns its input unchanged:
-
- if we have the abstraction `(λx.x)` and the variable `y` to use for the application, and then lay the application out as so:
-
- ```
- ( (λx.x) y )
- ```
-
- we can then begin applying.
-
- the identity function has `x` as its argument, so we take the application body, in this case `y`, and every time we see `x` in the abstraction body (the bit past `.`) we replace it with our argument, `y`.
-
- so our abstraction body is `x`, and `x` is equal to our argument `y`, so therefore our function will return `y`, which is the identity.
-
- a sligtly more interesting example is something like:
-
- ```
- ( (λx.xx) y )
- ```
-
- here, our argument to our abstraction is `y`, which gets bound to `x` in the abstraction body, which is then fed into the `xx` to produce:
-
- `yy`
-
- and thats how we go.
-
- as a spoiler for what the next lambda calc post will cover, heres a bit of an example, imagine we were using the same abstraction:
-
- ```
- (λx.xx)
- ```
-
- and instead of passing it `y`, we passed it **another abstraction**... say, itself?
-
- ```
- ( (λx.xx) (λx.xx) )
- ```
-
- here, we bind the entire abstraction `(λx.xx)` to the variable `x` in the first abstraction.
-
- when we do the substitution into the body `xx` we get left with...
-
- ```
- ( (λx.xx) (λx.xx) )
- ```
-
- the same thing, which means this is an ***infinite loop***
-
- fun stuff fun stuff imo
-
- ## further thoughts
-
- theres a lot more to go before we get to a numbering system, and at this point it may seem like theres not much use to lambda calculus, but i am not joking when i say ***anything that can be done on a computer can be written in lambda calculus***.
-
- it may be abstracted, it may be thousands of millions of pages long, but it is possible.
-
- and thats what makes it so wonderful.
-
- i'll write more in depth on this at some point in the near future when i'm feeling smarter, less lazy, and don't wanna write edgy armchair psych pieces instead.
-
- peace out ny'all, if you're unlucky i'll talk about Nock after this.
|