search

kevinsullivan / cs6501s23

Formal Mathematics for Software Design
6 stars 6 forks source link

Chapter 2.1.5 - Clarifying Writing #31

Open RoboticMind opened 1 year ago

RoboticMind commented 1 year ago

2.1.5

Total functions and natural numbers are not defined before they are used. Perhaps this can be rewritten:

In this case, there is total function from terms of type bal to ℕ, so we can specify the semantics as a function in Lean. (All functions in Lean represent total functions in mathematics.)

to be more like this:

In this case, this is a function from terms of type bal to ℕ (positive whole numbers). This is also total because all inputs (the strings) have a defined output (their depth). We can use that to specify the semantics as a function in Lean. (All functions in Lean represent total functions in mathematics)

This paragraph is a little tricky to read without background in lean. This may also be a good place for a visual. I could help create one here if you would like that

The function is defined by case analysis on the argument. If it is the empty string, mk_empty, the function returns 0. Otherwise (the only remaining possibility) is that the value to which sem is applied is of the form (mk_nonempty l b r) where l and r are values representing left and right parenthesis, and where b is some smaller string/value of type bal. In this case, the nesting depth of the argument is one more than the nesting depth of b, which we compute by applying bal recursively to b.

Perhaps something along the lines of:

The function is defined by giving values base on the possible ways the given string could be have been constructed. This is called case analysis. If it is the empty string, mk_empty, the function returns 0 since the empty string has no depth. Otherwise (the only remaining possibility) is that the value was constructed from combined some other string with parenthesis. In our code that means using mk_nonempty l b r where l and r are values representing left and right parenthesis, and where b is some smaller string/value of type bal. In this case, the nesting depth of the argument is one more than the nesting depth of b, so we can compute the depth by applying bal recursively to `b.