The phrase "we know it's correct because it type checks" has blown my mind. I must learn more about Curry-Howard correspondence now

@tylerfusco7495

13 күн бұрын

if you want to go really far into it, look into languages with this taken to the logical extreme, like Lean4. people have written a huge amount of math as code, and *the fact that it type checks* means that all of those proofs are correct.

@warmooze

13 күн бұрын

Absolutely insane

@MrSamwise25

13 күн бұрын

Just a warning: the treatments I've seen of the CH correspondence (e.g. Girard's Proofs and Types) have either been frustrating in key technical points or too vague to get a deep understanding. This isn't to dissuade you, but to reassure you that it isn't you, it's the text.

@MrSamwise25

13 күн бұрын

What's your favorite first-order logic system? Mine is Fitch-style proofs, and I found it easier to just go through the correspondence myself with that system.

@jawad9757

13 күн бұрын

wait until you hear about dependently typed programming languages

This video is super good. Multiple times throughout the video, I was like "ok this does not make any sense" and then immediately after saying that, you said "That seems confusing. Let's look at an example."

@Eyesomorphic

5 күн бұрын

That's very reassuring, I'm glad you enjoyed it :)

Wait, this was released 10 days ago? I swear I come back to watch this every 6 months

as someone who loves both maths and programming, this is probably my favourite math video I've ever seen

@sadsongs7731

13 күн бұрын

I mean, to claim that Lambda calculus can replace any programming language is like saying assembly can replace any programming language. True in theory but GOOD LUCK trying to get anywhere.

@tylerfusco7495

13 күн бұрын

@@sadsongs7731 i mean, thats literally what functional programming languages are. Lisp, Haskell, OCaML, Lean, Clojure, etc. Are all pretty widely used, and are literally built on top of nothing but lambda calculus (but in practice are optimized or compiled to speed up evaluation).

@sadsongs7731

13 күн бұрын

@@tylerfusco7495 Those languages offer far more conveniences than what lambda calculus notation provides. They may be "built on top of" but they are not just lambda calculus. That was my point with assembly. You technically don't need anything else, but it's a pain in the behind to write compared to a higher level programming language. These languages offer abstractions that take time to learn and, sure, would be better if you didn't have to learn them but they are there because raw lambda, like raw assembly, is not user friendly.

@tylerfusco7495

13 күн бұрын

@@sadsongs7731 well yeah, nobody is advocating for lambda calculus being the actual thing you program in. that's like thinking a video outlining how assembly language works is advocating for assembly language to replace higher level languages. that's not the point, the point is that the higher level abstractions can all be built on top of and formalized using the lower level ones.

@Darkon10199

12 күн бұрын

if you love both math and cs i really recommend type theory. it's the math field that studies this stuff, lambda calculus is the starting point, but it's some of the most beautiful and groundbraking math i've ever studied

One of the things I took away from reading _Gödel, Escher, Bach_ (mumble, mumble) years ago was that computer languages don't differ in their _ability_ only in their _expressiveness_ . In other words, any language (of at least λ-calculus complexity) can do what any other language can. It's just easier to express in some.

@anywallsocket

13 күн бұрын

Yeah cuz λ calc is Turing complete, so it’s complexity is sufficient to simulate any normal computation, including the simulation of any other computer.

@writerightmathnation9481

13 күн бұрын

Complexity is not the same as effectiveness. Some languages are faster because of their expressiveness, and others are slower because of the design of their use of their expressive power.

@anywallsocket

13 күн бұрын

@@writerightmathnation9481 i believe that was OP's point, you just said it differently. no one is saying complexity == effectiveness

@SL3DApps

13 күн бұрын

This isn’t true. A language ability is highly different when used for certain areas in computing. However, If you’re only interested in making simple programs then you won’t ever have to worry.

@cinderwolf32

13 күн бұрын

