lain.church gopherhole repo. automatically pushed to by rf
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

128 lines
4.2KB

  1. # An Idiot's Guide to Lambda Calculus
  2. clarification: this is not a guide to lambda calculus for idiots, this is a guide to lambda calculus written by an idiot.
  3. imagine for a second you need to explain our numbering system without ***any*** background. any at all, think about that for a second.
  4. * you have no idea what the number symbols mean
  5. * you have no idea what plus minus or anything mean
  6. * you have no idea of anything
  7. 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.
  8. what you would need is....
  9. **is**...
  10. ***is***...
  11. ## a way to describe computability
  12. and one way of doing that is with lambda calculus. to define lambda calculus we need just a few rules - variables, abstraction, application.
  13. these concepts aren't too difficult, so awayyyy we go.
  14. ### variables
  15. 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:
  16. * 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.
  17. * 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.
  18. this guide is gonna use lowercase letters for the most part, so the examples are `a b c d e f` etc etc
  19. ### abstraction
  20. abstractions are the functions of lambda calc, and take the form off:
  21. ```
  22. (λx.M)
  23. ```
  24. where `λ` denotes that this is a function
  25. `x` is an argument name (that is local to this function)
  26. and `M` is a list of variables that will form the function body
  27. a quick example of an abstraction is the identity function:
  28. ```
  29. (λx.x)
  30. ```
  31. we'll get onto more to do with fuctions in a bit, but next
  32. ### application
  33. application is what we pretentious people call "actually using a function" and it takes the form of:
  34. ```
  35. (M N)
  36. ```
  37. 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
  38. 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.
  39. for example, lets do an easy one using the identity function, which is a function that returns its input unchanged:
  40. if we have the abstraction `(λx.x)` and the variable `y` to use for the application, and then lay the application out as so:
  41. ```
  42. ( (λx.x) y )
  43. ```
  44. we can then begin applying.
  45. 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`.
  46. 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.
  47. a sligtly more interesting example is something like:
  48. ```
  49. ( (λx.xx) y )
  50. ```
  51. 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:
  52. `yy`
  53. and thats how we go.
  54. 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:
  55. ```
  56. (λx.xx)
  57. ```
  58. and instead of passing it `y`, we passed it **another abstraction**... say, itself?
  59. ```
  60. ( (λx.xx) (λx.xx) )
  61. ```
  62. here, we bind the entire abstraction `(λx.xx)` to the variable `x` in the first abstraction.
  63. when we do the substitution into the body `xx` we get left with...
  64. ```
  65. ( (λx.xx) (λx.xx) )
  66. ```
  67. the same thing, which means this is an ***infinite loop***
  68. fun stuff fun stuff imo
  69. ## further thoughts
  70. 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***.
  71. it may be abstracted, it may be thousands of millions of pages long, but it is possible.
  72. and thats what makes it so wonderful.
  73. 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.
  74. peace out ny'all, if you're unlucky i'll talk about Nock after this.