CIS 425讲解、Programming辅导、Java，Python，c/c++程序语言讲解 辅导R语言编程|辅导Python编程
- 首页 >> Python编程 Spring 2020 Assignment 4 (Interpreters)
CIS 425
April 2020
In this assignment, you will develop an SML interpreter for a small functional language called
PCF, which stands for Programming language for Computable Functions. The language is
relatively simple, yet powerful, with arithmetic expressions and functions. The syntax of
PCF programs is given by the following BNF grammar:
e ::= x | n | true | false | succ | pred | iszero | if e then e else e |
fn x => e | e e | (e) | let x = e in e
In the above, x stands for an identifier; n stands for a non-negative integer literal; true and
false are the boolean literals; succ and pred are unary functions that add 1 and subtract 1
from their input, respectively; iszero is a unary function that returns true if its argument is
0 and false otherwise; if e1 then e2 else e3 is a conditional expression; fn x => e is a
function with parameter x and body e; e e is a function application; (e) allows parentheses
to be used to control grouping; and let x=e1 in e2 is a let expression.
It should be clear to you that the above grammar is quite ambiguous. For example, should
fn f => f f be parsed as fn f => (f f) or as (fn f => f) f? We can resolve such
ambiguities by adopting the following conventions (which are the same as in SML):
• Function application associates to the left. For example, e f g is (e f) g, not e (f g).
• Function application binds tighter than if, and fn. For example, fn f => f 0 is
fn f => (f 0), not (fn f => f) 0.
We don’t want to interpret concrete syntax directly. Instead, the interpreter will work on
a parse tree (also called abstract syntax tree ) representation of the program; these syntax
trees will be values of the following SML datatype:
datatype term = AST_ID of string | AST_NUM of int | AST_BOOL of bool
| AST_SUCC | AST_PRED | AST_ISZERO | AST_IF of term * term * term
| AST_FUN of string * term | AST_APP of term * term
| AST_LET of (string * term * term)
| AST_ERROR of string
This definition mirrors the BNF grammar given above; for instance, the constructor AST_ID
makes a string into an identifier, and the constructor AST_FUN makes a string representing
the formal parameter and a term representing the body into a function. Note that there is
no abstract syntax for (e); the parentheses are just used to control grouping.
Practice1
Write the PCF abstract syntax tree term corresponding to the following PCF source expressions
(do this manually so that you understand; later, use your PCF parser to confirm your
answers).
1You do not have to submit anything for this part
1
Spring 2020 Assignment 4 (Interpreters)
CIS 425
April 2020
• (a) 123
• (b) (fn x => x ) 123
• (c) if iszero x then x else 0
Continuing
You will be building an interpreter that will evaluate Abstract Syntax Trees (ASTs) for PCF
to a final AST that represents a computed result.
Instead of building the parse trees for arithmetic expressions by hand (as in the previous
problem), we are providing you with a parser that converts from concrete PCF syntax to an
abstract syntax tree. The parser is available parser.sml. Include the command
use "parser.sml";
at the beginning of the file containing your interpreter. The parser defines the datatype term
as well as two useful functions, parsestr and parsefile. Function parsestr takes a string
and returns the corresponding abstract syntax; for example
- parsestr "iszero (succ 7)";
val it = AST_APP (AST_ISZERO,AST_APP (AST_SUCC,AST_NUM 7)) : term
Function parsefile takes instead the name of a file and parses its contents. (By the way,
the parser is a recursive-descent parser; you may find it interesting to study how it works.)
You are to write an SML function interp that takes an abstract syntax tree represented as
a term as well as an environment, represented as an env, and returns the result of evaluating
it, as a result. Initially, we will define our result datatype as follows:
datatype result = RES_ERROR of string | RES_ERROR of string | RES_NUM of int
| RES_BOOL of bool | RES_SUCC | RES_PRED | RES_ISZERO
| RES_FUN of (string * term);
The evaluation should be done according to the rules given below. (Rules in this style are
known in the research literature as a natural semantics.) The rules are based on judgments
of the form
env |- e --> v
which means that term e evaluates to value v (and then can be evaluated no further). For the
sake of readability, we describe the rules below using the concrete syntax of PCF programs;
remember that your interp program will actually need to work on SML values of type term.
2
Spring 2020 Assignment 4 (Interpreters)
CIS 425
April 2020
Environments
Interpreters also need a way of passing parameters to user-defined functions. In our interpreter,
we will be using environments. An environment is at its core, a set of relations, from
names to values. Whenever a term is evaluated, it will be done in the context of an environment.
This environment must be extendable to allow new variables to be bound, and it
must be searchable, to allow bound variables to be later retrieved. For example, if we were
to evaluate the expression:
We would start with an empty environment (). When we come to the first let expression,
we would add the relation (x,4) to our environment, and evaluate the body of the let in
that context. Similarly, when we come to the second let expression, we add (y,5) to our
environment, and evaluate its body in the further extended environment. Thus, when we
come to the expression x+y, we evaluate it in the environment ((x,4), (y,5)). In order to
determine the values of x and y, we merely look them up.
In the rules below, each judgement will occur in the context of an environment. For this
assignment, you will be provided with an environment implementation, so you won’t have to
write one yourself.
Rules The first few rules are uninteresting; they just say that basic values evaluate to
themselves:
(1) env |- n --> n, for any non-negative integer literal n
(2) env |- true --> true and env |- false --> false
(3) env |- succ --> succ, env |- pred --> pred, and env |- iszero --> iszero.
The interesting evaluation rules are a bit more complicated, because they involve hypotheses
as well as a conclusion. For example, here’s one of the rules for evaluating an if-then-else:
env |- b --> true env |- e1 --> v
(4) -----------------------------------------
env |- if b then e1 else e2 --> v
In such a rule, the judgments above the horizontal line are hypotheses and the judgment
below is the conclusion. We read the rule from the bottom up: “if the expression is an
3
Spring 2020 Assignment 4 (Interpreters)
CIS 425
April 2020
if-then-else with components b, e1, and e2, and b evaluates to true and e1 evaluates to v,
then the entire expression evaluates to v”. Of course, we also have the symmetric rule:
env |- b --> false env |- e2 --> v
(5) ------------------------------------------
env |- if b then e1 else e2 --> v
The following rules define the behavior of the built-in functions:
env |- e1 --> succ env |- e2 --> n
(6) ------------------------------------------
env |- e1 e2 --> n+1
env |- e1 --> pred env |- e2 --> 0
(7) -----------------------------------------
env |- e1 e2 --> 0
env |- e1 --> pred env |- e2 --> n+1
-------------------------------------------
env |- e1 e2 --> n
env |- e1 --> iszero env |- e2 --> 0
(8) ---------------------------------------
env |- e1 e2 --> true
env |- e1 --> iszero env |- e2 --> n+1
-----------------------------------------
env |- e1 e2 --> false
(In these rules, n stands for a non-negative integer.) For example, to evaluate
if iszero 0 then 1 else 2
we must, by rules (4) and (5), first evaluate iszero 0. By rule (8) (and rules (3) and (1)), this
evaluates to true. Finally, by rule (4) (and rule (1)), the whole program evaluates to 1.The
following rule describes variable evaluation
env(x) = v (i.e. lookup x in env )
(9) ----------------------------------------
env |- id x --> v
Just like the built-in functions (succ, pred, and iszero), functions defined using fn evaluate
to themselves:
4
Spring 2020 Assignment 4 (Interpreters)
CIS 425
April 2020
(10) env |- (fn x => e) --> (fn x => e)
Computations occur when you apply these functions to arguments. The following rule defines
call-by-value (or eager ) function application, also used by SML:
env |- e1 --> (fn x => e) env |- e2 --> v1 env[x = v1] |- e --> v
(11) -----------------------------------------------------------------------
env |- e1 e2 --> v
The above rule says that in order to evaluate an application e1 e2 in an environment env,
we first evaluate e1 and e2 in the same environment, if e1 and e2 evaluate to fn x => e and
v1 then the environment env is extended by binding variable x to v1, and in that extended
environment one evaluates the body e of the function. If that returns v then v is the result
of the application.
Similarly, the last rule implements let.
env |- e1 --> v1 env[x = v1] |- e --> v
(12) -----------------------------------------------
env |- let x = e1 in e end --> v
1 Problem 1
First, convince yourself that the above rules give semantics to a dynamically scoped call-byvalue
language. Then, using the above rules write an interpreter,
interp: (env * term) -> result
Do not assume that programs have been typed checked before, this means that you will need
to return error terms for type errors like succ true. Here is a skeleton file (interp.sml)
to help you to get started. It contains an implemented environment datatype and related
functions, as well as a mostly unimplemented interp function. Once you’ve implemented
your interpreter, you can test it with some of the examples in this file: interpExamples.sml.
2 Problem 2
Your next step is to implement a call-by-value statically scoped language. To that end, let
us change the semantics of functions by introducing the notion of a closure as follows:
(10a) env |- (fn x => e) --> ((fn x => e), env)
5
Spring 2020 Assignment 4 (Interpreters)
CIS 425
April 2020
Notice that we save the environment in the return value. This environment will be used when
we invoke the function:
env |- e1-->((fn x => e), env1) env |- e2-->v1 env1[x=v1]|- e-->v
(11)-------------------------------------------------------------------------
env |- e1 e2 --> v
As explained in the above rules, in order to achieve static scoping, you will need to add
closures to our language. You can do this by adding a RES CLOSURE tag to our result
type, which contains both a function and an environment. Write a new statically scoped
interpreter
interp_static: (env * term) -> result
You should be able to copy a lot of the code from interp. NOTE: In constructing your
closure, you may need to use mutually recursive datatype definitions. While SML generally
requires datatype definitions to come before their uses, you can define two datatypes at the
same time using the “and” keyword. For example:
datatype foo = FOO of int | FOOBAR of bar
and bar = BAR of bool | BARFOO of foo
6
CIS 425
April 2020
In this assignment, you will develop an SML interpreter for a small functional language called
PCF, which stands for Programming language for Computable Functions. The language is
relatively simple, yet powerful, with arithmetic expressions and functions. The syntax of
PCF programs is given by the following BNF grammar:
e ::= x | n | true | false | succ | pred | iszero | if e then e else e |
fn x => e | e e | (e) | let x = e in e
In the above, x stands for an identifier; n stands for a non-negative integer literal; true and
false are the boolean literals; succ and pred are unary functions that add 1 and subtract 1
from their input, respectively; iszero is a unary function that returns true if its argument is
0 and false otherwise; if e1 then e2 else e3 is a conditional expression; fn x => e is a
function with parameter x and body e; e e is a function application; (e) allows parentheses
to be used to control grouping; and let x=e1 in e2 is a let expression.
It should be clear to you that the above grammar is quite ambiguous. For example, should
fn f => f f be parsed as fn f => (f f) or as (fn f => f) f? We can resolve such
ambiguities by adopting the following conventions (which are the same as in SML):
• Function application associates to the left. For example, e f g is (e f) g, not e (f g).
• Function application binds tighter than if, and fn. For example, fn f => f 0 is
fn f => (f 0), not (fn f => f) 0.
We don’t want to interpret concrete syntax directly. Instead, the interpreter will work on
a parse tree (also called abstract syntax tree ) representation of the program; these syntax
trees will be values of the following SML datatype:
datatype term = AST_ID of string | AST_NUM of int | AST_BOOL of bool
| AST_SUCC | AST_PRED | AST_ISZERO | AST_IF of term * term * term
| AST_FUN of string * term | AST_APP of term * term
| AST_LET of (string * term * term)
| AST_ERROR of string
This definition mirrors the BNF grammar given above; for instance, the constructor AST_ID
makes a string into an identifier, and the constructor AST_FUN makes a string representing
the formal parameter and a term representing the body into a function. Note that there is
no abstract syntax for (e); the parentheses are just used to control grouping.
Practice1
Write the PCF abstract syntax tree term corresponding to the following PCF source expressions
(do this manually so that you understand; later, use your PCF parser to confirm your
answers).
1You do not have to submit anything for this part
1
Spring 2020 Assignment 4 (Interpreters)
CIS 425
April 2020
• (a) 123
• (b) (fn x => x ) 123
• (c) if iszero x then x else 0
Continuing
You will be building an interpreter that will evaluate Abstract Syntax Trees (ASTs) for PCF
to a final AST that represents a computed result.
Instead of building the parse trees for arithmetic expressions by hand (as in the previous
problem), we are providing you with a parser that converts from concrete PCF syntax to an
abstract syntax tree. The parser is available parser.sml. Include the command
use "parser.sml";
at the beginning of the file containing your interpreter. The parser defines the datatype term
as well as two useful functions, parsestr and parsefile. Function parsestr takes a string
and returns the corresponding abstract syntax; for example
- parsestr "iszero (succ 7)";
val it = AST_APP (AST_ISZERO,AST_APP (AST_SUCC,AST_NUM 7)) : term
Function parsefile takes instead the name of a file and parses its contents. (By the way,
the parser is a recursive-descent parser; you may find it interesting to study how it works.)
You are to write an SML function interp that takes an abstract syntax tree represented as
a term as well as an environment, represented as an env, and returns the result of evaluating
it, as a result. Initially, we will define our result datatype as follows:
datatype result = RES_ERROR of string | RES_ERROR of string | RES_NUM of int
| RES_BOOL of bool | RES_SUCC | RES_PRED | RES_ISZERO
| RES_FUN of (string * term);
The evaluation should be done according to the rules given below. (Rules in this style are
known in the research literature as a natural semantics.) The rules are based on judgments
of the form
env |- e --> v
which means that term e evaluates to value v (and then can be evaluated no further). For the
sake of readability, we describe the rules below using the concrete syntax of PCF programs;
remember that your interp program will actually need to work on SML values of type term.
2
Spring 2020 Assignment 4 (Interpreters)
CIS 425
April 2020
Environments
Interpreters also need a way of passing parameters to user-defined functions. In our interpreter,
we will be using environments. An environment is at its core, a set of relations, from
names to values. Whenever a term is evaluated, it will be done in the context of an environment.
This environment must be extendable to allow new variables to be bound, and it
must be searchable, to allow bound variables to be later retrieved. For example, if we were
to evaluate the expression:
We would start with an empty environment (). When we come to the first let expression,
we would add the relation (x,4) to our environment, and evaluate the body of the let in
that context. Similarly, when we come to the second let expression, we add (y,5) to our
environment, and evaluate its body in the further extended environment. Thus, when we
come to the expression x+y, we evaluate it in the environment ((x,4), (y,5)). In order to
determine the values of x and y, we merely look them up.
In the rules below, each judgement will occur in the context of an environment. For this
assignment, you will be provided with an environment implementation, so you won’t have to
write one yourself.
Rules The first few rules are uninteresting; they just say that basic values evaluate to
themselves:
(1) env |- n --> n, for any non-negative integer literal n
(2) env |- true --> true and env |- false --> false
(3) env |- succ --> succ, env |- pred --> pred, and env |- iszero --> iszero.
The interesting evaluation rules are a bit more complicated, because they involve hypotheses
as well as a conclusion. For example, here’s one of the rules for evaluating an if-then-else:
env |- b --> true env |- e1 --> v
(4) -----------------------------------------
env |- if b then e1 else e2 --> v
In such a rule, the judgments above the horizontal line are hypotheses and the judgment
below is the conclusion. We read the rule from the bottom up: “if the expression is an
3
Spring 2020 Assignment 4 (Interpreters)
CIS 425
April 2020
if-then-else with components b, e1, and e2, and b evaluates to true and e1 evaluates to v,
then the entire expression evaluates to v”. Of course, we also have the symmetric rule:
env |- b --> false env |- e2 --> v
(5) ------------------------------------------
env |- if b then e1 else e2 --> v
The following rules define the behavior of the built-in functions:
env |- e1 --> succ env |- e2 --> n
(6) ------------------------------------------
env |- e1 e2 --> n+1
env |- e1 --> pred env |- e2 --> 0
(7) -----------------------------------------
env |- e1 e2 --> 0
env |- e1 --> pred env |- e2 --> n+1
-------------------------------------------
env |- e1 e2 --> n
env |- e1 --> iszero env |- e2 --> 0
(8) ---------------------------------------
env |- e1 e2 --> true
env |- e1 --> iszero env |- e2 --> n+1
-----------------------------------------
env |- e1 e2 --> false
(In these rules, n stands for a non-negative integer.) For example, to evaluate
if iszero 0 then 1 else 2
we must, by rules (4) and (5), first evaluate iszero 0. By rule (8) (and rules (3) and (1)), this
evaluates to true. Finally, by rule (4) (and rule (1)), the whole program evaluates to 1.The
following rule describes variable evaluation
env(x) = v (i.e. lookup x in env )
(9) ----------------------------------------
env |- id x --> v
Just like the built-in functions (succ, pred, and iszero), functions defined using fn evaluate
to themselves:
4
Spring 2020 Assignment 4 (Interpreters)
CIS 425
April 2020
(10) env |- (fn x => e) --> (fn x => e)
Computations occur when you apply these functions to arguments. The following rule defines
call-by-value (or eager ) function application, also used by SML:
env |- e1 --> (fn x => e) env |- e2 --> v1 env[x = v1] |- e --> v
(11) -----------------------------------------------------------------------
env |- e1 e2 --> v
The above rule says that in order to evaluate an application e1 e2 in an environment env,
we first evaluate e1 and e2 in the same environment, if e1 and e2 evaluate to fn x => e and
v1 then the environment env is extended by binding variable x to v1, and in that extended
environment one evaluates the body e of the function. If that returns v then v is the result
of the application.
Similarly, the last rule implements let.
env |- e1 --> v1 env[x = v1] |- e --> v
(12) -----------------------------------------------
env |- let x = e1 in e end --> v
1 Problem 1
First, convince yourself that the above rules give semantics to a dynamically scoped call-byvalue
language. Then, using the above rules write an interpreter,
interp: (env * term) -> result
Do not assume that programs have been typed checked before, this means that you will need
to return error terms for type errors like succ true. Here is a skeleton file (interp.sml)
to help you to get started. It contains an implemented environment datatype and related
functions, as well as a mostly unimplemented interp function. Once you’ve implemented
your interpreter, you can test it with some of the examples in this file: interpExamples.sml.
2 Problem 2
Your next step is to implement a call-by-value statically scoped language. To that end, let
us change the semantics of functions by introducing the notion of a closure as follows:
(10a) env |- (fn x => e) --> ((fn x => e), env)
5
Spring 2020 Assignment 4 (Interpreters)
CIS 425
April 2020
Notice that we save the environment in the return value. This environment will be used when
we invoke the function:
env |- e1-->((fn x => e), env1) env |- e2-->v1 env1[x=v1]|- e-->v
(11)-------------------------------------------------------------------------
env |- e1 e2 --> v
As explained in the above rules, in order to achieve static scoping, you will need to add
closures to our language. You can do this by adding a RES CLOSURE tag to our result
type, which contains both a function and an environment. Write a new statically scoped
interpreter
interp_static: (env * term) -> result
You should be able to copy a lot of the code from interp. NOTE: In constructing your
closure, you may need to use mutually recursive datatype definitions. While SML generally
requires datatype definitions to come before their uses, you can define two datatypes at the
same time using the “and” keyword. For example:
datatype foo = FOO of int | FOOBAR of bar
and bar = BAR of bool | BARFOO of foo
6