​@@SL3DApps things like I/O, direct memory access, network access, etc don't count here. This video, and the comment you're replying to, are about computation, not making programs and apps. Computation does not care about these things, and studying it takes place in an imaginary world with infinite memory and infinite time. In that case, Scratch and C are equivalent. If you're seriously unconvinced, consider that someone has successfully emulated a RISC machine in Scratch and used it to boot Linux all within the project.

This video is amazing! I encourage everyone to watch the video, and then grab a pen and paper and rewatch the video, trying to get ahead of what is being shown. I tried that and realized that I hadn’t actually understood many of the things in the video, like the notation. Videos like these are so well explained that you often feel like you understood everything. But then when you grab pen and paper you realize that there’s many details that you missed. And by the end of it, you feel like you truly understood 90% of it

halfway through the video I suddenly understood Haskell

@ckpioo

23 сағат бұрын

💀💀

@ckpioo

23 сағат бұрын

haskell mentioned

Lambda Calculus seems like the Functional version of a Turing Machine. Very interesting.

@Eyesomorphic

14 күн бұрын

They are computationally equivalent, so you can actually encode a Turing Machine in the lambda calculus, and vice versa! This also means that there is a lambda calculus equivalent of a Universal Turing Machine, so you can build terms in the lambda calculus that act as an interpreter to run terms in the lambda calculus!

@anywallsocket

13 күн бұрын

Bro watched the video 😂

@scottcarothers837

13 күн бұрын

@@Eyesomorphicwell, yeah, of course they’re equivalent. lamba calculus is turing complete.

@zTJq40sl

13 күн бұрын

​@@Eyesomorphic It's even relatively simple: If we encode the variable x as λ a b c . a x the application M N as λ a b c . b [encoding of term M] [encoding of term N] the lambda abstraction λ x . M as λ a b c . c (λ x . [encoding of M]) then an interpreter for the such-encoded lambda terms is "just" E = Y λ e m . m (λ x . x) (λ m n . (e m) (e n)) (λm v . e (m v)) where (as seen at 12:28) Y = λ f . (λ x . f (x x)) (λ x . f (x x)) (I'm using here "λ x y z . M" as a shorthand for "λ x . λ y . λ z . M", as usual once we've seen that we can emulate multi-argument functions by currying.) So yeah, if just looking at these lambda terms, they might seem rather unwieldy. But considering that they implement a fully self-hosting interpreter for a turing-complete language, they are rather tame. (And all the a b c-dot-something stuff is just for marking the encoded terms as (a) variable, (b) application or (c) abstraction, so that the interpreter can handle them accordingly.)

@BC2300-NewStart

13 күн бұрын

Yeah, there's this thing called the church Turing thesis thay was only found cuz church and Turing realized that their attempts at defining computability were basically equal fr

Years of fp propaganda from my friends; And it is this video that finally convinces me it is in fact worth the effort

@Eyesomorphic

10 күн бұрын

That is quite the compliment, thank you!

And if you've ever had the privilege of writing Haskell code, it uses the same kind of type checker using an algorithm developed by Milner and Hindley to prove that your program is 100% type-safe, which actually means that if your code compiles, there's a decent chance it's correct. And if it's not, then your toe definitions aren't robust enough.

@asdf-mu8zi

10 күн бұрын

> partial function joins the game

so what your saying is i can write every single python program in one line

@neutillius

11 күн бұрын

But It ld be a very long one. Like classical literature sentences for pages.

@natebrown2805

7 күн бұрын

exec("print('hello') print('world')")

@TrusePkay

6 күн бұрын

Try languages like F# and Scala. You will see how 3 lines of Scala will dwarf 15 lines of Java

I’m a linguist, not particularly mathematically inclined, and honestly, I can’t believe I understood half of it. Incredibly simple yet intuitive. I love the visuals too! Please keep up the good work! :))

Alice is so obsessed with Java.

@mythacker4365

5 күн бұрын

😂😂😂😂

7:30 "This method...is named currying after the magician Haskell Curry." I'm sure advanced mathematics seems to be magic to some people.

@houstonbova3136

13 күн бұрын

