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