Re: please recommend book or web page on beginners lambda calculus

In article <sddr75mjcag.fsf@xxxxxxxxxxxxxxxxxxxx>,
Chris F Clark <cfc@xxxxxxxxxxxxxxxxxxxx> wrote:
My lamba calculus knowledge is old and stale and I can't easily read
some of the papers I want
(e.g. http://www-staff.it.uts.edu.au/~cbj/patterns/wrc_slides.pdf),
because I can't recall the notation, precedence, etc.

So, I'd like to read a good, quick, easy overview of the lambda
calculus, especially one that covers the notation, so that I can parse
a line like:

update_salary = \lambda f -> salary \lamba y -> salary ( f y )

That syntax (from the above slides) is very idiosyncratic and
knowledge of common conventions wouldn't help you there.

Apparently

Salary \lambda y -> ...

is itself a pattern, or two patterns: the first one just matches the
constructor Salary, the second one matches any value and binds it to
y. Usually this would be expressed as

\lambda Salary -> \lambda y -> ...

or just

\lambda Salary y -> ...

or with any of a number of variants. However, the syntax used in those
slides I have never seen before. The motivation seems to be that there
are first-class patterns (or at least first-class constructors), so we
need to distinguish between a pattern parameter (match the pattern this
variable is bound to) or an ordinary binder (match anything, bind this
variable to the value).

The slides also use the same syntax (juxtaposition) both for building
compound data and for function application. So in

update_Salary f y (update_Salary f z)

we are applying update_Salary to two arguments f and y, and the
resulting data structure is combined with the result of the
application in the parenthesis. This is apparently intentional, but
I'm not sure what the benefit is (apart from making the syntax a bit
simpler).

So these slides present a relatively exotic calculus, whose definition
is provided in the slides, too. Knowing "standard" lambda calculi
isn't going to be much use here, though of course it helps in
understanding the context and motivation for the work.


Lauri
.

Relevant Pages

  • Re: Feature request: String-inferred names
    ... especially since all the proposed syntax are ugly (the most acceptable ... When I first started seeing @ show up in Python code, ... the EXACT syntax of the ... The pattern manifested itself ...
    (comp.lang.python)
  • Re: Feature request: String-inferred names
    ... especially since all the proposed syntax are ugly (the most acceptable ... When I first started seeing @ show up in Python code, ... the EXACT syntax of the ... The pattern manifested itself ...
    (comp.lang.python)
  • Re: a SED need
    ... > every syntax I've tried has not worked. ... character is used for regular expression rather than a possible RE ... The match regular expression is repeated in gsub ... Therefore the next match-all pattern ...
    (freebsd-questions)
  • Re: Scheme closures
    ... > were writing the macro in a good way. ... It's useful to be able to choose between pattern matching or not. ... "Stx" is the syntax object representing the source syntax, ... In syntax-rules, the identifier in that position is ignored, and there's no ...
    (comp.lang.lisp)
  • Re: Looking for test slide for CTF measurements
    ... pattern with sufficiently fine line spacing to make CTF measurements ... alternating line patterns at 500 lp/mm, 1000 lp/mm, 2000 lp/mm. ... measuring slides. ...
    (sci.techniques.microscopy)