I thought he said Logician.

@maximumhamster

13 күн бұрын

I heard the same thing, but it was due to listening on 2x speed. When I put it back to the 1x speed I could hear Logician.

@BonktYT

13 күн бұрын

get off your high horse

@angeldude101

13 күн бұрын

I heard "magician" and I was playing at 1x speed _and_ had captions turned on that said "logician."

@lemoneer7474

13 күн бұрын

What’s funny is that this isn’t even the first time I’ve misheard logician as magician.

As a computer science student that studied functional programming and mathematics, I absolutely love this video. Please keep going!

This is why i pay for internet. Thank you very much. I did not pay much attention in class , but if the class was explained like this it would have been awesome.

11:00 - "there aren't any y in M" If only Coq would accept this as a proof every time this one detail comes up...

@user-qm4ev6jb7d

13 күн бұрын

Are you using de Brujin indices? If so, when substituting M into x, the last thing you do to M is increase all indices by 1, which means there aren't any zeroes there, right?

@shadamethyst1258

13 күн бұрын

@@user-qm4ev6jb7d That's the solution that the class I followed quickly led us to, yeah. But for a bit, we would work with call by value without de bruijn indices, and propagating substitutions across lambdas was a pain

Great timing! I've always wanted to share this with my friends but I find it extremely hard to explain. It's nice that you made it accessible to others without much experience in math.

@Eyesomorphic

14 күн бұрын

Glad it was helpful!

@scroipt

13 күн бұрын

Though this really is more of a "hey this seems to work out" kind of proof than a particularly rigorous one.

You summed up most of the Theory of Computation, Complexity and Logic course that I attended at university. Kudos to you Eyesomorphic! 👏🏼

Wow! Definitely a must watch!

that's nice, now print "hello world"

@angeldude101

13 күн бұрын

Hmm... that might be challenging... Would you accept just returning a string containing the characters for "hello world". In typed lambda calculus: "hello world" In untyped lambda calculus: (would need to define cons cells to form a linked list and store in that list the Church-encoded Peano numbers corresponding to the ASCII/Unicode codepoints of each character)

@AnarchoAmericium

13 күн бұрын

(λx:String.x)("hello world")

@gregoryfenn1462

13 күн бұрын

No, returning a string or data object isn't what the OP wants, they want the program to literally write to our stdout console. It's the most basic task in any new programming language, so how is that done in lamda calculus?

@angeldude101

13 күн бұрын

@@gregoryfenn1462 For a more serious answer, one possibility would be to evaluate to a function whose argument is a hypothetical print "function", and then call that "function" with "hello world". Lambda Calculus can perform any _pure_ computation, but it doesn't inherently have any access to any host environment. Technically, if you stripped C of external libraries (including libc) and inline assembly, you would be just as incapable of "printing" to a "screen" as you would be in pure Lambda Calculus. Same as if you tried to write Brainfuck without the . and , commands.

@nikolaygruychev2504

12 күн бұрын

consider a "standard library" - your program must be a function, not an application, and it accepts a pair list of all input. it can also emit a pair list itself, to represent the output. funnily, pairs can be used as sort-of-iterators, given that cons = \x. \y. \f. f x y; car = \p. p (\x.\y. x) ; cdr = \p. p (\x.\y. y), then we can have a lazyCons = \x.\f.\g. g x (lazyCons (f x) f) [google y combinator recursion], meaning that lazyCons 1 (\x. x + 1) gives us a list of all natural numbers, i.e. enumFrom 1 in haskell. with this, we can theoretically process any input stream, do computation with it, and emit output partially while the computation is going on much the same way a regular turing machine can. lambda calculus was not intended as proof math can be a programming language, but that machines can do math or something, idk im not a computer scientist

Those pauses you make are key. Great job!!!

What a lovely video. This nicely clarified a few concepts I'd encountered in passing but had not unpacked yet. Thanks for this.

@Eyesomorphic

15 сағат бұрын

That's very kind 🤠

