Advanced Programming Languages (שיטות תכנות מתקדמות)

Scheme is the main programming language for the first part of the course. It is a semi-functional, late-binding, dynamically-typed, interactive programming language. It is the most suitable language for working with the untyped lambda calculus. For this course, I'm going to ask you to work with Petite Chez Scheme, which is avaiable for free on most common platforms. You are welcome to try out other Scheme systems (there are even a couple for the iPhone! ☺ ), but for the purpose of the assignments, please make sure your code runs on Chez. Click here to go to my Scheme page.

ML is the second language we shall be using the the first part of the course. It is a semi-functional, early-binding, statically-typed interactive programming language. We shall be using it in our discussions on types, and perhaps in other places as well. Click here to go to my ML page.

• Introduction to functional programming
• The syntax of the \(\lambda\)-calculus
• \(\alpha\)-equivalence, \(\beta\)-reduction, \(\eta\)-reduction
• The notion of confluence, and the first and second Church-Rosser theorems
• Introduction to \(\lambda\)-definability
  • Church numerals
  • Successor on Church numerals
  • Multiplication on Church numerals
  • Exponentiation on Church numerals
  • Super-exponentiations, and the Ackermann-Péter function

• Continuing \(\lambda\)-definability
  • Review of Church numerals and the functions we defined on them
  • The Ackermann-Péter function, and why it is second-order primitive recursive
  • Boolean values, Boolean functions
  • The Zero-predicate & related functions
  • Pairs, triples, and the projections on them
  • Factorial, Fibonacci, and the predecessor functions
  • The monus function
  • <=?, >=?, <?, >?, <>?, =?

• Closing notes on \(\lambda\)-definability
  • Defining alternate numeral systems
  • Adding reflective capabilities to our representation of ordered \(n\)-tuples
• More on the syntax of the \(\lambda\)-calculus
  • Free variables, bound variables
  • Combinators
• Introduction to fixed points (part I)
  • The motivation: Difficulty to define recursive functions
    • Combinators
    • Global names as macros in the meta-language of the \(\lambda\)-calculus
    • The inappropriateness of the substitution model in recursive definitions
  • Fixed points over real numbers
  • Programs as fixed points
  • The notion of leastness and least fixed-points in programming languages
  • Recursive functions as solutions to fixed-point equations
  • An in-place derivation of a fixed-point combinator
    • \(\mathrm{Factorial} \rightarrow F \rightarrow G \rightarrow H\)
    • \(G\) in the C programming language
      • The (void *) type as a hack to facilitate recursive types in C
    • The recursive function as a fixed point, the fixed point as \((H H)\)
    • Defining \(H\) in terms of \(F\)
      • Composition
      • Abstracting \(F\): Curry's fixed-point combinator
      • Applicative order vs normal order
      • Monadic, dyadic, triadic, and variadic eta-expansion (\(\eta^{-1}\)) of \((x x)\).
  • Simple uses of fixed-point combinators
    • Defining recursive functions
    • Defining circular structures

• Introduction to fixed points (part II)
  • Turing's fixed-point combinator
  • The infinitude (אין-סופיות) of fixed-point combinators
  • More on relations
    • The one-step relation \(\rightarrow_{R}\)
    • The reflexive-transitive closure of the one-step: the multi-step relation \(\rightarrow\hskip-1.5em\rightarrow_{R}\)
    • The the reflexive-symmetric-transitive closure of the one-step: the equality relation \(=_{R}\)
    • A formal definition of the \(\beta\) relation
    • A formal definition of the \(\eta\) relation
    • A formal definition of the \(\beta\eta\) relation
    • The finitude of \(\beta\eta\)-equality (equality on \(\lambda\)-terms)
    • The recursive enumerability of fixed-point combinators
  • Böhm-trees, equality-by-extension
    • Non-standard fixed-point combinators & observational equivalence
  • "Happy Birthday" fixed-point combinators

• Introduction to fixed points (part III)
  • Multiple fixed-point combinators
    • Curry's construction
    • Turing's construction
    • Smullyan's construction
    • A construction based on \(n\)-tuples
    • The infinitude of multiple fixed-point combinators
    • Re-visiting the construction of circular structures with multiple loops, the expansion of letrec, etc.

• Set-equality vs \(\beta\eta\)-equality
• A set generated by another set
• The closure under application
  • Church numerals
  • Projections
• Bases
  • Definition
  • Abstraction algorithm
  • The basis \(\mathfrak{B} = \{I, K, B, C, S\}\)
    • Proof
    • The abstraction algorithm
  • The basis \(\mathfrak{B}^{\mathrm{II}} = \{S, K\}\)
    • Proof
    • The abstraction algorithm
  • The basis \(\mathfrak{B}^{\mathrm{III}} = \{I, J, K\}\)
    • Proof
    • The abstraction algorithm
  • One-point bases
    • Proof
    • The abstraction algorithm
  • Proofs by contradiction
  • The Schönfinkel meta-game

• The \(\lambda{I}\beta\eta\)-calculus
• Motivation: How Church tried to capture the notion of strictness, namely, that \(f(\bot) = \bot\)
• The "natural" basis for the \(\lambda{I}\beta\eta\)-calculus: \(\{I, B, C, S\}\)
• Church's original: \(\{I = \lambda x.x, J = \lambda xyzt.xy(xtz)\}\) basis and how to think in terms of it.

• Closure under application
• Online G\"odelization
• 1-point bases for Scheme (\(\lambda\)-calculus with finitely-many constants)
• Solution to the tragic squares problem

• Introduction to type theory
• Finding the simple type of an expression
• The Curry-Howard Isomorphism
• The simply-typed \(\lambda\)-calculus
• The polymorphically-typed \(\lambda\)-calculus
  • Ackermann's function has second-order Church numerals

