-
Notifications
You must be signed in to change notification settings - Fork 59
/
Copy pathc1_grounded_basic.metta
165 lines (146 loc) · 5.06 KB
/
c1_grounded_basic.metta
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; The standard library contains a few basic grounded operations
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Implementation of grounded arithmetics may change location,
; but these examples should work
!(assertEqualToResult
(+ 2 (* 3 5.5))
(18.5))
!(assertEqualToResult
(- 8 (/ 4 6.4))
(7.375))
!(assertEqualToResult
(% 21 17)
(4))
!(assertEqualToResult
(< 4 (+ 2 (* 3 5)))
(True))
!(assertEqualToResult
(and (> 4 2) (< 4 3))
(False))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Currently, `ln` is not a grounded symbol.
; If we don't define its type, then its application
; will not be refused, but it will be unreduced.
; Currently, its grounded argument will be reduced.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
!(assertEqualToResult
(ln (+ 2 2))
((ln 4)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Similarly, passing ordinary symbols to grounded
; operations will not cause errors and simply remain
; unreduced, if it type-checks.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
!(assertEqualToResult
(> 4 (+ ln 2))
((> 4 (+ ln 2))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; This will also remain unreduced unless
; grounded operations can do pattern matching
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
!(assertEqualToResult
(> 4 (+ $x 2))
((> 4 (+ $x 2))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; `==` is now implemented to work with both grounded and
; symbolic atoms (while remaining a grounded operation)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
!(assertEqualToResult
(== 4 (+ 2 2))
(True))
!(assertEqualToResult
(== 2 3)
(False))
!(assertEqualToResult
(== (A B) (A B))
(True))
!(assertEqualToResult
(== (A B) (A (B C)))
(False))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Unlike `<` or `>`, `==` will not remain unreduced if one
; of its arguments is grounded, while another is not.
; Instead, it will return `False`
!(assertEqualToResult
(== 4 (+ ln 2))
(False))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Grounded symbols have predefined types.
; Evaluation of ill-typed expressions produces
; a error expression
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
!(assertEqualToResult
(+ 2 "String")
((Error "String" BadType)))
; Custom symbols as arguments of grounded operations
; work similarly
(: ln LN)
!(assertEqualToResult
(== 4 (+ ln 2))
((Error (+ ln 2) BadType)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Custom functions over grounded functions behave ordinarily
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(= (sqr $x) (* $x $x))
!(assertEqualToResult
(sqr 4)
(16))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Evaluation of grounded operations over nondeterministic
; expressions work in the same way as of custom symbols
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
!(assertEqual
(+ (superpose (1 2 3)) 1)
(superpose (2 3 4)))
(= (bin) 0)
(= (bin) 1)
!(assertEqualToResult
(+ 1 (bin))
(1 2))
!(assertEqualToResult
(let $x (+ 2 3)
(* $x $x))
(25))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; basic recursion
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(= (fact $n) (if (== $n 0) 1 (* (fact (- $n 1)) $n)))
!(assertEqual (fact 5) 120)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Grounded symbols work with non-determinism based "reasoning"
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Uses the grounded call `bin`, which returns a list of
; both possible bits (0, 1), to recursively construct all possible
; binary lists of length `$n`, appending bits one by one.
(= (gen $n)
(if (> $n 0)
(:: (bin) (gen (- $n 1)))
nil))
; Note: `::` is just a custom symbol, used here as a constructor,
; but any other symbol can be used for this.
; Calculates the sum of element-wise products between two lists
(= (subsum nil nil) 0)
(= (subsum (:: $x $xs) (:: $b $bs))
(+ (* $x $b)
(subsum $xs $bs)))
; Non-determinism "reasoning":
; Among all 3-bit binary lists, return the one whose `subsum`
; with (:: 3 (:: 7 (:: 5 nil))) equals 8, or `nop` if not found
; (`superpose` is used to return an empty result acting as termination
; of evaluation of the branch)
!(assertEqualToResult
(let $t (gen 3)
(if (== (subsum (:: 3 (:: 7 (:: 5 nil))) $t) 8) $t (superpose ())))
((:: 1 (:: 0 (:: 1 nil)))))