TE
科技回声
首页24小时热榜最新最佳问答展示工作
GitHubTwitter
首页

科技回声

基于 Next.js 构建的科技新闻平台,提供全球科技新闻和讨论内容。

GitHubTwitter

首页

首页最新最佳问答展示工作

资源链接

HackerNews API原版 HackerNewsNext.js

© 2025 科技回声. 版权所有。

What is the contribution of lambda calculus to the theory of computation?

112 点作者 kocheez75大约 11 年前

6 条评论

tikhonj大约 11 年前
The λ-calculus is basically the MVP of programming languages. It allows somebody designing a language feature or part of a type system to experiment with that feature <i>in isolation</i>. Fast iteration for programming language designers.<p>It&#x27;s also great as the core of a programming language. If you can express a feature just in terms of the λ-calculus, you can implement it almost for free. It&#x27;s just desugaring. Most of Haskell is like this: while the surface language has become rather complex, the majority of the features boil away rather transparently into typed lambda terms. Haskell uses a variant of System F which it actually calls &quot;Core&quot; to underscore how core this concept is :).<p>Of course, as the accepted answer points out, the λ-calculus is also very useful for logic. In some sense, it is a sort of &quot;proof essence&quot;: the basic building block of what a proof <i>is</i>. I really like this notion because it gives me a concrete, first-class object to represent a proof. Seeing proofs as programs really helped me come to terms (heh) with mathematical logic.<p>One surprising use for the λ-calculus outside of CS is in linguistics. In particular, linguists use typed λ-calculi to construct formal semantics for sentences. It&#x27;s a way to build up the <i>meaning</i> of, well, meaning. Or at least the things we say ;). I&#x27;m not super familiar with semantics in linguistics, but I&#x27;ve always thought it was very cool that they <i>also</i> use some of the same tools as programming language theory! Wikipedia has more about this: <a href="http://en.wikipedia.org/wiki/Formal_semantics_%28linguistics%29" rel="nofollow">http:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Formal_semantics_%28linguistics...</a>
评论 #7506895 未加载
评论 #7506601 未加载
评论 #7508000 未加载
javajosh大约 11 年前
The importance of <i>calculus</i> is most easily demonstrated by applying it to physics problems. For example, if I tell you how a ball moves in time, and then ask you how fast it&#x27;s moving after a certain number of seconds, then calculus will help you find the answer (take the derivative of the equation of motion and plug in the time).<p>What is the equivalent computer science problem that lambda calculus can help you solve? Challenge: pretend like you&#x27;re Richard Feynman and avoid jargon, if at all possible.<p>EDIT: I find it quite curious that I got so badly down-voted (-3 and counting!) for simply asking for concrete examples of applicability to actual, concrete problems. I&#x27;ve always found that tools are best understood in the context of their use. Even an abstract concept is useful to speak about in this way - for example, complexity&#x2F;Big O analysis helps us with capacity planning, comparing algorithms, and so on. It may be that lambda calculus helps us with, oh, decomposition of computation or something like that. But for all the digital ink I&#x27;ve read about it, it&#x27;s always seemed like an academic form of name-dropping. Even the name is intimidating, right? Reminds me of terms like &quot;schroedinger&#x27;s equation&quot; or &quot;canonical ensemble&quot; from the good old days in physics class. But behind the intimidating names is just a tool for solving problems - and I have yet to see anyone demonstrate this for lambda calculus. Granted I haven&#x27;t looked very hard!<p>It takes self-awareness to realize that you are enthralled with something without understanding it. The litmus test for this is the umbrage taken by someone who&#x27;s asked simple question about what their high-status concept is really used for. That&#x27;s why I mentioned Feynman in particular, because of his wonderful reputation as having knowledge that was totally grounded in reality.
评论 #7508564 未加载
评论 #7506766 未加载
评论 #7507010 未加载
评论 #7506652 未加载
评论 #7507045 未加载
评论 #7508695 未加载
评论 #7538863 未加载
评论 #7508773 未加载
评论 #7506685 未加载
评论 #7508601 未加载
nvarsj大约 11 年前
For anyone that wants a readable overview of the λ-calculus, I recommend reading the second chapter in Simon Peyton Jones&#x27; book:<p><a href="http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/" rel="nofollow">http:&#x2F;&#x2F;research.microsoft.com&#x2F;en-us&#x2F;um&#x2F;people&#x2F;simonpj&#x2F;papers...</a>
hyp0大约 11 年前
see also <a href="https://cstheory.stackexchange.com/questions/3650/historical-reasons-for-adoption-of-turing-machine-as-primary-model-of-computatio/3680#3680" rel="nofollow">https:&#x2F;&#x2F;cstheory.stackexchange.com&#x2F;questions&#x2F;3650&#x2F;historical...</a><p>It&#x27;s interesting that Turing never rigorously proved Turing Machines were a model of computation, it was only an intuitive appeal. He actually apologised for this when introducing them, in his <i>Entscheidungsproblem</i> paper <a href="http://www.turingarchive.Entscheidungsproblemorg/browse.php/B/12" rel="nofollow">http:&#x2F;&#x2F;www.turingarchive.Entscheidungsproblemorg&#x2F;browse.php&#x2F;...</a><p>Also curious is that Church wrote to him, saying that he found Turing&#x27;s model more intuitively convincing.<p>Intuitive appeal isn&#x27;t everything of course.
评论 #7511190 未加载
analog31大约 11 年前
This is probably going to sound really dumb, but I have utterly no formal computer science background. Lambda calculus in the languages where I have seen it (Scheme and Python) simply seems like a way to express a function as a one-liner. Surely, I&#x27;m missing something important, but I can&#x27;t figure out what.
评论 #7509694 未加载
评论 #7507579 未加载
评论 #7507601 未加载
评论 #7512237 未加载
评论 #7511208 未加载
betterunix大约 11 年前
This comes to mind:<p><a href="http://en.wikipedia.org/wiki/Curry-Howard_Correspondence" rel="nofollow">http:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Curry-Howard_Correspondence</a>