CS 3MI3: Fundamentals of Programming Languages - A3: Revenge of the Goblins and Gnomes
CS 3MI3: Fundamentals of Programming Languages
Idea
The goals of this assignment are:
1. Learn how to interpret small-step semantics
2. Learn how to translate semantics into an implementation
3. Learn how to identify buggy semantics
Logistics
A project template is available on the course GitHub that includes all of the code from this document, along with a testing framework. You can find it at the following url:
The Tasks
1 Revenge of the Goblins and Gnomes [40 points]
The goblins and gnomes of the magical island were very entertained by your riddle solving program. Unfor- tunately, they got bored of that pretty fast, and will not let you go home unless you can write a program that plays the famous Gnomish game called “SKI”.
The rules of “SKI” are as follows: you are given an expression in the following grammar:
⟨expr⟩ ::= S |K
|I
| |
⟨expr⟩ ⟨expr⟩ (⟨expr ⟩)
Unparenthesized expressions are left associated, so SKI should be parsed as (SK)I. To play “SKI”, you must apply the following sequence of reduction rules1:
e 1 → e ′1
e1 e2 →e′1 e2
e 2 → e ′2
v1 e2 →v1 e′2
Sxyz → xz(yz)
Implement a Haskell datatype called SKI that corresponds to the provided BNF, and then implement a
Kxy → x Ix → x
Haskell function with the following signature that performs a single step of these reduction rules.
1Nobody said that gnomes were good game designers.
1
ski :: SKI=>MaybeSKI
The function ski should return a Just containing a reduced value, or Nothing if no reductions were possible. Write at least 10 tests using HUnit, making sure that you test all reduction rules, as well as edge cases. Code is worth 15 points, tests are worth 15, and documentation is worth 10. You should write your code in a file called “src/A3/SKI.hs”, and your tests in a file called “test/SKITests.hs”; both of these files are already set up for you in the project skeleton.
2 Loopy Lambdas
One of the major reasons programming-language theorists love the λ-calculus is that it is a good basis for building other programming languages. Here, we will consider an extension of the λ-calculus that adds natural numbers, and a simple looping construct.
⟨expr⟩ ::= ⟨var⟩
-
| λ ⟨var⟩. ⟨expr⟩
-
| ⟨expr⟩ ⟨expr⟩ |0
| | |
1 + ⟨expr⟩
loop ⟨expr⟩ ⟨expr⟩ ⟨expr⟩
(⟨expr ⟩)
Intuitively, ‘loop i s f’ denotes a loop that counts down from i to 0, applying f at each step until it terminates with s. However, intuition isn’t enough: we need some sort of formal semantics to specify exactly how our programs evaluate!
2.1 One Small Step for Lambdakind [40 points]
Implement the following operational semantics in Haskell; it should have the signature
stepLoop :: Expr => Maybe Expr
e 1 → e ′1
e1 e2 → e′1 e2 (λx.e1) e2 → e1[e2/x]
e → e′
1 + e → 1 + e′
e 1 → e ′1
loope1 e2 e3 →loope′1 e2 e3 loop0e2 e3 →e2 loop(1+e1)e2 e3 →e3(loope1 e2 e3)
The Expr type can be found in the project skeleton, along with code for checking α-equivalence of terms and performing substitutions.
You should also write at least 25 tests, making sure to cover all constructors, as well as edge cases. At least 3 of these tests should construct your student number. You are allowed (and encouraged!) to use the provided helper functions in your testing code.
Furthermore, both you step function and tests should be documented. The documentation for the step function should make clear what rules you are applying, and the documentation for the tests explain why you are testing something. Code is worth 15 points, tests are worth 15, and documentation is worth 10. You should write your code in a file called “src/A3/LoopyLambda.hs”, and your tests in a file called “test/LoopyLambdaTests.hs”; both of these files are already set up for you in the project skeleton.
2.2 Another Small Step for Lambdakind? [20 points]
Consider the following additional reduction rule.
e 2 → e ′2
loope1 e2 e3 →loope1 e′2 e3
If it is possible to extend our implementation with this reduction rule, write a function
stepLoopExtra : : Expr => Maybe Expr
If it is not possible, explain why. Your answer should take the form of a comment, using the following format:
{= [Question 2.2]: <your answer here>
=}
Submission Requirements
-
Must be handed in as a .zip, .gz, or .7z file. Other archive formats will not be accepted, resulting in a score of 0. The archive should be called A3 macemailid.zip (with your email address, I am “carette”, substituted in).
-
The name of the file does matter.
-
Code which does not compile is worth 0 marks for the code (including testing) portion of the
assignment. Code should be compilable on at least Windows, macOS, and Linux.
-
Marks will be deducted if you have junk in your archive (such as object files, .DS Store files, pointless subdirectories, etc.). Stack project files and cabal files are exempt from this.
-
If you looked things up online (or in a book) to help, document it in your code. If you have asked a friend for help, document that too. “Looked things up online” includes all AI tools. Put this in a README file (as plain text, Markdown, or HTML).
Bonus
Mechanized Metatheory [Difficulty: ⋆⋆]Encode the loopy lambda calculus in either Agda or Idris 2, and encode the reduction rules as an indexed type. Use this indexed type to prove that (λx. x x)(λx. x x) has no normal form.
Include the Agda or Idris file inside of the submitted .zip file. Downhill SKI-ing [Difficulty: ⋆⋆⋆]
Gnomes may be bad game designers, but it turns out that they know a thing or two about theoretical computer science. To start, note that it is possible to interpret the SKI language into the λ-calculus like so2:
S 7→ λx.λy.λz.xz(yz) K 7→ λx. λy. x
I 7→ λx. x
In fact, it is also possible to interpret lambda calculus into SKI. Your task is to invent an algorithm for compiling expressions in the untyped λ-calculus into SKI expressions, and to implement this algorithm in Haskell.
This should be submitted as src/A3/LambdaToSKI.hs.
Self-referential SKI [Difficulty: ⋆⋆⋆⋆⋆]
Church-encoding allows us to represent datatypes inside of the untyped λ-calculus. Furthermore, the syntax of untyped λ-calculus is itself a datatype. If we put these two facts together, we can encode the syntax of untyped λ-calculus inside of itself via Church-encodings. Use this observation to implement the compiler from λ-calculus into SKI inside of your implementation of the untyped λ-calculus. For fun, note that you can use your solution from Bonus 2 to make your program “self-hosting”: it is a compiler from untyped λ-calculus to SKI, written only using SKI!3
This should be submitted as src/A3/SelfReferenceSKI.hs. Be warned: this is devilishly hard.