I knew about your channel since I watched the videos about category theory. I don't know how i didnt subscribe this channel. This video popped up and i was amazed by it. It's so wonderful in all sense. I watched this and saw that I hadn't subscribed to this channel.

Wow, this was so intuitively explained. Excellent!

I'm so glad I find your channel man.

Can't believe it took me this video to understand Python's lambda function 😭 thx for this video! ☺️☺️☺️💖

This reminds me of that MIT video from '86 talking about the eval / apply loop at the core of Lisp.

@dw3yn693

11 күн бұрын

you've got a link?

@jackren295

11 күн бұрын

@@dw3yn693 I think it's this series, which is a classic: kzread.info/dash/bejne/X36T2q5tearOeqQ.html

@chrisray9653

8 күн бұрын

@@dw3yn693 It's called Structure and Interpretation of Computer Programs (SICP MIT by Abelson and Sussman)

@nythrox3047

8 күн бұрын

What's the name

Thank you soo much. I found programming languages super difficult but this, this is so simple and easy to understand.

Very good introductory content, from lambda calculus to types and the CH correspondence

We need more channels like this. Great Computer Science content mate!! Instant subscribe 🙏🏼

Thank you for the great introduction.

Awesome video :-) Formalized mathematics is the future! A proof of Fermat's Last Theorem in LEAN is being currently worked on by professor Kevin Buzzard and the lean community!

Very nice video. I would have added a hint as to why java is not more powerful than lambda calculus: we can write a java interpreter in lambda calculus. Thus any computation of a java program can be be performed by a lambda term.

@56independent42

13 күн бұрын

How does one then interact with the OS like most programming languages allow? How does one do the less abstract and more pragmatic "get me onto the internet" stuff? Whilst programming and lambda are equally powerful when considering closed systems where all the data is spoon-fed, in the real world of hardware and connections, one needs the interface with the real world.

@Matthew-by2xx

13 күн бұрын

@@56independent42There are functional languages like Haskell, you still very much so can.

@fredericmazoit1441

13 күн бұрын

@@56independent42 As with a processor, there are 2 kind of conputation: inputs/outputs and "real" computation. The structure of most programs can be reduced to while not finished: inputdata=input() data=computation(data) output(data) When we say that lambda calculus is as powerful as, say, java, we do not consider inputs/outputs.

@aioia3885

13 күн бұрын

you could also make a java interpreter in the lambda calculus. In fact, someone made a compiler from c to the lambda calculus

@56independent42

13 күн бұрын

@@Matthew-by2xx ah, i forgot i even tried to learn it once

Impressive video once again!

10/10, clear explanation, good examples, awesome balance of rigor and simplicity. And a conclusion that very much so made me wonder about lambda calculus! I was always too afraid to approach lambda calculus, but your video showed it to just be python! Thanks so much

@Eyesomorphic

13 күн бұрын

That's very encouraging, thanks for the kind words

I was expecting some haskell propaganda, but its actually for proof-assistants, great to hear about that!

This video reminds me of my F# days. The real fundamental property of functional languages that separate them from mainstream imperative languages is that functional code has an immutable state. You cannot reassign values on the fly. And there are no nulls, although these are compensated with Option type systems. This makes functional languages not suitable for applications where states are important. Because the definition is clear, functional languages are short and free of bugs most of the time. They read code left to right. I was talking to a friend. He asked me how can a programming language be practically acceptable if it does not have procedures like if statements, loop statements, nulls, return keywords. I showed him how pattern matching, function composition, partial applications, generative sequences, and list comprehension, pattern work in F# and Scala, and you don't need to write verbose repetitive loops and branches. Just go straight to the point, and the program is ready. It's sad that functional programming is not mainstream or not even computing with the mainstream.

Fantastic! Thanks for sharing ❤

this channel is so underrated!

I thank you for this excellent introduction to lambda-calculus. Thanks for the video. 😀

@Eyesomorphic

11 күн бұрын

That means a lot, thank you :D

this is actually really easy to understand if your first programming language was functional

