tag:blogger.com,1999:blog-10770855.post111602852610488327..comments2024-03-28T03:20:57.393-04:00Comments on The Little Calculist: The lambda machineDave Hermanhttp://www.blogger.com/profile/00405190527081772997noreply@blogger.comBlogger3125tag:blogger.com,1999:blog-10770855.post-1116103185425055822005-05-14T16:39:00.000-04:002005-05-14T16:39:00.000-04:00Well, maybe in that sense it's a misleading metaph...Well, maybe in that sense it's a misleading metaphor. But yes, I meant that it's a <I>mathematical</I> black box, where the observations of the machine's output are made by proving the machine halts or loops, not made within the computational framework itself.<BR/><BR/><I>So the black box is something that you always have to put at the top-level, wrapped around the underlying composition lf lambda expressions.</I><BR/><BR/>I think the natural expression of this generalization is in a process calculus. The lambda calculus is good for reasoning about computation, but when you want to reason about observing effects, process calculi are natural for expressing the relevant notions:<BR/><BR/>1. observation (reductions are tagged with observable labels)<BR/>2. information hiding (transition labels can be masked)<BR/>3. composition (processes can be combined in very general ways)Dave Hermanhttps://www.blogger.com/profile/00405190527081772997noreply@blogger.comtag:blogger.com,1999:blog-10770855.post-1116097993445406522005-05-14T15:13:00.000-04:002005-05-14T15:13:00.000-04:00The odd thing about your choice of black box is th...The odd thing about your choice of black box is that you can't build up larger black boxes in terms of the smaller one, because the terms themselves cannot observe the "false" output (loop).<BR/><BR/>So the black box is something that you always have to put at the top-level, wrapped around the underlying composition of lambda expressions.<BR/><BR/>To me, that's not as useful as something that I can build on top of. But I'm probably mixed up and thinking about this as an engineer, and not as a semanticist.pnkfelixhttps://www.blogger.com/profile/04222189622973190255noreply@blogger.comtag:blogger.com,1999:blog-10770855.post-1116085385281204432005-05-14T11:43:00.000-04:002005-05-14T11:43:00.000-04:00Interesting. Of course this is the bog-standard tr...Interesting. Of course this is the bog-standard trick for reducing particular problems to the halting problem in the context of Turing machines, but for some reason I'd never thought about it in the context of the lambda calculus. Neat!Jacob Matthewshttps://www.blogger.com/profile/01440842967865877789noreply@blogger.com