• Type theory – Continued
• Circular types
  • \(\lambda x.(x x)\) and its type
• Embedding recursive function types using recursive data types
• Self-application in SML/NJ
• Fixed-point combinators in SML/NJ
• Run-time type information & reflection kar, kdr, cons,

• Introduction to CPS
• Control in procedural languages
• Control in functional languages vs object-oriented languages
• Continuations and their equivalent in OOPLs
• Continuations & the tail-call optimization
• Different kinds of continuations
  • Multiple continuations
  • Continuations of several arguments

• Representation independence
• Defunctionalization (of the continuation)
• The stack machine transformation
  • The continuation tag as a return address
  • The apply-k procedure as a dispatcher over symbolic addresses
  • Please have a look at this page for worked-out examples of the steps to transform programs from direct style to stack machines

• Examples of the stack machine transformation
• Interleaving two functions
• Implementation of a multi-threaded kernel in Scheme
• The call/cc (call-with-current-continuation) procedure
  • Contexts, prompts, \(\lambda^{\!\!{}^{>}}\)
  • How to use call/cc
  • The escaper procedure: the non-tail-recursive version vs. the tail-recursive version

• Examples of CPS (now that the computer is back)
  • A defunctionalized version of Ackermann's function, in BASIC -- a language without recursion or local state
  • Fast Fibonacci using continuations
  • Dwandawa: Computing discrete convolutions with one pass
    • Using discrete convolutions to multiply numbers, using Vedic algorithms
• More on call/cc
  • Backtracking, computing alternatives, the one-of procedure
  • How to implement call/cc in the interpreter

• Introduction to Monads
  • Threading a computation with a store
  • Packaging value & store
  • Sequencing
• Examples
  • The store monad
  • The IO monad
  • The random monad
  • The gensym monad
• Introduction to threaded code
  • Direct threading
  • Indirect threading
  • Address interpretation

• More on threaded code
  • Threaded code & binding time
    • Significance for recursive procedures
    • TILs with early binding
    • TILs with late binding
  • The implementation of threads
    • Threads vs continuations
  • Threaded code & multi-threading
  • Threaded code as a compilation technique

• More on threaded code
  • The definition of WHILE in the threaded.scm file
• The Duff Device
  • Coroutines in C
  • Cannot be used to write a re-entrant recursive procedure
• Back to functional programming
  • Mapping functions
    • Map in LISP, Scheme
      • Map in Interlisp
      • Map with index
    • andmap, ormap
    • Filter
    • Partitions

• More on mapping functions in Scheme
  • Cross products (think how this is related to problem set #2 (!)
• Streams
  • Finite & infinite
  • Mapping over streams
  • Interesting examples
    • Stream of prime numbers
    • Streams of regular expressions (problem set #2)
    • Computable real numbers implemented as streams (option, contact me if this interests you)

• Introduction to Erlang (I)
  • Physically interacting with the Erlang process
  • Sessions & their names
  • The Erlang REPL
  • The Erlang datatypes
  • The Erlang source file
    • The module system: importing & exporting functions
  • Loading Erlang source files

Construct the expression \(P\) that satisfies the equation below, for Church numerals \(c_k, c_n\), where \(0 \leq k \leq n \in \mathbb{N}\): \begin{eqnarray*} P\ c_n\ c_k & = & \lambda x_1 \cdots x_n f_1 \cdots f_n . f_k(x_1 x_1 \cdots x_n f_1 \cdots f_n) \cdots (x_n x_1 \cdots x_n f_1 \cdots f_n) \end{eqnarray*} Now do notice that \(n, k\) are indecies both on the right-hand side as well as on the left-hand side of the above equation.

The motivation for this exercise is that once you have \(P\), it is straightforward to define a variadic version of Turing's multiple fixed-point combinators.

• Create a monad (in Scheme) to model random-access file IO. You should support the operations: open/create, close, put-char, get-char, set-file-position, get-file-position. The file could be modelled via a string, but may not use any side effects on that string. This last restriction implies that you may not be able to capture true random-access.

• Create a program (in one of Scheme, ML, Erlang, Java, Python), that takes some representation for a regular expression (that defines a set of strings), and returns a stream of all those strings. The set of strings can be empty, finite or infinite. The language for regular expressions should include support for constants, and operations for catenation, disjunction, and the Kleene star. You are welcome to support additional, derived operations.

Please solve 2 problems out of the following:

• The number of Combinators
  

  Write a procedure that take the number \(n\) and returns the number of combinators of length \(n\). For this problem, the \textit{length} of a combinator is defined as follows:

  \begin{eqnarray*}\def\Size#1{\mid #1 \mid} \Size{\nu} & = & 1 \\ \Size{(P Q)} & = & 1 + \Size{P} + \Size{Q} \\ \Size{(\lambda \nu . P)} & = & 1 + \Size{P} \end{eqnarray*}

  Your code will be tested on large numbers. For example, the number of combinators of length 300 is

  473477381975190304152771173386219140737139330572727481574 786077988437776485374930756297967309535888631641055198100 186060372310059690213121901539467263248370729333568234992 881170746462932742300417445775187087736611038605424576071 564968041698609452989548022519111112309976379200605183913 879075157976088494

• Address Interpretation
  

  Implement your own threaded, interactive language (TIL) using address interpretation. The implementation language should be C (not C++). Your system should support basic arithmetic & Boolean operations, conditionals (an if-then-else-like mechanism), function calls.

• Object-Oriented Programming in C
  

  Use C macros to write your own object-oriented extension to C. You should be able to define classes and methods. You do not need to support inheritance, thought hat would be nice. You should not go outside the C programming language (e.g., use M4 or Scheme for pre-processing).

  Demonstrate your object-oriented extension using some non-trivial example.