From c59b15a701884cea99fa9ce5dd7bec0d00b355c7 Mon Sep 17 00:00:00 2001
From: Jim Pryor
Date: Thu, 16 Sep 2010 06:32:01 0400
Subject: [PATCH] deleted monday notes
Signedoffby: Jim Pryor

monday  591 
1 file changed, 591 deletions()
delete mode 100644 monday
diff git a/monday b/monday
deleted file mode 100644
index d058da35..00000000
 a/monday
+++ /dev/null
@@ 1,591 +0,0 @@
 Forwarded message from Jim Pryor 

Some notes on notation

Probably we won't want to explicitly give this to them until week 2 (or
later), but I jotted it down now so that we might agree about it and
stick to it.


These languages have VALUES of various TYPES. For instance, the number 2
is a value of the type integer. The string "horse" is a value of the
type string. Functions are also values. Their type depends on the values
of their domain and range. For instance, the successor function is a
value of the type integer > integer. The plus function is a value of
the type > integer. I'm fudging a bit here with the ; we'll come back to this and talk about the fudge soon.

We can talk equally of expressions having types: they have the types of the values they express.

(Sometimes the "untyped" lambda calculus is said to be "singlytyped". It may nor may not be helpful to think of it that way. If its expressions do have a type, though, it's a type T such that functions from T > T are also of type T. Myself I find it easier to think "untyped.")


In some of the languages, one refers to (and sometimes quantifies over) the types in the object language itself; so the object language itself has syntax for talking about types. We'll be discussing this later in the course. For now I'm just saying what notation will eventually be so used.

You need to keep straight about the difference between Constants of a
given sort, Objectlanguage Variables of the same sort, and Metalinguistic Schemas of that sort. I say "sort" here because you have this same threeway divide with BOTH expressions that express values and expressions that express types.

Sticking just to values, here are some examples of constants: 2, 3, +,
*, "horse", and so on.

Here are some examples of objectlanguage
variables: x, y10, first, second_place, and so on (you needn't stick to a
single letter). x', x'', and so on are also typically used as variables.
All the languages we'll be looking at will permit this syntax.

Conventions for metalinguistic schemas vary. In logic textbooks, one
often sees lowercase Greek letters used in this way. But in the fields
we'll be looking at, those are often used specifically as schematic
letters for TYPES. For schematic letters for VALUES, we'll go with the
convention that uses Capital Letters. For example:
 E is some expression of the lambda calculus. E may be "x" or "lambda
x: x" or "(lambda x: x y) (lambda z: w)" or whatever.
 (M N) is another expression of the lambda calculus, where some
possibly complex expression M is applied to another possibly complex
expression N.
 and so on.


More systematically:

 value variables in OCaml: start with lower case letter, can be
followed by any letter or number or _ or '
 value variables in lambda calculus: no fixed rules, but we'll
use the OCaml conventions, which is what you commonly see in practice.
 value variables in Scheme: all the OCaml variables are permitted.
Some Schemes are casesensitive, others aren't, others let you flip a
switch to decide. To avoid worrying about it, never use "firstPlace" as a
variable if you also use "firstplace" as a variable. Scheme also permits
very funky variable names, like "*add*" and "aretherethreeyet?" and
so on.

 Remember, value variables can be bound to values of various types,
including functions.

 value constants in lambda calculus: some lambda calculi have
primitive values in them, such as the number 0. But the mainstream ones
don't have any primitive values of any sort. All you've got are
variables, lambda abstractions of other stuff you've got, and
applications of other stuff you've got. If you want numbers or boolean
constants, you've got to "encode" them or build them yourself out of the
materials just described. We'll be looking at how that's done.

 in Scheme:
 simple values: 2, 3; #t, #f; #\h is a character (the eighth
letter in the Latin alphabet)
 function values: +, *
 in Scheme, like in the lambda calculus, functions always go
to the left: so you write (+ 2 3) not 2 + 3.
 compound nonfunction values: "h" "horse" and "" are three
strings of different length (the string "h" is built from the character
#\h but isn't identical to it; these values have different types)
 '(2 . 3) or (cons 2 3) is an ordered pair
 '(2 3) or (list 2 3) is a list. Other lists (with different
lengths) are (list), (list 2), (list 2 3 4).

 OCaml:
 pretty much like Scheme, except that:
 the ordered pair is written (2, 3)
 the list is written [2; 3]
 the eighth character in the Latin alphabet is written 'h'
 the string consisting just of that character is written "h", as
in Scheme
 true and false are written like that
 most functions are written leftmost, as in Scheme and the lambda
