This is the homepage for
*CS 465: Language, Logic and Computation),*
a course offered by
Fritz Ruehr at the
Computer Science Department of
Willamette University.
The course develops formal languages from the perspectives of logic,
mathematics and computer science, but emphasizes semantics of programs,
in contrast with the traditional treatment of formal languages as sets of
strings.
It is organized as a tour of successively enriched object languages and of
the meta-linguistic techniques needed to rigorously describe them.

The style of presentation will be influenced by functional programming, category theory, the Curry-Howard correspondence, and the Squiggol school of constructive programming (catamorphisms, anamorphisms, etc.); Haskell is used as an implementation meta-language.

The official course description reads:

Language is the basic for complex communication, whether as natural language between humans or as formal language between humans and computers. In programming, different kinds of formal languages are crucial tools in all stages of development, from the logics used to specify requirements, to the programming languages used to implement algorithms and the mathematical notations used to analyze their behavior. In this course we will study the general phenomenon of formal language by exploring the syntax, semantics and logics of a broad range of examples, beginning with the simplest numeral notations and operator algebras and continuing through to computationally complete languages and sophisticated type systems. In addition to studying abstract descriptions of syntax and semantics, students will reinforce their understanding by implementing language-based tools in a functional meta-language.

(This course *is* a rather idiosyncratic approach to a revised CS Theory curriculum;
but the general topic is not without some precedent, as evidenced by, e.g.,
the Tbilisi Symposium on Language, Logic and Computation,
the Institute for Logic, Language and Computation at Universiteit van Amsterdam
(also here),
the Journal of Language, Logic and Computation,
the book Algebras, Diagrams and Decisions in Language, Logic and Computation,
the breadth studies program in Language, Logic and Computation at The University of Melbourne,
the Centre for Logic, Language and Computation at the University of Melbourne,
the workshop Language, Logic, and Computation in Honor of Prof. Nachum Dershowitz,
the The Association for Logic, Language and Information,
and the Workshop on Logic, Language, Information and Computation, among others.)

**Welcome to the 2015 version of the course!**

- Here are some outline-formatted notes on lambda calculus (study-guide style): notes on lambda calculus.
- Some materials on lambda calculus:
- a nice, short introduction
*(by Rojas)*; - a longer introduction
*(by Barendregt & Barendsen)*; - the Wikipedia page;
- from the Stanford Encyclopedia of Philosophy.

- a nice, short introduction
- Just for fun:
*The Mathematician‘s Alphabet*(from lab). - You can find the new homework assignment on formal proofs here.
- According to this article in the research journal of the
*British Psychological Society*, we think more rationally in a non-native language.

Shirley, this must have implications for the psychology of formal languages. - The midterm grades are summarized in this histogram.
- Some materials on logic:
- Here are some presentations of deduction rules:
- Here is a sample deduction or two.
- Here are some links at Wikipedia relevant to logic:

- Once we’re done with the midterm, we will take a look at this
application of “folds-as-compositional-semantics” to
print out full truth tables (which would have been helpful for
doing
*and grading*homework and exam problems):`TTable.pdf`

. - Lab 2 on parsing Java
is now available. The Haskell code file you will use in this
lab is:
`Parsing.lhs`

.

*(See also the monadic parsing resources listed below.)* - The midterm is still being graded; hopefully it will turn out better than the 2011 midterm.
- Some materials on monadic parser combinators:
- You can read an actual journal article about monadic parsers here:

Graham Hutton and Erik Meijer’s*Monadic Parsing in Haskell*

(note especially the treatment of expressions on page 7); - here are some PowerPoint slides from Graham Hutton for lecture on Friday 20 March;
- here is a(n abbreviated) version of the parsing library:
`ShortParse.hs`

; - … and here is a little cartoon: Dr. Seuss on Parser Monads.

- You can read an actual journal article about monadic parsers here:
- Review for the midterm exam using these notes.
- For Friday, March 6, we’ll clean up loose ends on semantics
for algebraic terms, including polynomial function semantics and
propositional logic; see these files:
- the polynomial code from below;
- this diagram concerning polynomials ; and
- this code for propositional logic.

*(Perhaps we should also consider*porpositional*logic, which concerns reasoning about the location of dolphins … .)* - For Monday, March 2, we’ll be working on terms with variables
and (polynomial) function semantics, using this file:
`PolyL15.hs`

. - Some links for lecture (Wed 25 Feb):
- Regarding algebraic terms, see
this diagram and
these notes.

*(Plus, see this diagram re last lecture.)* - Get the latest lecture/outline here.
- Some links for lecture, Wed 18 Feb 2015:
- a stylized lecture on Haskell code for natural numbers a la Peano;
- putting (binary) products of arbitrary symbol sets into order (also see lexicographic ordering of face cards);
- selected slides from a(n incomplete) lecture on numeral notation:
- unfolding natural numbers to get numerals (strings);
- a simplified file for natural/numeral conversion (by base);
- and an inspirational cartoon!

