|
1 | 1 | (* **************************************************************************** |
2 | 2 |
|
3 | | - by Brian Beckman. License the same as for mathics. |
| 3 | + by Brian Beckman. License the same as for Mathics3: GPL3. |
4 | 4 |
|
5 | 5 | Oct 2020 |
6 | 6 |
|
|
32 | 32 | (* Section 1.2 Textual substitution, page 8 |
33 | 33 | _____ _ _ ___ _ _ _ _ _ _ |
34 | 34 | |_ _|____ _| |_ _ _ __ _| | / __|_ _| |__ __| |_(_) |_ _ _| |_(_)___ _ _ |
35 | | - | |/ -_) \ / _| || / _` | | \__ \ || | '_ (_-< _| | _| || | _| / _ \ ' \ |
36 | | - |_|\___/_\_\\__|\_,_\__,_|_| |___/\_,_|_.__/__/\__|_|\__|\_,_|\__|_\___/_||_| |
| 35 | + | |/ -_) \ / _| || / _` | | |__ \ || | '_ (_-< _| | _| || | _| / _ \ ' \ |
| 36 | + |_||___/_|_||__||_,_|__,_|_| |___/|_,_|_.__/__/|__|_||__||_,_||__|_|___/_||_| |
37 | 37 |
|
38 | 38 | Mathics gives us direct syntax for Gries & Schneider's (G&S)'s "textual |
39 | 39 | substitution:" |
|
245 | 245 |
|
246 | 246 | (* Inference Rule Substitution (1.1), page 10 |
247 | 247 | ___ __ ___ _ _ |
248 | | -|_ _|_ _ / _|___ _ _ ___ _ _ __ ___ | _ \_ _| |___(_) |
249 | | - | || ' \| _/ -_) '_/ -_) ' \/ _/ -_) | / || | / -_)_ |
250 | | -|___|_||_|_| \___|_| \___|_||_\__\___| |_|_\\_,_|_\___(_) |
| 248 | +|_ _|_ _ / _|___ _ _ ___ _ _ __ ___ | _ |_ _| |___(_) |
| 249 | + | || ' || _/ -_) '_/ -_) ' |/ _/ -_) | / || | / -_)_ |
| 250 | +|___|_||_|_| |___|_| |___|_||_|__|___| |_|_||_,_|_|___(_) |
251 | 251 | ___ _ _ _ _ _ _ |
252 | 252 | / __|_ _| |__ __| |_(_) |_ _ _| |_(_)___ _ _ |
253 | | -\__ \ || | '_ (_-< _| | _| || | _| / _ \ ' \ |
254 | | -|___/\_,_|_.__/__/\__|_|\__|\_,_|\__|_\___/_||_| |
| 253 | +|__ | || | '_ (_-< _| | _| || | _| / _ | ' | |
| 254 | +|___/|_,_|_.__/__/|__|_||__||_,_||__|_|___/_||_| |
255 | 255 |
|
256 | 256 | The inference rule 'Substitution' takes in a top-line expression e, a list |
257 | 257 | of variables v, and a corresponding list of replacement expressions f, and |
|
335 | 335 | (* Section 1.3 Textual substitution and equality, page 11 |
336 | 336 | _____ _ _ ___ _ _ _ _ _ _ |
337 | 337 | |_ _|____ _| |_ _ _ __ _| | / __|_ _| |__ __| |_(_) |_ _ _| |_(_)___ _ _ |
338 | | - | |/ -_) \ / _| || / _` | | \__ \ || | '_ (_-< _| | _| || | _| / _ \ ' \ |
339 | | - |_|\___/_\_\\__|\_,_\__,_|_| |___/\_,_|_.__/__/\__|_|\__|\_,_|\__|_\___/_||_| |
| 338 | + | |/ -_) | / _| || / _` | | |__ | || | '_ (_-< _| | _| || | _| / _ | ' | |
| 339 | + |_||___/_|_||__||_,_|__,_|_| |___/|_,_|_.__/__/|__|_||__||_,_||__|_|___/_||_| |
340 | 340 | _ ___ _ _ _ |
341 | 341 | __ _ _ _ __| | | __|__ _ _ _ __ _| (_) |_ _ _ |
342 | | -/ _` | ' \/ _` | | _|/ _` | || / _` | | | _| || | |
343 | | -\__,_|_||_\__,_| |___\__, |\_,_\__,_|_|_|\__|\_, | |
| 342 | +/ _` | ' |/ _` | | _|/ _` | || / _` | | | _| || | |
| 343 | +|__,_|_||_|__,_| |___|__, ||_,_|__,_|_|_||__||_, | |
344 | 344 | |_| |__/ |
345 | 345 |
|
346 | 346 | Going forward, we want more inference and less evaluation. This is tricky in |
@@ -1054,8 +1054,8 @@ over and over (google "don't repeat yourself"), introduce "Postfix notation |
1054 | 1054 | (* Here is a cheat sheet of all the rules we've defined so far. |
1055 | 1055 | ___ _ _ ___ _ _ __ |
1056 | 1056 | / __| |_ ___ __ _| |_ / __| |_ ___ ___| |_ ___ ___ / _|__ _ _ _ |
1057 | | -| (__| ' \/ -_) _` | _| \__ \ ' \/ -_) -_) _| (_-</ _ \ | _/ _` | '_| |
1058 | | - \___|_||_\___\__,_|\__| |___/_||_\___\___|\__| /__/\___/ |_| \__,_|_| |
| 1057 | +| (__| ' |/ -_) _` | _| |__ | ' |/ -_) -_) _| (_-</ _ | | _/ _` | '_| |
| 1058 | + |___|_||_|___|__,_||__| |___/_||_|___|___||__| /__/|___/ |_| |__,_|_| |
1059 | 1059 |
|
1060 | 1060 | (* 1.1 *) substitutionInferenceRule[e_, v_:List, f_:List] := |
1061 | 1061 | Module[{ rules = MapThread[ Rule, {v, f} ] }, e /. rules ] |
@@ -1091,13 +1091,13 @@ over and over (google "don't repeat yourself"), introduce "Postfix notation |
1091 | 1091 |
|
1092 | 1092 | (* Section 1.4 Leibniz's rule and function evaluation, page 13 |
1093 | 1093 | _ _ _ _ _ ___ _ _ |
1094 | | -| | ___(_) |__ _ _ (_)__( )___ | _ \_ _| |___ __ _ _ _ __| | |
1095 | | -| |__/ -_) | '_ \ ' \| |_ //|_ / | / || | / -_) / _` | ' \/ _` | |
1096 | | -|____\___|_|_.__/_||_|_/__| /__| |_|_\\_,_|_\___| \__,_|_||_\__,_| |
| 1094 | +| | ___(_) |__ _ _ (_)__( )___ | _ |_ _| |___ __ _ _ _ __| | |
| 1095 | +| |__/ -_) | '_ | ' || |_ //|_ / | / || | / -_) / _` | ' |/ _` | |
| 1096 | +|____|___|_|_.__/_||_|_/__| /__| |_|_||_,_|_|___| |__,_|_||_|__,_| |
1097 | 1097 | ___ _ _ ___ _ _ _ |
1098 | 1098 | | __| _ _ _ __| |_(_)___ _ _ | __|_ ____ _| |_ _ __ _| |_(_)___ _ _ |
1099 | | -| _| || | ' \/ _| _| / _ \ ' \ | _|\ V / _` | | || / _` | _| / _ \ ' \ |
1100 | | -|_| \_,_|_||_\__|\__|_\___/_||_| |___|\_/\__,_|_|\_,_\__,_|\__|_\___/_||_| |
| 1099 | +| _| || | ' |/ _| _| / _ | ' | | _|| V / _` | | || / _` | _| / _ | ' | |
| 1100 | +|_| |_,_|_||_|__||__|_|___/_||_| |___||_/|__,_|_||_,_|__,_||__|_|___/_||_| |
1101 | 1101 |
|
1102 | 1102 | Start at the bottom of page 13. A lot of this we can do without prose, now, |
1103 | 1103 | because we're getting accustomed to the style. |
@@ -1524,9 +1524,9 @@ calculus is (from page 42) |
1524 | 1524 |
|
1525 | 1525 | (* Section 1.6, The assignment statement, page 16 |
1526 | 1526 | _ _ _ |
1527 | | - /_\ _____(_)__ _ _ _ _ __ ___ _ _| |_ |
1528 | | - / _ \ (_-<_-< / _` | ' \| ' \/ -_) ' \ _| |
1529 | | -/_/ \_\/__/__/_\__, |_||_|_|_|_\___|_||_\__| |
| 1527 | + /_| _____(_)__ _ _ _ _ __ ___ _ _| |_ |
| 1528 | + / _ | (_-<_-< / _` | ' || ' |/ -_) ' | _| |
| 1529 | +/_/ |_|/__/__/_|__, |_||_|_|_|_|___|_||_|__| |
1530 | 1530 | |___/ |
1531 | 1531 |
|
1532 | 1532 | Here we exhibit the first instance of a "type." It's just a head and some |
@@ -1675,8 +1675,8 @@ enclosing our variables in curly braces (List brackets). |
1675 | 1675 | (* Exercises for Chapter 1, pages 21-23 |
1676 | 1676 | ___ _ ___ _ _ |
1677 | 1677 | | __|_ _____ _ _ __(_)___ ___ ___ / __| |_ / | |
1678 | | -| _|\ \ / -_) '_/ _| (_-</ -_|_-< | (__| ' \ _ | | |
1679 | | -|___/_\_\___|_| \__|_/__/\___/__/ \___|_||_(_) |_| |
| 1678 | +| _|| | / -_) '_/ _| (_-</ -_|_-< | (__| ' | _ | | |
| 1679 | +|___/_|_|___|_| |__|_/__/|___/__/ |___|_||_(_) |_| |
1680 | 1680 |
|
1681 | 1681 | *************************************************************************** *) |
1682 | 1682 |
|
|
0 commit comments