index 788e827..0122ed9 100644 (file)
@@ -99,6 +99,30 @@ For the most part, these uses are only loosely connected to each other. We'll te
Map
===

+<table>
+<tr>
+<td>Scheme (functional part)</td>
+<td>OCaml (functional part)</td>
+<td>C, Java, Pasval<br>
+Scheme (imperative part)<br>
+OCaml (imperative part)</td>
+<tr>
+<td>lambda calculus<br>
+combinatorial logic</td>
+<tr>
+<td colspan=3>--------- Turing complete ---------</td>
+<tr>
+<td>&nbsp;
+<td>more advanced type systems, such as polymorphic types
+<td>&nbsp;
+<tr>
+<td>&nbsp;
+<td>simply-typed lambda calculus (what linguists mostly use)
+<td>&nbsp;
+</table>
+
+
+

Rosetta Stone
=============
@@ -309,13 +333,11 @@ both represent the same function, the identity function. However, we said above

(\z z)

-yet when applied to any argument M, all of these will always return M. So they have the same extension. It's also true, though you may not yet be in a position to see, that no other argument can differentiate between them when they're supplied as an argument to it. However, these expressions are all syntactically distinct.
+yet when applied to any argument M, all of these will always return M. So they have the same extension. It's also true, though you may not yet be in a position to see, that no other function can differentiate between them when they're supplied as an argument to it. However, these expressions are all syntactically distinct.

The first two expressions are *convertible*: in particular the first reduces to the second. So they can be regarded as proof-theoretically equivalent even though they're not syntactically identical. However, the proof theory we've given so far doesn't permit you to reduce the second expression to the third. So these lambda expressions are non-equivalent.

-There's an extension of the proof-theory we've presented so far which does permit this further move. And in that extended proof theory, all computable functions with the same extension do turn out to be equivalent (convertible). However, at that point, we still won't be working with the traditional mathematical notion of a function as a set of ordered pairs. One reason is that the latter but not the former permits uncomputable functions. A second reason is that the latter but not the former prohibits functions from applying to themselves. We discussed this some at the end of seminar (and further discussion is best pursued in person).
-
-
+There's an extension of the proof-theory we've presented so far which does permit this further move. And in that extended proof theory, all computable functions with the same extension do turn out to be equivalent (convertible). However, at that point, we still won't be working with the traditional mathematical notion of a function as a set of ordered pairs. One reason is that the latter but not the former permits uncomputable functions. A second reason is that the latter but not the former prohibits functions from applying to themselves. We discussed this some at the end of Monday's meeting (and further discussion is best pursued in person).

@@ -325,7 +347,11 @@ Booleans and pairs
Our definition of these is reviewed in [[Assignment1]].

-
+It's possible to do the assignment without using a Scheme interpreter, however
+you should take this opportunity to [get Scheme installed on your
+computer](/how_to_get_the_programming_languages_running_on_your_computer), and
+[get started learning Scheme](/learning_scheme). It will help you test out