I was introduced to Alonzo Church’s lambda calculus paper when carrying out my a MSc. Course back in 1978. I don’t know how this popped up in my feed :)

1:45 Do not confuse this with multivariable equations that you can find the inverse of or isolate for a variable and determine properties given that alpha equivalence and alpha conversion capacity. If y = x^2 that doesn’t mean x = x^2 unless the “programming language” overwrites the interpretation to make them isomorphic. Because that’s what different glyphs holding the same value is doing.

This is so good! 😮

Wish someone made step-by-step explanaition of that simple lean proof with unfolding the stuff.

Wonderful video!

Thanks for the nice video again! It's very unfortunate that Coq wasn't mentioned here. :) For anyone interested in proof assistants, I recommend Software Foundations volume 1 for Coq, and mathematics in lean tutorial for Lean!

I was always curious about what a lamda function did. I did some digging around and eventually understood how it works on the programming side of things. So watching this verified my understanding to some extent and made me feel a little better knowing i'm not quite strong in math,lol.

Thank you!

Cool, will study later

Your intro is dope

@ 2:30 I like how this presented as some sort of obvious improvement over writing an arrow even though it's more visual noise and more characters.

Is definitely worth giving it a try.

Hearing Bob and Alice literally reminds me of GBG.

"Makes ANYTHING a comptuter can do", except for spell checking, apparently. :)

@Eyesomorphic

13 күн бұрын

That does seem to be the case 😭

This video is a treasure I always wanted to understand lambda calculus, this is so beautiful i actually almost cried

If you want to do another video about math that's the foundation for a lot of code I recommend the Relational Model by E. F. Codd. I'll admit that the first paper was not as rigorous as the Lambda Calculus, but it is Super fundamental to any relational database.

@NostraDavid2

11 күн бұрын

Oh, and use both 1969 (nice!) and 1970 papers!

Please do a video on Calculus of Constructions and encoding logic in it

Great video!

close enough welcome back haskell

20:45 - well there are some long elaborate proofs that could be found using LEAN but still you need to pass some time for it as many many of conjectures simply live over the basic axioms - as Turing proved himself.

As a software developer if I had to work on something like this I'd quit right away and find another career path. This is beautiful and helpful for mathematicians, a math scripting language but I'd place this as an extra module somewhere.. like a LaTex feature, python lambda notebook, a new Wolfram's suite scripting language, Matlab module or even as a small framework if I'm stretching a system too much so data scientists can be more comfortable performing in something more native to them... Anywhere where it can just be used for pure math. This is so hard to read and therefore will be so hard to maintain.

Bravo! I didn't think that the notion of higher order was special, but it was astounding that you could encode True and False. And "3", which seems to be three applications of any old function f. And recursion. And it seemed to me that the Curry-Howard correspondence could also itself be expressed in terms of the lambda calculus, as a proposition. Is there an end to this madness? It occured to me that, I myself might correspond to a kind of imperfect lambda machine, which begs the question, what machine? Where did the lambda notion of this representation of True and False come from? Is it possible to define a lamba expression/machine that comes up with hypotheses such as True and False, and is able to make and name things like Bool and "numbers"? I feel the answer to this imperfectly phrased question is False. But bravo again on this episode, I finally "get it", at the expense of going slightly mad. I just mention that I had to pause at several points, whereas on most other videos, I go at twice normal speed. Bravo!

Brilliant!

now i can finally declare that i understand calculus 😮

Good idea to replace that strange arrow, it is not on a regular keyboard. but but there is no lambda on my keyboard too!

Best sub ever

well, ifthen is just the identity function

@Eyesomorphic

13 күн бұрын

ifthen is indeed a rather boring function, the encoding of the booleans act as the conditionals so ifthen doesn't have to do too much. Interestingly enough, we can also encode ifthen as the literal identity function, \x.x, but I find it slightly less obvious as to why it works.

