Lalish-Menagh, Trevor on 4 Nov 2011 14:29:49 -0700


[Date Prev] [Date Next] [Thread Prev] [Thread Next] [Date Index] [Thread Index]

Re: Functional Fall tomorrow night: A Tutorial Introduction to the Lambda Calculus


Here is the text file from the meeting for MBL to prettyify. :)

On Wed, Nov 2, 2011 at 11:30 PM, Dan Mead <d.w.mead@gmail.com> wrote:
> good meeting guys.
>
> Had the fire alarm not gone off i wanted to have a discussion about how
> lambda-calc is turing complete, but here are some interesting links instead:
>
> http://en.wikipedia.org/wiki/Lambda_calculus
>
> -basically everything covered in the short and long papers. pretty good
> article
>
> Can anyone find an article that says the lambda calc and be used as an
> acceptor for a type-0 grammers?
>
> It's implied by the church-turing thesis, but I haven't seen it explicitly
> stated anywhere.
>
> http://en.wikipedia.org/wiki/Chomsky_hierarchy
>
> http://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis
>
>
> also, during the meeting I tried to conflate alpha and beta reduction with
> evaluation orders. that was totally wrong.
>
> Dan
>
> On Wed, Nov 2, 2011 at 12:54 AM, Jim Snavely <ludflu@gmail.com> wrote:
>>
>> Ok, this paper sort of blew my mind a little. I knew a little about
>> lambda calculus before this...but not really, I realized.
>>
>> As usual, the only way I understand anything is by writing working
>> code. The following is the logical operations section translated into
>> Haskell. (note the backslash is Haskell syntax for a lambda
>> expression)
>>
>> true = \x y -> x
>> false = \x y -> y
>>
>> toBool f = f 1 2 == 1
>>
>> land = \x y -> x y (\u v -> v)
>> lor = \x y -> x (\u v -> u) y
>>
>> lnegate = \x -> x (\u v -> v) (\a b -> a)
>>
>> main = print $ toBool $ lnegate false
>>
>> or try:
>>
>> main = print $ toBool $ true `land` false
>>
>> contrast with:
>>
>> main = print $ toBool $ true `lor` false
>>
>>
>> --Jim
>>
>>
>> On Wed, Nov 2, 2011 at 12:15 AM, Dan Mead <d.w.mead@gmail.com> wrote:
>> > the other longer paper gives alot of good definitions that this one kind
>> > of
>> > just skips over. I'll bring printouts.
>> >
>> > Dan
>> >
>> > On Tue, Nov 1, 2011 at 2:42 PM, Lalish-Menagh, Trevor <trev@trevmex.com>
>> > wrote:
>> >>
>> >> Hi all,
>> >>
>> >> Don't forget that tomorrow night at 6:30pm is Functional Fall 5 at the
>> >> Comcast Center (Room 45P). We will be
>> >> reading "A Tutorial Introduction to the Lambda Calculus."
>> >> (http://www.utdallas.edu/~gupta/courses/apl/lambda.pdf)
>> >>
>> >> As always there will be pizza and cola provided, and beer afterwards.
>> >>
>> >> Don't forget to RSVP at http://www.doodle.com/dvd85t6iw8hs8vqp
>> >>
>> >> I hope to see you there!
>> >>
>> >> Yours,
>> >> Trevor
>> >> --
>> >> Trevor Lalish-Menagh
>> >> trev@trevmex.com
>> >> 484.868.6150Â(mobile)
>> >> trevmex (AIM)
>> >
>> >
>>
>>
>>
>> --
>> --Jim
>
>



-- 
Trevor Lalish-Menagh
trev@trevmex.com
484.868.6150 (mobile)
trevmex (AIM)
\x. xy

\x xy 1

1y


let x = 2
    y = 1
  x + y

def wtf(x)
  x * y
end
wtf(2)

\x.x \y.yx

\y yx


(\x.xy) (\z.z) 1

((\z.z) y) 1

y 1

(\x.(\t.xt))y

(\t xt) [x/ y]

\t. yt


(\x.(\y.(x(\x.xy)))) y

[x q] (\x. (\y. (x (\x.  x y)))) y


(\q. (\y. (q (\x.  x y)))) y


[y / b] (\q. (\y. (q (\x.x y)))) y


(\q. (\b. (q (\x.x b)))) y

[q / y] (\q. (\b. (q (\x.x b)))) y

(\b. (y (\x.x b)))


(\b. (y (\x.x b)))

 
(\b. (y (\x.x b)))

           S            0
S0 == 

(\wyx. y(wyx)) (\sz.z)


 [w / (\sz.z)] (\wyx. y(wyx))

(\yx. y ( (\sz.z) y x))



(sz:s(sz))(wyx:y(wyx))(uv:u(u(uv)))















S0  (S0 == ((\b. (y (\x.x b)))
	wyx:y(wyx))((\b. (y (\x.x b)))
sz:z)
wyx:y(wyx))(S0 == ((\b. (y (\x.x b)))
	wyx:y(wyx))((\b. (y (\x.x b)))
sz:z)
sz:z)