calculus. But a few familiar binary operators can be written infix: so
you can write 2 + 3. You can also write it functionleftmost, like so:
 ( + ) 2 3
 Here the parentheses are needed so that the OCaml parser can
figure out what you're doing.

Aside on parentheses:

 Parentheses are often optional in lambda caluli and also in OCaml.
 If M, N, and P are syntactically simple expressions, you can write ((M N) P), but you don't have to: you can also just write M N P. These mean exactly the same thing. To write M (N P) you do need the parentheses.

 In Scheme, EVERY parenthesis is meaningful and they are never
 optional. Typically parentheses mean to "apply this function to these
 arguments". So to add 2 and 3, you write (+ 2 3). In Scheme, this is different from
 ((+ 2) 3)  we'll talk about this later. For the purposes of our
 course, it would be more convenient if Scheme behaved more like lambda
 calculi and OCaml here.
 However, parentheses sometimes also do other duty in Scheme: if you
 print out the list (list 2 3) (also writable '(2 3)), the interpreter
 will display: (2 3). And the pair (cons 2 3) will display: (2 . 3). The
 parentheses here don't mean that 2 is being used as an argument.
 However, if you asked Scheme to "evaluate" one of these, it would think
 you were using 2 as a function.
 There are good reasons why parentheses are used in "both" of these
 ways in Scheme. We'll leave them for you to discover and read about.
 Another example of parentheses in Scheme: most of the parentheses in
 (let ((x 2)) (+ x 1)) don't play the role of applying functions to arguments.


Back to notation...

We've described value variables and value constants in all of these
languages. As we said, we'll follow the convention of using capital
Latin letters as metalinguistic schemas for value expressions in each of
the languages. Typically these schemas can stand for expressions of any
syntactic complexity. When we want them to stand for syntactically
simple expressions, we'll say so.


When we get to types, we'll use small Greek letters as metalinguistic
schemas for type expressions (of any syntactic complexity, unless we say
otherwise).

There are no type expressions or variables in standard Scheme.

Type expressions in OCamlwhether type variables or constants
representing predefined typesare usually written with lowercase
expressions (following the same rules as objectlanguage variables). So
"stack" in OCaml could designate a type or a value; it depends on the
linguistic context.

OCaml (and all languages of its ML family) does have a special rule for
type variables bound by quantifiers. Here you use 'x, 'stack, and so
on. It looks like the prefix ' used in Scheme, but it's used very
differently. Also, don't confuse the type variable 'x with the value
variable x'.

Aside:
 What's the difference between the type variable stack and the type
 variable 'stack? You use stack when you're binding it to a specific type
 value. So you might say:
 type stack = HERE SOME COMPLEX EXPRESSION THAT EXPRESSES A TYPE
 On the other hand, you use 'stack when you're only binding the variable
 with a quantifier: when you're saying suchandsuch holds for EVERY type
 'stack...


It would be good for us to fix on conventions for objectlanguage type
constants and variables in the lambda calculi (and to use something
other than small Greek letters, because they are metalanguage schemas).
 I don't know whether there are uniform conventions about this.



 End forwarded message 
 Forwarded message from Jim Pryor 

1. Introducing and pounding on difference between declarative and
imperatival computation.

2. Some geography

 Haskell
Scheme (functional parts) OCaml (functional parts)
  
  
  
Untyped lambda calculus 
  
Combinatorial logic 
 
 
============ Turing complete (briefly explain)=======================
 
 more advanced type systems 
 e.g. polymorphic types (System F)
 dependent types

 simply typed lambda calculus
 what linguists standardly use


Imagine in third column to the right of the others:

Typical languages like C, Python
Imperatival parts of Scheme, OCaml


3. How the same thing looks in each of these:

 in untyped lambda: add three two
 (if those are predefined, e.g. three defined as \sz.s(s(sz))
 in combinatorial logic: too long, pieces look like: S(BKI)K

 in Scheme: (let* [(three 3)
 (two 2)]
 (+ three two))

 in OCaml: let three = 3 in
 let two = 2 in
 three + 2;;

 in C: int three = 3;
 int two = 2;
 three + two;


Mutation in C: int x = 0;
 x = 1;

 in OCaml: let x = ref 0 in
 x := 1;;

 in Scheme: (let* [(x (box 0))]
 (setbox! x 1))


Pound more on how this is different, and we won't be looking at until a
lot of groundwork has been laid.


4. Question: how can mutation be something fundamentally new if some of
these other languages without it are Turing complete? How are they able
to encode/represent the same computations, without using mutation? (And
in fact, Turing completeness is more than is needed for this.)

Say a few words to sketch / reserve a place for an answer that they
should be able to appreciate at the end of the course.


5. Commonly people think of programming/computation as a sequence of
changes. But in the languages we'll first be looking at, there are no
changes. And moreover, there isn't at the beginning a very useful notion
of sequencing, either.

You can write sequences: in Scheme: (begin M N P Q R)
 in OCaml: begin M; N; P; Q; R end
 or: (M; N; P; Q; R)

however, these just have the value of R. So if none of the earlier
expressions have any sideeffects / make any changes, a sequence ending
in R means just the same as R.

Aside:
 I'm fudging a bit here: there may also be a difference if some of the
 earlier expressions in the sequence are incomputable, and so have what we'll
 later be calling the "bottom" value. More on this when we talk about
 evaluation order in a few classes.

 Another difference is that sequencing is explicit about what order the
 expressions get evaluated in, and this can affect computational
 efficiency. But that's not about their semantics.)

There's a bit of syntactic shorthand, which I'll introduce in a bit,
that LOOKS LIKE a kind of sequencing. However, once you understand what
it's shorthand for, you'll see that fundamentally, there's no sequencing
going on.

6. Instead of sequencing, we just have the
evaluation/simplification/"reducing" of single, often syntactically
complex, expressions.
 Later, when we introduce changes and sequencing, we'll do so in a
way that makes that a new piece of syntactic structure.




More "how to say the same thing in different languages"


1. Anonymous functions

 Lambda: \x.B
 for example, \x. times x five
 here times and five are free variables, we suppose they're bound
 to appropriate values by the surrounding linguistic context

 Scheme: (lambda (x) B)
 for example, (lambda (x) (* x 5))
  perhaps aside about role of parens in Scheme should go here
instead

 OCaml: fun x > x * 5
 or: fun x > ( * ) x 5


2. Binding variables to values with "let"

 in Scheme:
 (let* [(x A) (y A')] B)

 explain that Scheme also has a simple "let", which sometimes
 has a different meaning from let*, and that they usually will
 want let*, so we'll stick to using that in our pedagogy

 explain that there's also a letrec, which does automatically
 something that we want them to learn how to do by hand
 so for the time being we'll avoid it

 in OCaml:
 let x = A in
 let y = A' in
 B

 for example: let x = 3 + 1 in
 ( * ) x 5


 explain OCaml also has "let rec", which we'll also avoid for now


3. binding with "let" same as supplying as an argument to a function

 Scheme's (let* [(x A)] B) and OCaml's let x = A in B are the same
as:

 in Lambda: (\x.B) A

 in Scheme: ((lambda (x) B) A)

 in OCaml: (fun x > B) A


4. Functions can also be bound to variables

 in Scheme: (let* [(f (lambda (x) B))] ...)

 in OCaml: let f = fun x > B in ...
 OCaml shorthand: let f x = B in ...

5. This in Scheme:
 (let* [(f (lambda (x) B))] (f A))
 as we've said, means the same as:
 ((lambda (x) B) A)
 and also means the same as:
 (let* [(x A)] B)

 Similarly, this in OCaml:
 let f = fun x > B in
 f A
 or in shorthand:
 let f x = B in
 f A
 as we've said, means the same as:
 (fun x > B) A
 and also means the same as:
 let x = A in
 B

6. What if you want to do something like this:

 (let* [(x A)] ...rest of the file or interactive session...)

 let x = A in ...rest of the file or interactive session...

You can override these bindings:
 (let* [(x A)] (let* [(x A')] B))
is the same as:
 (let* [(x A')] B)

The closest/innermost binding of x "shadows" or overrides more outer
bindings.

Scheme and OCaml have shorthands for wrapping a binding around the rest
of the file or interactive session.

In Scheme it's written like this:
 (define x A)
 ...rest of file or session...

In OCaml it's written like this:
 let x = A;;
 ...rest of file or session...

This is the construction that I said misleadingly looked like
sequencing. Fundamentally, though, it's just a syntactic shorthand for
complex letexpressions that don't involve any sequencing.


7. One more bit of shorthand, which is very often used.

This in Scheme:
 (define f (lambda (x) B))
can be written like this:
 (define (f x) B)

Similarly, this in OCaml:
 let f = fun x > B;;
can be written like this:
 let f x = B;;

(Compare how "let f = fun x > B in ..." can be written "let f x = B in
...")




Subject: Concatanation (!= sequencing)

When we concatenate expressions in these languages, we'll usually be
treating the leftmost expression as a function, and the rest of the
expressions as arguments to it.

M N P

in lambda and OCaml treat M as as the function, and N as its first
argument. M N should evaluate to another function, which takes P as its
first argument. So this is equivalent to:

(M N) P

If you want M (N P) instead, you need to explicitly use parentheses.

Explain currying:
 add three two = (add three) two

In Scheme, on the other hand, in the first place you always need to
include parentheses to force a function to be applied to arguments:

 (M N P)

Moreover, there's a difference between ((M N) P) and (M N P). And each
of those are different from ((M) N P). Scheme differentiates between
functions that take one argument, those that take zero arguments (these
are called "thunks"), and those that take more than one argument.

This is awkward for our pedagogy, especially when you play with lambda
calculus inside Scheme. We'll try to do some special tricks that will
let ((M N) P) and (M N P) come out in Scheme when you'd expect them to.
We'll tell you about this later.




Subject: Constants / predefined variables

In Scheme we have:
 #t and #f (Scheme uses # to start lots of special values, e.g. #\h)
 2, 3
 +, *

 Syntax for building compound values: '(2 . 3) or (cons 2 3) is a
pair; '(2 3) or (list 2 3) is a list. Other lists: '() or (list)

In OCaml we have
 true, false
 2, 3
 +, *
 in OCaml most functions are written to the left of their
arguments, as in lambda and Scheme. But common arithmetic operations are
infix unless they're enclosed in parens. So you'd write:
 2 + 3
or:
 ( + ) 2 3
(Note: if you do this, best to always write ( + ) not (+). Sometimes it
doesn't matter but sometimes it does because of a language design
issue.)
 pairs: (2, 3)
 lists: [2; 3] others: []


In lambda, we have:
 Nothing!

Some lambda calculi do have constants, such as numbers. But mainstream
ones don't.

If you want boolean values, or numbers, or ordered pairs, or anything,
you'll have to make them by hand out of the raw stuff of the lambda
calculus.


How do we build our own?
 We'll start with boolean values
 Next we'll do pairs, triples, and so on
 = possibly typeheterog collections, of a specific length >= 2
 Next class we'll do numbers
 We'll also do lists
 = ordered typehomogeneous collections permitting repetition,
 of arbitrary length >= 0

 Building multisets = unordered typehomog collections permitting rep
 sets = unordered typehomog collections without rep
 is harder. In these languages, functions are quite basic, ordered
pairs are harder, sets harder yet. Inverts the usual conceptual order.


Booleans

if B is a boolean value (simple or syntactically complex), and IFTRUE
and IFFALSE are any two other, arbitrary expressions, we want:

 B IFTRUE IFFALSE
to evaluate either to IFTRUE or to IFFALSE (depending on which boolean
value B is).

For instance:
 equal? two three X Y
should evaluate to Y.

The boolean constant true needs to be an expression such that:
 true X Y
always evaluate to X. How to do that?

Easy: define true to be: \x \y. x
Or more mnemonically: \t \f. t




Ordered pairs

If p is an ordered pair, we want it to accept a function of the form
(\x y. B) which does something with its component values.

For example:
 p (\x y. x)
should return the first member of p.
 p (\x y. add x y)
should return the sum of the members of p (assuming an appropriate
binding for add).

 Note: `p (\x y. add x y)` could also be written as `p add`

How to do this?

Easy: define p to be (\f. f first_value second_value)

then p (\x y. B) is
 (\f. f first_value second_value) (\x y. B) is
 (\x y. B) first_value second_value

Some comments here about CPS.


 End forwarded message 
 Forwarded message from Jim Pryor 

Date: Sun, 12 Sep 2010 20:13:46 0400
From: Jim Pryor
To: Chris Barker
Subject: Other...

I've got some other notes pounding on the declarative / imperatival
difference, that I'd want to work into discussion preceding everything I
sent you.

Other ideas I had for homework were just doing some betareductions and
so on. I can look for some Scheme exercises in Little Schemer or another
tutorial we've linked to. I'm sorry, I haven't really come up with much
more specific yet here.

Miscellany:

I've got a pet peeve about the standard presentation of the grammar for
lambda calculus as this simple, three rule system. Oh and then by the
way here's also this unofficial shorthand. It's fine to give them that,
but I also want to mention you can just give a mildly more complex
grammar for what people really write. And we can point them to that. I
worked it out myself, quickly, and could have missed some cases, but I
think I have it. If you know of another statement of this, we could
crosscheck it sometime.

I want to deemphasize the role of alphaconversion. It's perfectly reasonable to regard \x.x and \y.y as syntactically identical. I think Hankin has discussion of three ways to think about this, only one of which makes alphaconversion any substantive transformation.

I don't mind mentioning etareduction, but I want to signal that it
makes a difference to the calculus whether that's permitted, say that
we'll be discussing it some later, and for now they shouldn't think much
about etareduction.


Pedagogically I'd like to suppress etareduction by default, except when
we explicitly allow it.


 Forwarded message from Chris Barker 


2.11.0