Homework Assignment 3 Due Tuesday, Feb 20th at 11:59PM (Pacific Time)
In this assignment, we will continue to augment . This time, we will add booleans, lists, and recursion. This homework will consist of four parts.
The first part gives you lots of practice with the syntax and the operational semantics of the augmented language.
The second part is where you will implement the language extensions for the interpreter.
The third part is a small hacking exercise in which you will reverse-engineer the operational semantics for a brand new language extension.
The fourth part (bonus) shows you how to use the same recipe from last HW to encode all kinds of fancy data structures into -calculus.
The final part will culminate in a self-interpreter for -calculus. Instructions
0. Makesureyoudownloadthelatestversionofthereferencemanualusingthislink.
1. Eitherclonethisdirectory,ordownloadthezippeddirectoryusingthislink.
2. You will be modifying lib/lamp/eval.ml , and (for bonus) lib/meta/encodings.txt by replacing the
placeholders denoted by todo , hmm , or bonus with your own code.
3. Youmustnotchangethetypesignaturesoftheoriginalfunctions.Otherwise,yourprogramwillnot
compile. If you accidentally change the type signatures, you can refer to the corresponding .mli file to
see what the expected type signatures are.
4. Onceyou’redone,runmake,whichwillcreateanarchivecalledsubmission.zipcontaining
lib/lamp/eval.ml , and (for bonus) lib/meta/encodings.txt . Submit the zip file to Gradescope. If your program contains print statements, please remove them before submitting. You do not need to submit any other file, including any .mli file or test code. The autograder will automatically compile your code together with our testing infrastructure and run the tests.
Important Notes
There will be 1 exercise that will be graded. Please do not forget to submit your solution to
Gradescope. The remaining exercises are ungraded.
Problems marked with are programming tasks, and will be autograded on Gradescope. In solving those problems:
You are not allowed to use in built-in OCaml library functions in your solutions, except for String.equal , ^ (for string concatenation), and Int.to_string (to convert an int into a string ). If you do, you will not be awarded any points. Note that language features like pattern-
matching do not count as library functions. You may use library functions like Fmt.pr to test your code, but you must remove them before submitting.
You are not allowed to use any kind of imperative features, including mutable state (e.g.
references and arrays), loops, etc. If you do, you will not be awarded any points.
Problems marked with bonus are optional. You will receive extra credit by solving them. You will not be tested on them in the midterm.
The actual programming problems were designed so that you won’t need to write more than 100 lines of code in total, but they do require a solid grasp of the concepts covered in lectures and in sections.
If you are struggling, please do not hesitate to ask questions in the #hw3 Slack channel or come to office hours.
We have provided one unit test for each programming problem. To run all unit tests, simply run
1 duneruntest
in the root directory of this homework. This will compile your programs and report tests that fail.
We highly encourage you to add your own tests, since the autograder won’t show you what the official test cases are (only the identifiers of passed/failed cases will be shown). You can locate the provided test cases in test/test_lamp.ml .
Part 1: Language Extensions 1.1 Concrete Syntax
Let’s augment with booleans, lists, and the fixed-point operator (to express recursive definitions). Please see the Overview section of the language reference manual for an informal discussion of the meaning and the concrete syntax of those language extensions. The new syntactic forms should be quite similar to OCaml.
Several things to note:
1. Recursivefunctiondefinitionsarede-sugaredintoacombinationoflet,lambda,andfix.For example, the following recursive definition
will be de-sugared into
fun rec fact with n =
if n = 0 then 1
else n * fact (n-1) in
let fact = fix fact is lambda n.
if n = 0 then 1
else n * fact (n-1) in
The de-sugaring procedure works as follows:
1. First, we ignore the rec keyword, and de-sugar the function definition as if it were non-recursive
into a combination of let and lambda . That is, we de-sugar
2. Then, we wrap the lambda function with fix f is … . That is, we replace lambda n. if n = 0 then 1 else n * fact (n-1) with a wrapped version using fix fact is … , which gives us
2. Pattern-match on lists must end with the end keyword, unlike in OCaml.
3. Youcanonlycompareintegersforequality.Booleanandlistequalitycaneasilybeimplementedwith custom functions, so we don’t include them as built-in features to make the core language as compact as possible.
1.2 Abstract Syntax
We will augment the AST of as follows:
fun fact with n =
if n = 0 then 1
else n * fact (n-1)
1 letfact=lambdan.ifn=0then1elsen*fact(n-1) 2 in…
1 letfact=fixfactislambdan.ifn=0then1elsen*fact(n-1) 2 in…
1 2 3 4 5 6 7 8 9
type expr =
(* as before *)
(* booleans *)
| IfThenElse of expr * expr * expr
| Comp of relop * expr * expr
(* lists *)
| Cons of expr * expr
| Match of expr * expr * expr
or booleans,
True and False represent the boolean constants “true” and “false” respectively IfThenElse(e1, e2, e3) represents the if-then-else expression if e1 then e2 else e3 Comp(op, e1, e2) represents the comparison e1 op e2 , where op is a comparison operator.
The comparison operators are Eq , Lt , and Gt . For lists,
Nil represents the empty list
Cons(e1, e2) represents the cons cell e1 :: e2 , i.e., making a new list whose head is e1 and
whose tail is e2
Match(e1, e2, e3) represents list pattern-matching as in match e1 with Nil -> e2 | x::xs -> e3 end . Note that the second branch of the match involves binding: the head of the list is bound to name “x” and the tail bound to “xs”. Therefore, the third argument of the Match constructor will always be two nested Scope constructors. For example, the concrete syntax
match e1 with Nil -> e2 | x::xs -> e3 end is represented as 1 Match(e1,e2,Scope(“x”,Scope(“xs”,e3)))
If the third argument does not have this form, then we say the AST is malformed. Examples of malformed Match includes:
1 2 3 4 5 6
(* the cons branch isn’t a scoped binding: *)
Match(.., .., Num 1)
(* the cons branch only declares one variable: *)
Match(.., .., Scope(“x”, Num 1))
(* the nil branch shouldn’t have binding: *)
Match(.., Scope(“x”, Num 2), …)
For recursion, the Fix constructor represents the fixed-point operator. Fix also has a binding structure: it declares the name of the recursive function to be in-scope in the function definition. Thus,
Fix(Scope(“f”, ..)) is well-formed, while Fix(Num 3) is not. Problem ( ): Parse the following expressions in concrete syntax into ASTs:
1. if if 3=10 then Nil else false then if true then lambda x.x else false else 1 2. 1::(Nil::true)::lambda x.x
Problem ( ): Augment the wf function from last HW to check whether an expression is well-formed in terms of its binding structure:
fun rec length with xs = match xs with Nil -> 0 | _::xs’ -> 1 + length xs’ end in
(* recursion *)
| Fix of expr
length (1::2::3::Nil)
let rec wf (vs: string list) (e: expr) : bool =
match e with
Programming Help
3 4 5 6 7 8 9
10 11 12 13 14
| … (* as before *)
| True -> (* todo *)
| False -> (* todo *)
| IfThenElse (e1, e2, e3) -> (* todo *)
| Comp (op, e1, e2) -> (* todo *)
| Nil -> (* todo *)
| Cons (e1, e2) -> (* todo *)
| Match (e1, e2, Scope (x, Scope (y, e3))) ->
(* todo *)
| Match _ -> false
| Fix (Scope (x, e)) -> (* todo *)
| Fix _ -> false
1.3 Operational Semantics
Problem ( ) For the following expressions, determine whether it is a value or not:
1. lambdax.x+2*y
3. (lambdax.x+2*y)3
5. 1::2::3+4::Nil
6. Nil::(Nil::lambda x.x)::true::1
7. if true then false else true
8. match Nil with Nil -> Nil | _::_ -> Nil end
Problem ( ): Formalize the is-value relation as a set of inference rules. The is-value relation determines whether an expression is a value, and is notated as e val . The following two rules are provided to you:
Your task is to add more rules to the above list to cover all values in as defined by natural language in the Operational Semantics section of the language reference manual.
Your inference rules should be
1. complete, meaning that if is indeed a value in , then the relation e val should be derivable using your rules.
2. sound, meaning that if the relation e val is derivable using your rules, then is indeed a value in .
And the is-value relation defined by your rules should satisfy the following property: e val if and only if .
——— (V-True)
——— (V-True)
Computer Science Tutoring
Problem ( ) When we say , we mean that there exists a value for which we can draw the derivation tree that shows holds using the inference rules. What do we mean when we say
? In which cases can we not draw the derivation tree?
Hint: There are at least two distinct cases.
Problem ( ) For the following expressions , determine whether there exists a value such that . If such a value exists, draw the derivation tree. Otherwise, draw a partial derivation tree and clearly indicate which place(s) of the tree is stuck.
1. (if 3>4 then 5 else 7+10*3) = 10 .
2. let f = lambda x:Bool. if x then false else true in f (10 > 0)
3. 1::10::Nil::Nil
4. (1::10) :: Nil :: Nil
5. match 1::Nil with Nil -> 0 | hd::_ -> hd end
6. match 1::Nil with Nil -> 0 | _::tl -> tl end
7. match 1::2 with Nil -> 3 | x::y -> x+y end
8. letg=fixrecurislambdan.ifn<1then1elserecur(n-1)+recur(n-2)ing2.
(fix recur is lambda xs. match xs with Nil -> 0 | _::ys -> 1 + recur ys end)
(you might want to abbreviate the function body using some symbol in your
10. (fix recur is lambda n. recur (n-1) 10
11. (fix recur is lambda n. n-1) 10
1.4 What if …?
Programming languages and their operational semantics are designed by humans. As such, the human designer will always face a load of design decisions that may lead to systems with different theoretical properties and practical trade-offs.
In this part, we will explore some of the “road not taken” in the design of , and explore their consequences. This will also help you gain a deeper understanding of why is designed the way it is. Finally, similar questions may appear on the midterm, so it’s good to get some practice.
Problem ( ): has the following App rule :
An alternative is to have the following App rule:
(false::true::Nil)
derivation tree)
e1 ↓↓ \lambda x.e1′ e2 ↓↓ v
e1′[x |-> v] ↓↓ v’
———————— (App) (e1 e2) ↓↓ v’
e1 = \lambda x.e1′ e2 ↓↓ v
e1′[x |-> v] ↓↓ v’
———————— (App-Alt1) (e1 e2) ↓↓ v’
where we simply changed the first premise to an equation instead of an evaluation relation.
Let us denote the original evaluation relation as and the alternative evaluation relation in which App is
replaced by App-Alt1 as .
Exhibit an expression such that but , i.e., the evaluation of works fine with the
original rule but gets stuck/doesn’t terminate with the alternative rule.
Hint: Consider the application of “multi-argument” functions.
Problem ( ): Another alternative to the App rule is to have the following rule:
Let us denote the original evaluation relation as and the alternative evaluation relation in which App is replaced by App-Alt2 as .
Exhibit an expression such that but , i.e., the evaluation of gets stuck/doesn’t terminate with the original rule but works fine with the alternative rule.
Hint: What is call-by-value, and what is call-by-name? (You’ve seen these concepts in lectures.)
Problem ( ): The size of a derivation tree can be computed simply by counting the total number of rules used. Note that multiplicities are counted, i.e., if the same rule is used N times, then it contributes N to the total size of the derivation tree. For example, the following tree has size 5:
Exhibit an expression such that evaluates to some value using both and , but the size of the derivation tree for is strictly smaller than the size of the derivation tree for .
In practical terms, this means that any interpreter that implements will take longer to evaluate than an interpreter that implements .
Problem ( ): Let’s consider the rule for evaluating let-expressions:
e1 ↓↓ \lambda x.e1′
e1′[x |-> e2] ↓↓ v ————————– (App-Alt2)
(e1 e2) ↓↓ v
浙大学霸代写 加微信 cstutorcs
e2[x |-> v1] ↓↓ v2 ————————— (Let)
let x = e1 in e2 ↓↓ v2
and the alternative
Let us denote the original evaluation relation as and the alternative evaluation relation in which Let is replaced by Let-Alt as .
e2[x |-> e1] ↓↓ v2 ————————— (Let-Alt)
let x = e1 in e2 ↓↓ v2
1. Does there exists an expression such that but derivation tree for . Then draw the partial derivation tree for gets stuck/gets into infinite loop.
2. Does there exists an expression such that but derivation tree for . Then draw the partial derivation tree for gets stuck/gets into infinite loop.
? If so, find one, and draw the and clearly indicate where it
? If so, find one, and draw the and clearly indicate where it
3. Exhibit an expression such that evaluates to some value using both and derivation tree for is strictly smaller than the size of the derivation tree for
Problem ( ): Recall the list-cons rule:
and consider the alternative
Then, recall the cons case of the list-match rule:
, but the size of the .
e2 ↓↓ v2 ———————— (Cons)
e1::e2 ↓↓ v1::v2
1 ————————(Cons-Alt) 2 e1::e2 ↓↓ e1::e2
1 2 3 4 5 6 7 8
e1 ↓↓ v1::v2
e3[x |-> v1][y |-> v2] ↓↓ v3 ———————— (MatchCons)
match e1 with
| Nil -> e2
| x::y -> e3
Your task is to design a new rule MatchCons-Alt that replaces MatchCons while also being compatible with Cons-Alt :
1 2 3 4 5 6 7 8
———————— (MatchCons-Alt)
match e1 with
| Nil -> e2
| x::y -> e3
Let us denote the original evaluation relation as and the alternative evaluation relation as in which Cons and MatchCons are replaced by Cons-Alt and MatchCons-Alt .
By compatible, we mean that if using the original rules, then we should also have using the alternative rules. That is, for any expression , the new rules should behave the same as the old rules if the old rules indeed evaluates to some value , although the new rules can be more permissive, i.e., may get stuck with the old rules but works fine with the alternative rules.
Problem ( ): Consider which you just defined. Update your rules for the “is-value” relation, such that is a value according to the updated rules if and only if .
Part 2. Augmenting the Interpreter
Problem ( , 40 points) Augment the interpreter you wrote for HW2 with support of booleans, lists, and recursion according to the operational semantics specified in the language reference manual. Specifically, for the free_vars , subst and eval functions:
Copy and paste the code you wrote in the previous assignment for free_vars , subst and eval into lib/lamp/eval.ml .
Fill in todo () with fresh code. Hint: the new cases of free_vars and subst should be trivial; you shouldn’t need to modify Var or Scope .
Ignore hmm () for this problem.
There are two ways to test your interpreter:
1. Weincludedsomeunittestsaswellasacoupleofrealistic programsintest/examples/thatyoucan
use to test your interpreter. Simply run dune runtest .
2. Youcanalsoruntheinterpreterinteractively(REPL)orinfilemodeasdescribedintheprevious assignments. For file mode, do dune exec bin/repl.exe —
1 duneexecbin/repl.exe
We added some convenience commands to the REPL:
CTRL-C interrupts the REPL and initiate a new prompt. This is useful if your interpreter enters an infinite loop, or you simply want to throw away the current input expression and start anew.
CTRL-D quits the REPL.
#let =
1 2 3 4 5 6 7 8 9
10 11 12 13
> #let x = 10
<== x + 1 [eval] ==> 11
> #let x = 20
<== x + 1 [eval] ==> 21
1. ThissyntaxisonlyavailableintheREPLmode.Donotconfuseitwithlet-expressionsinthe language itself, which you implemented in HW2.
2. Laterbindingsmayshadowearlierones,justlikeinOCaml.
#print shows the current binding environment.
#clear resets the binding environment.
#save
#load
Part 3. Semantics Reverse-Engineering
In CS162, we are model citizens who always define the meaning of each language feature precisely using operational semantics rule first, before we proceed to make claims about the language. In this way, we are highly confident that we know exactly what we mean when we express something using this language, and we know for sure we aren’t planting time bombs with our code.
Unfortunately, this style of carefully specifying language semantics is an exception instead of the norm in the real world. Here are some common ways people define a language, ranked by increasing likelihood of imminent disaster:
1. Definealanguagebyprovidingacanonicalinterpreter:Ifwewonderwhatalanguagefeaturemeans, we need to construct an example program containing said feature, and observe the behavior of the program on the official interpreter. Of course, the interpreter itself is written in some other
programming language (so the meaning of the target language fundamentally depends on the meaning of the implementation language, which by itself also needs a definition). Examples include Python, Ruby, and JavaScript.
2. Definealanguagebyprovidingacanonicalcompiler:Ifwewonderwhatalanguagefeaturemeans,we need to construct an example program containing said feature, and run the official compiler on the program to get a low-level program (such as assembly). Then, based on (i) our understanding of the semantics of the low-level language or (ii) the runtime side effect of the low-level program, we infer the meaning of the high-level program. Examples include C, C++, and Rust.
3. Definealanguagebynaturallanguage.Noexamplesareneededhere,andnomoreshallbesaidabout this forbidden dark art. May the gods have mercy on the souls of those who have to maintain such languages.
In this part of the homework, you will get some practice with the first approach. That is, you will be inferring the meaning of a new language extension from a reference interpreter provided to you. However, to bring good to the world, you will also formalize your understanding of the meaning of this language feature into operational semantics rules.
The language extension we are considering is products (aka pairs, tuples, etc.). We introduce one syntactic form that introduces / makes / constructs a product from two elements: { e1, e2 } , and two syntactic forms that eliminates / uses / destructs a product: fst e and snd e . In the AST, the introduction form is represented as Pair of expr * expr , and the elimination forms are represented as Fst of expr and
Snd of expr . None of those constructors have any binding structure.
The reference interpreter on CSIL (located at ~junrui/lamp ) implements products. Your task is to reverse- engineer their operational semantics by experimenting with different example expressions and observing the behavior of the interpreter. Finally, you will formalize your understanding of the semantics of products into a set of inference rules.
Problem ( , GRADED, 10 points): Augment the operational semantics of with rules for products. You should define three rules: one for the introduction form, and one for each of the two elimination forms. You should name the first rule E-Pair , and the second and third rules E-Fst and E-Snd respectively.
For each rule, you should also include 1-2 sentences to informally explain what your rules are doing. In addition, you should ensure that the augmented set of rules is
1. complete, meaning that if the reference interpreter evaluates to , then the relation should be derivable using your rules.
2. sound,meaningthatiftherelation isderivableusingyourrules,thenthereferenceinterpreter should evaluate to .
Note that the above two conditions imply that derivation using your rules should get stuck if and only if the reference interpreter gets stuck.
You can either typeset your solution using LaTeX’s ebproof package (recommended), or hand-write your rules on a piece of paper and take a picture. You can find a LaTeX template for this part of the homework in template.tex. If you take the hand-write route, you must make sure that the writing is clean and legible for the TAs to read.
Once you’re done, submit your rules to the Gradescope assignment called “HW3 (Part 3 Written Problem)”. As an example of using LaTeX’s ebproof package, the following derivation:
can be typeset with
1 2 3 4 5 6 7 8 9
10 11 12 13
\usepackage{ebproof}
\begin{prooftree}
\infer0[\textsc{Int}]{1 \Downarrow 1}
\infer0[\textsc{Int}]{2 \Downarrow 2}
\hypo{1+2 = 3}
\infer3[\textsc{Add}]{1 + 2 \Downarrow 3}
\infer0[\textsc{Int}]{4 \Downarrow 4}
\hypo{3+4 = 7}
\infer3[\textsc{Add}]{(1 + 2) + 4 \Downarrow 7}
\end{prooftree}
where infer
Once you’re satisfied with your rules, you can optionally implement the Pair , Fst , and Snd cases of the eval function, although none of the autograder tests involve those cases.
Part 4. Encoding Recursive Data Structures into – calculus
This part is completely optional.
Total: 4 bonus points
In the previous homework, we have seen how to encode booleans and options into -calculus. We followed a recipe that goes like this:
1. Weobservedthatanydatastructurehastwoaspectsthataredualtoeachother:theintroductionform (i.e. constructors) and the elimination form (i.e. pattern matching).
2. We observed that encoding the introduction form of a type into -calculus was hard, so we started from the elimination form instead.
3. Wewrotedownafunctionthatdoesthesamethingastheeliminationform.Forexample,the elimination form for boolean is
which we translated into an OCaml function as
4. We inspected the type of the elimination form, which for type t would look like 1 valelim_t:t->…
Since we wanted to encode t , we simply defined the encoding of t to be whatever type is on the right- hand-side of the arrow.
For example, the type of elim_bool was
1 bool->’result->’result->’result
so we defined the encoding of bool to be functions of type ‘result -> ‘result -> ‘result , i.e., functions that, given what to do in the then case and what to do in the else case, picks one of them depending on which branch is taken.
5. Wethenderivedtheintroductionformsfromtheeliminationformbyfeedingtheconstructorsintothe elimination function. For example, we derived true_encoding by considering elim_bool true , which had the same behavior as
6. Finally, we translated those OCaml functions into -calculus.
This time, we’ll use the same recipe to derive the -calculus encoding of fancier data structures, like singly linked-lists, binary trees, and the AST of -calculus itself. But we will start with something humbler: natural numbers, which, as we shall see very soon, distills the “essence” of lists, trees, and basically any recursive data structure you can think of.
then do something
else do something
1 letelim_bool(b:bool)(true_case:’result)(false_case:’result):’result= 2 if b then true_case else false_case
1 let true_encoding (true_case: ‘result) (false_case: ‘result) : ‘result = 2 true_case
4.1 Encoding Natural Numbers
Again, we will do some experiments in OCaml before we move on to -calculus. Natural numbers can be defined in OCaml as
1 typenat=Zero|Succofnat
which specifies its introduction forms as Zero and Succ . The Succ constructor takes a natural number as its argument, and gives us back . For example, the number is represented as Succ (Succ (Succ Zero)) .
According to our recipe, the first step is to identify the elimination form of nat , which seems to be
which is largely the same as the elimination form for options.
This pattern-match be easily translated into the following OCaml function:
Intuitively, however, nat seems to be more complicated than option : the only thing we can do with option is to pattern-match on it and see if it’s None or Some . But with nat , we can do much more: we can
also do recursion! For example, here’s the addition function for natural numbers:
Unfortunately, we cannot use elim_nat_nonrec to rewrite add : we also need recursion to do it!
In a previous part of the assignment, you have implemented general recursion using the fixed-point operator fix . However, generality also came at a tremendous cost: fix can be used to express any kind of
recursion, including non-terminating ones! For example, fix f is f is an expression that will never terminate.
In some sense, fix is too powerful. In addition to allowing us to express good old terminating recursion, it also opens the door to all kinds of evil non-terminating recursion. 99% of the time, however, we just need a way to express terminating recursion. For example, just by looking at the syntax of the add function, we know for sure it terminates: it always decreases the first argument n in the recursive call. Since any nat
match n with
| Zero -> do something
| Succ n’ -> do something else with n’ in mind
1 letelim_nat_nonrec(n:nat)(base_case:’result)(succ_case:nat->’result): ‘result =
match n with
| Zero -> base_case
| Succ n’ -> succ_case n’
let rec add (n: nat) (m: nat) : nat =
match n with
| Zero -> m
| Succ n’ -> Succ (add n’ m)
can only have finitely many Succ constructors, the recursion must terminate.
Thus, it would be nice if our elimination form for nat encodes all terminating recursive functions into – calculus, which should allow us to express 99% of what we want to do with nat . If the user really, really, really wants to express non-terminating recursion, they can always use fix in case they are so desperate.
Background note: This exemplifies a good language design principle: instead of allowing the programmer to do anything they want at anytime, the language itself should only expose a set of safe constructs that are guaranteed to well-behaved while also being sufficient for most use cases. If the programmer really wants to do something that can’t be expressed using the safe interface, the language may provide a “jail-break” mechanism that allows the programmer to temporarily disable the protection.
The mutual contract is that, if the programmer decides to jail-break and ends up wreaking havoc, it’s their own fault. But if they use the safe interface and still wreak havoc, it’s the language designer’s fault.
Examples of this principle include the unsafe keyword in Rust which allows the programmer to temporarily break memory safety. Contrast this with C, which allows the programmer to break memory safety (e.g., do pointer arithmetic) at any time and thus no assurances can be made about the safety of C programs whatsoever ̄\_(ツ)_/ ̄
4.2 Primitive Recursion
Our revised goal is thus: we would like an elimination form for nat that permits safe, terminating recursion, which is sufficient for most use cases. Then, we will encode this elimination form into -calculus.
Actually, we claim that you already know how to guarantee a recursion on natural numbers always terminate… when you do induction! If our inductive proofs didn’t “terminate”, then we would not be proving anything at all! We will use this observation to derive the elimination form for nat .
The structure of an inductive proof on some statement is as follows:
We show that holds
Assuming we have a proof of , we use this proof to make a new proof that shows holds.
Note that this is the same structure of (bottom-up) divide-and-conquer algorithms:
We first compute the base case
Assume we have a solution to the sub-problem of size . That is, assume we get our hands on what should be. We then use to make a solution to the original problem of size , which is .
It is actually not too difficult to update our previous elim_nat to handle this pattern! Recall that we had
1 2 3 4 5 6 7 8 9
let elim_nat_nonrec
(base_case: ‘result)
(succ_case: nat -> ‘result)
: ‘result =
match n with
| Zero -> base_case
| Succ n’ -> succ_case n’
The only missing piece is that, in the Succ case, the function succ_case only had access to the number in order to compute the result of . However, the induction/recursion principle suggests that we can strengthen it to give the result of recursively computed , aka the inductive hypothesis! So our
new elim_nat will look li