I recommend the talk "Lambda Calculus - Fundamentals of Lambda calculus & functional programming in Javascript" and follow along in the code examples - for anyone that wants to try this in practice and encode your own functions

This looks great and is very well explained, which software do you use for the slides ?

@Eyesomorphic

13 күн бұрын

I use Manim for the animated mathematics and pivot for the animated figures. Then I use da Vinci resolve to splice them all together :)

As type correspondences to proposition, when you have proposition type, its instance can be used as type again

I'd be interested to learn how the encodings would change if incorporating ternary/paraconsistent logic

and you could define the the ifthen as that (lambda:b.lambda:x.lambda:y.b x y) function

When you try to find a category corresponding to the untyped lambda calculus, and end up on rabbit hole journey trying to understand domain theory. Err- I mean... I would NEVER do that. /s

programming isin't complicated if you learn it the error when trying to print "Hello" is because you used the wrong brackets, to print hello world you use () instead of []

any book recommendations on lambda calculus / computation theory?

I have always been kind of comfortable with programming, but found it difficult to go into proofs and higher mathematics. But learning about this and LEAN is giving me hope. I am surely gonna check it out!

@Eyesomorphic

13 күн бұрын

That's great to hear, proof assistants can be daunting but I find them very rewarding!

Thanks for the video. A few questions/clarifications: what does Applications M M means at 4:10 , and it would have been helpful to explain how multiple inputs work: the most left input goes first and works on the most left lambda abstraction and so on. Because input goes where the variable is kinda obvious but other semantics of lambda calculus are not that clear

You can talk about logical programming next, like PROLOG.

Woah, I did not know!

Loved this video! If anyone is interested, I created an entire standard library with custom syntax that makes programming in pure lambda calculus easier: the "bruijn" programming language! I think some of you might enjoy it :)

The mother of LISP, Scala and Haskell

I've been trying to tell everyone about this for 10 years. I have a project which iterates through each possible algorithm.

since regular lambda calculus is untyped, you can give functions inputs that shouldn't work. for example, if you add 2 instances of church + using church +, you get another binary function f(x,y) = 2x + y

Imagine inventing any more programming languages after this

@vader567

9 күн бұрын

There is.. Its called Haskell

@TrusePkay

6 күн бұрын

There are many functional languages tho

This is why I love Haskell

Smooth.

functional programming stays winning

7:43 soooo much better than computerphile's vids on lambda-caic + haskell currying. since u took it slow, and from ground zero

Wait until you find out about the Haskell programming language

I can see how to win this year code obfuscated contest.

@not_herobrine3752

13 күн бұрын

devillish

This seems very similar to assembly language

I love this

13:53 ngl i woulda loved to see what happens when you replace the higher-order terms with the lambda-equivalents and let them resolve

Whyyy would we not stick with the arrow notation 😭😭

It might help if you point out how this is significantly different from the traditional notation using Polish notation: f(x).

now im starting to wonder what the "simplest" kind of tool equal to a turing machine is. im not sure if simple is the correct word here, but take a non-deterministic turing machine for an example. idk if its "simpler" than a regular turing machine, but it definitely achieves the same output with equally as many or less steps. and then again, simpler doesnt always mean easier

@electra_

13 күн бұрын

