lambda-match vs PMC

[Claus Reinke]

> lambda-abstraction doesn't even exist at expression level, but is 
> replaced by spliced matching; application exists, but is not needed,
> because (f e) = {| e |> {| f |} |} (unless I'm mistaken?)

oops, wrong brackets around f - should be:

{| e |> ^f^ |} --> {| ^f e^ |} --> f e

with f supposedly being a lambda abstraction ( \v.b ) represented 
as a match ( {| v => ^b^ |} ), we get:

f e = {| v => ^b^ |} e --> {| e |> v => ^b^ |} --> {| ^b^[ v\a ] |}
    --> b[ v\a ]

as seen on page 3 of the MPC2006 paper, also showing that
application reduces to argument supply, which provides beta
reduction.

claus