- Here is a quick summary of regular language definitions, including REs, DFAs, and NFAs.
- Lab 1 on regular languages is now available. The Haskell code file you will use (i.e., read, digest, experiment with, and extend) is available in two versions (text and PDF) as:
- Here are the hints about the state-ripping transformation from NFAs to REs.
- (I made a quick update to the topical calendar to reflect our current routing through the basic math and language materials.)
- Slight (or is it “sl
*e*ight”?) change of plans: we will move right from [Symbols, strings, and sequences] to [Regular languages], topically speaking. You can find a broad summary “road map” of the various concepts and constructions involved here: regular languages roadmap. - You can read the details of the UTF-8 encoding scheme for Unicode characters at Wikipedia page on UTF-8; you might pay special attention to the technical description and the “salient features” bullet list that follows. Since the encoding is pretty straightforward, but also technically adept (and cute/slick), I will include it amongst the skills I allow myself to test on exams.
- Here are some course-wide documents, for posterity & reference:
- The little mini-lab for students who have just been introduced to Haskell
is now available as
Lab Zero. This lab will
*not*be graded, but rather gone over in lab: it is intended to helo those who need it get started with Haskell (or get back “get back in the saddle” if they’ve been away from it for a while). *[Quick political aside: You just can’t buy irony this good; I opened the news this morning to find these 2 articles listed one right after the other:**I guess I should be glad to live in a time when entertainment is so cheap!]*- Here are links to diagrams about:
- The review of math is available, although not complete (as of Wed 21 Jan); more to come soon!
- Here are the “chunking” exercises for those who are new to Haskell.

- Lab 2 on parsing Java.
- Lab 1 on regular languages.
- Lab Zero is not an official, graded lab (see above).

We will be using the Haskell programming language as our primary meta-language and implementation vehicle. There are plenty of on-line resources on Haskell, how to use it, downloadable implementations, etc. For example, you can try Haskell out in your browser, including a nice set of guided lessons and exercises.

You might also want to take a look at a tutorial or two from
this list
at the Haskell Wiki pages. I especially recommend the book, available
on-line for free,
*Learn You a Haskell for Great Good* (complete with cartoons).

You also might want to download an implementation for use on your own machine;
there is a fully-featured, multi-platform version available as
**the Haskell Platform**;
it includes an industrial-strength compiler and a bunch of libraries.

On the other hand, we really don‘t need all this power, so you might want to get the simpler

- If you use a Mac, try this MacHugs installer which uses the command line (Terminal app) under Mac OS X.
- For Windows, try the WinHugs installation.
- For other operating systems (e.g., Linux), look for Hugs installers at this page.

We won't be using a formal textbook this semester, so I will be trying to gather links to relevant on-line material. A lot of good-quality articles are available on Wikipedia, the free on-line "open source" encyclopedia.

**Math review**We will need some basic background in set theory and related topics (orderings, functions, relations and some basic logic) as a foundation for later work. You should have some exposure to this material already, but I will work (quickly) through some review notes (to be linked above) in lecture. You can also read about some of the same topics at Wikipedia:

- top-level set theory links
- functions
- countable sets
- cardinality
- relations
- equivalence relations
- partial orderings
- Boolean algebra

**Sets, domains and types**- Wikipedia on Domain Theory
- Wikipedia on Denotational Semantics
- Math usage of "image"
- Math usage of "domain" (
**not**as in "domain theory") - Wikipedia on Abstraction in CS
- Wikipedia on Semantics of Programming Languages

**Some references on symbols (Unicode and semiotics)**- The Unicode home page
- Wikipedia on Unicode
- Joel Spolsky (software pundit) on Unicode
- A unix/linux Unicode FAQ
- A free on-line Unicode character map
- Wikipedia on graphemes versus glyphs
- Wikipedia entry on semiotics
- Semiotics for Beginners by Daniel Chandler

**Formal languages, finite automata and regular expressions**- Wikipedia on Formal Languages
- Wikipedia on Finite State Machines
- Wikipedia on Context-Free Grammars
- Wikipedia on the Chomsky Hierarchy
- Wikipedia on Formal Grammars
- Wikipedia on Parsing
- Wikipedia on NFAs

**Tries and related data structures (reifying functions on strings)****Lambda calculus, types and type theory**- Lambda calculus - Wikipedia, the free encyclopedia
- SKI combinator calculus - Wikipedia, the free encyclopedia
- Church encoding - Wikipedia, the free encyclopedia
- Type system - Wikipedia, the free encyclopedia
- Typed lambda calculus - Wikipedia, the free encyclopedia
- Curry-Howard - Wikipedia, the free encyclopedia
- Intuitionistic Type Theory - Wikipedia, the free encyclopedia

**Some references on the Collatz ("3n+1") problem**