I think a decent candidate is the "find and replace" algorithm, where you just have a list of terms to find and replace, and you do them in order, and then repeat. So like if the replacements were A -> B, BB -> A, then you'd have like BABA (A -> B) BBBB (BB -> A) AA (A -> B) BB (BB -> A) A (A -> B) B To demonstrate this is Turing Complete, you can have a sequence of find and replaces that act primarily on the "head" of the tape, represented by its state. So if the states of the machine are A and B, and the data is 1s and 0s, a tape would look like 001001A001010 and a relevant find and replace operation for (When in state A, if 0 move to the left in state A, if 1 turn it into 0 and move to the right in state B) would be 0A0 -> A00 1A0 -> A10 A1 -> 0B Another similar one is having a list of resource exchanges to be done, something like Lose 10 As, add 3 Bs Lose 2 As and 2 Bs, add 1 C and you just try to do these exchanges in order if possible, with the higher ones having higher priority This ends up being turing complete if you have 7 resource types, and maybe less. The proof is more complicated than the previous one, the tape is represented by 3 resource types: L, C, R the count of L and R are binary numbers representing the tape, and C is the center (the one that's selected) so the tape 100(0)101 would be L = 4, C = 0, R = 5 note that least significant bit is always closest to the center theres also a temporary variable T and this is used for multiplication and division you can do something like 2R -> T T -> R to half or double things and this can be used to bit-shift but you need a control signal of some sort to make that work so there is SL, SR for the shift left and shift right so that'd be something like 5SR, R -> 5SR, T 5SR -> 4SR 4SR, T -> 4SR, 2R and having different values of SR required ensures that you always do the steps in order so to shift right you would multiply R by 2 move C to R divide L by 2, putting remainder in C then to control the state, you have S where the count of S is the state you're on and that would be something like S, C -> 3S, 5SR S -> 2S, C, 5SL so you can very easily determine the shift direction, next state, and next center value to reduce that to 4 types from 7, you can notice that C, SL, SR, and S all have a finite amount of states so you can just combine those into one state variable which encodes all of those state transitions L, R, and T represent infinitely long binary numbers and thus you can't do the same with them

@M_1024

13 күн бұрын

Here is a very simple turing complete system: start with a bitstring (input) and a "book" of bitstrings (instructions). Every iteration: 1. Remove the first bit from the main bitstring. 2. If it was a 1 append the contents of the current page of the book to the bitstring. 3. Flip to the next page in the book (or the first page if you are at the end). 4. Repeat.

@M_1024

13 күн бұрын

Another simple turing complete system: a programming launguage with 3 instructions: 1. Increase variables A and B by one. 2. Decrease A by one if its positive, otherwise jump to a specific point in the program 3. Same as above but for B. It can be made even simpler if you make it so that instructions 2 and 3 always jump the same amount K forward, and join the end of the program to its beggining. If K is large enough this will also be turing complete.

@cinderwolf32

13 күн бұрын

You should check on the Wikipedia page for single instruction set computers!

@tylerfusco7495

13 күн бұрын

I mean there's the SK combinator calculus, with just two terms and no variables, and there's also cellular autonomic rules that seem incredibly simple but are turing complete. It all depends on what your definition of "simple" is

Maybe this will let people understand why Haskell's Int -> Int -> Int is not as unreasonable as it looks

@maruseron

13 күн бұрын

it's still definitely unreasonable. one must remember the application order to parse "int -> int -> int", while "int (int, int)" (or the preferred modern (int, int): int) are very clear on intent. one can appreciate lambda calculus' power in spite of its simplicity without complicating oneself with syntax alien to daily life. we're not computers.

@oserodal2702

13 күн бұрын

​@@maruseronTBF, (ordered) tuples are kinda verbose to express mathematically than just making your functions only able to take one argument.

@maruseron

13 күн бұрын

@@oserodal2702 so? under no circumstance is conciseness a worthy pursuit during language design. ordered tuples are present in day to day human language, making them a concept significantly easier to understand (and therefore parse)

@user-kz4ym4tw4q

13 күн бұрын

​​@@maruseronThe issue with the representation you are proposing, it that it is not equivalent : one could want the function that adds 1 to it's argument. To do so, you could apply the "add" function to 1, and stop there. This is called partial application, and cannot be expressed in the way you want to express the types.

@maruseron

13 күн бұрын

@@user-kz4ym4tw4q you're incorrect - i'm talking purely about syntax and clarity, while partial application is a feature, hence existing only in the realm of semantics. it is entirely possible to have a language defining "int -> int -> int" as "(int, int): int" which allows partial application - in fact, it would be quite trivial. most languages don't do that because they find overloading (arity based, namely) to be a more worthwhile venture

I seriously thought you said "magician" instead of "logician" there - that's hilarious and probably also true.