Good Luck!
Function x -> y + 1 ~= Function y
-> x + 1f x + x ~= x + f x
True,
False, and If-Then-Else that use variants
and don't use the built-in Fb booleans. Note that
you may not simply use the Church encodings using only functions for
your answer, you must make fundamental use of variants to accomplish
your encoding.
Let super = ... In
{
getX = super.getX; (* inherited, not overridden *)
getY = super.getY; (* inherited, not overridden *)
setX = Function this -> Function _ -> count := !count + 1;
super.setX this _ (* override *)
...
}
Method overloading, on the other hand, is the process by which
the same name can represent multiple different methods, such as in
the following Java-like code:
public class FooBar
{
public int foo(int x) {
return x + 1;
}
public int foo(int x, int y) {
return x + y;
}
}
The compiler then decides which of the methods to call based upon the
types of the arguments it observes. How could method overloading be
encoded in FbSR? Encode the above FooBar class example to show
your method.
cheapY which works like the
Y-combinator but only supports ten levels deep of recursive
call. So for example
cheapY (Function this -> Function x ->
If x = 1 then 1 Else x + this (x-1)) 10
returns 55 but if the 10 was replaced with
11 it diverges since the recursion tried to go 11
levels deep. This behavior is the same as a
recursive function invocation with a runtime stack depth of at
most 10 in e.g. the C language. Hint: you don't actually need a
counter to count the number of recursive calls, its easier than that.
=.= was
replaced with the following two rules:
e1 and e2 are identical integers
------------------------------------
e1 = e2 ==> True
plus
e1 and e2 are both integers but are not identical
-------------------------------------------------------
e1 = e2 ==> False
This would in fact be a pretty bad set of rules to have; give an example
program which would suffer if this was the = rule.
= was
replaced with the following two rules:
e1 ==> v e2 ==> v
-------------------------
e1 = e2 ==> True
plus
e1 ==> v e2 ==> v' v is not identical to v'
--------------------------------------------------
e1 = e2 ==> False
This rule set looks very nice but it also has a big problem, not in terms
of how programs run but how it would mess up operational
equivalence. Assuming we used our usual Fb
definition of operational equivalence for this modified
language, give an example of an operational equivalence that
held for Fb (and rightly so), but which would
no longer hold using these new rules. =. Note the context C could
include =. Feel free to use the same answer for b)
and c) if it satisfies both questions.
checkpoint and snapback which are
expressions (not values). Executing checkpoint makes a
full checkpoint of the current state; later on if
snapback is ever executed it rolls back all of the
values that were checkpointed to their old checkpointed values. We
will call this new language FbSnap. For this
question you are to write the operational semantics rules for
FbSnap. Since there are many rules you only need
to give the rules for function application, assignment :=,
checkpoint,
and snapback.
Here are answers to a few questions you
may have. First, start with the FbS operational
semantics as your basis. Note that any newly allocated locations should still be
kept around at snapback -- new memory locations could have been allocated since
the previous checkpoint and variables could reference them, so only
snap back for the things that existed back then. The
checkpoint is global in the sense that a second checkpointing just
overwrites any previous checkpoint if any. (Hint: the operational semantics execution
state should be a triple here, not a pair as was the case in FbS.)
Here are a few examples of evaluations (only showing the initial and
final values, not the full state).
Let x = Ref 5 In
(checkpoint; x := 3; snapback; !x) returns 5
checkpoint; Let x = Ref 5 In
(snapback; !x) returns 5 (* checkpoint empty *)
Let x = Ref 5 In
(snapback; !x) returns 5 (* no checkpoint same as empty *)
Let x = Ref 5 In
(checkpoint; x := 3; checkpoint; x := 6; snapback; !x) returns 3
null is of a special type (the null type). The
keyword null represents the only value of this special type. The null
value may be used in place of values of any reference type; for
instance, the keyword null may be used where a String is expected. We
use the set of values from Fb and add the value
Null. Operations which make use of Null will
diverge; for instance, Null + 1 =/> and Null And True
=/>. We also introduce the keyword IsNull which
tests whether or not a value is Null. For example,
IsNull Null ==> True and IsNull 5 ==> False.
Null). The value Null has the type Null (just as
the value 5 has the type Int). However, we can use
Null whenever any other type is expected. For instance,
(Function x:Int -> 4) Null ==> 4 even though Null
is not an Int. We cannot use other types in place of
Null; for instance, (Function x:Null -> 4) 0 =/>.
If-Then-Else,
and function application, as well as any new rules needed in
TFbN for which there was no analogous
TFb rule.
Null). For example, (Function f -> f Null) has type ('a ->
'b) -> 'b \ emptyset -- observe that the use of a Null argument did
not assign the type Null to the function so the inferred type
for f is pretty much completely unconstrained.
If-Then-Else,
function application, and any new rules plus any changes to closure or
consistency. (Hint: its a good idea for Function x ->
Null to have type 'a -> 'b \ emptyset).