extra/logic/logic-docs.factor

   1 ! Copyright (C) 2019-2020 KUSUMOTO Norio.
   2 ! See http://factorcode.org/license.txt for BSD license.
   3 USING: arrays assocs help.markup help.syntax kernel logic.private
   4 make quotations ;
   5 IN: logic
   6
   7 HELP: !!
   8 { $var-description "The cut operator.\nUse the cut operator to suppress backtracking." }
   9 { $examples
  10   "In the following example, it is used to define that cats generally eat mice, but Tom does not."
  11   { $example
  12     "USING: logic prettyprint ;"
  13     "IN: scratchpad"
  14     ""
  15     "LOGIC-PREDS: is-ao consumeso ;"
  16     "LOGIC-VARS: X Y ;"
  17     "SYMBOLS: Tom Jerry Nibbles"
  18     "         mouse cat milk cheese fresh-milk Emmentaler ;"
  19     ""
  20     "{"
  21     "    { is-ao Tom cat }"
  22     "    { is-ao Jerry mouse }"
  23     "    { is-ao Nibbles mouse }"
  24     "    { is-ao fresh-milk milk }"
  25     "    { is-ao Emmentaler cheese }"
  26     "} facts"
  27     ""
  28     "{ consumeso X milk } {"
  29     "    { is-ao X mouse } ;;"
  30     "    { is-ao X cat }"
  31     "} rule"
  32     ""
  33     "{ consumeso X cheese } { is-ao X mouse } rule"
  34     "{ consumeso Tom mouse } { !! f } rule"
  35     "{ consumeso X mouse } { is-ao X cat } rule"
  36     ""
  37     "{ { consumeso Tom X } { is-ao Y X } } query ."
  38     "{ H{ { X milk } { Y fresh-milk } } }"
  39   }
  40 } ;
  41
  42 HELP: (<)
  43 { $var-description "A logic predicate. It takes two arguments. It is true if both arguments are evaluated numerically and the first argument is less than the second, otherwise, it is false." }
  44 { $syntax "{ (<) X Y }" }
  45 { $see-also (>) (>=) (==) (=<) } ;
  46
  47 HELP: (=)
  48 { $var-description "A logic predicate. It unifies two arguments." }
  49 { $syntax "{ (=) X Y }" }
  50 { $see-also (\=) is } ;
  51
  52 HELP: (=<)
  53 { $var-description "A logic predicate. It takes two arguments. It is true if both arguments are evaluated numerically and the first argument equals or is less than the second, otherwise, it is false." }
  54 { $syntax "{ (=<) X Y }" }
  55 { $see-also (>) (>=) (==) (<) } ;
  56
  57 HELP: (==)
  58 { $var-description "A logic predicate. It tests for equality of two arguments. Evaluating two arguments, true if they are the same, false if they are different." }
  59 { $syntax "{ (==) X Y }" }
  60 { $see-also (>) (>=) (=<) (<) =:= =\= } ;
  61
  62 HELP: (>)
  63 { $var-description "A logic predicate. It is true if both arguments are evaluated numerically and the first argument is greater than the second, otherwise, it is false." }
  64 { $syntax "{ (>) X Y }" }
  65 { $see-also (>=) (==) (=<) (<) } ;
  66
  67 HELP: (>=)
  68 { $var-description "A logic predicate. It is true if both arguments are evaluated numerically and the first argument equals or is greater than the second, otherwise, it is false." }
  69 { $syntax "{ (>=) X Y }" }
  70 { $see-also (>) (==) (=<) (<) } ;
  71
  72 HELP: (\=)
  73 { $var-description "A logic predicate. It will be true when such a unification fails. Note that " { $snippet "(\\=)" } " does not actually do the unification." }
  74 { $syntax "{ (\\=) X Y }" }
  75 { $see-also (=) } ;
  76
  77 HELP: (\==)
  78 { $var-description "A logic predicate. It tests for inequality of two arguments. Evaluating two arguments, true if they are different, false if they are the same." }
  79 { $syntax "{ (\\==) X Y }" }
  80 ;
  81
  82 HELP: ;;
  83 { $var-description "Is used to represent disjunction. The code below it has the same meaning as the code below it.
  84 "
  85 { $code
  86   "Gh { Gb1 Gb2 Gb3 ;; Gb4 Gb5 ;; Gb6 } rule" }
  87 ""
  88 { $code
  89   "Gh { Gb1 Gb2 Gb3 } rule"
  90   "Gh { Gb4 Gb5 } rule:
  91 Gh { Gb6 } rule" }
  92 } ;
  93
  94 HELP: =:=
  95 { $values
  96     { "quot" quotation }
  97     { "goal" logic-goal }
  98 }
  99 { $description "The quotations takes an environment and returns two values. " { $snippet "=:=" } " returns the internal representation of the goal which returns t if values returned by the quotation are same numbers.\n" { $snippet "=:=" } " is intended to be used in a quotation. If there is a quotation in the definition of rule, " { $snippet "logic" } " uses the internal definition of the goal obtained by calling it." }
 100 { $see-also (==) =\= } ;
 101
 102 HELP: =\=
 103 { $values
 104     { "quot" quotation }
 105     { "goal" logic-goal }
 106 }
 107 { $description "The quotations takes an environment and returns two values. " { $snippet "=\\=" } " returns the internal representation of the goal which returns t if values returned by the quotation are numbers and are not same.\n" { $snippet "=\\=" } " is intended to be used in a quotation. If there is a quotation in the definition of rule, " { $snippet "logic" } " uses the internal definition of the goal obtained by calling it." }
 108 { $see-also (==) =:= } ;
 109
 110 HELP: LOGIC-PRED:
 111 { $description "Creates a new logic predicate." }
 112 { $syntax "LOGIC-PRED: pred" }
 113 { $examples
 114   { $code
 115     "USE: logic"
 116     "IN: scratchpad"
 117     ""
 118     "LOGIC-PRED: cato"
 119     "SYMBOL: Tom"
 120     ""
 121     "{ cato Tom } fact"
 122   }
 123 }
 124 { $see-also \ LOGIC-PREDS: } ;
 125
 126 HELP: LOGIC-PREDS:
 127 { $description "Creates a new logic predicate for every token until the ;." }
 128 { $syntax "LOGIC-PREDS: preds... ;" }
 129 { $examples
 130   { $code
 131     "USE: logic"
 132     "IN: scratchpad"
 133     ""
 134     "LOGIC-PREDS: cato mouseo ;"
 135     "SYMBOLS: Tom Jerry ;"
 136     ""
 137     "{ cato Tom } fact"
 138     "{ mouseo Jerry } fact"
 139   }
 140 }
 141 { $see-also \ LOGIC-PRED: } ;
 142
 143 HELP: LOGIC-VAR:
 144 { $description "Creates a new logic variable." }
 145 { $syntax "LOGIC-VAR: var" }
 146 { $examples
 147   { $example
 148     "USING: logic prettyprint ;"
 149     "IN: scratchpad"
 150     ""
 151     "LOGIC-PRED: mouseo"
 152     "LOGIC-VAR: X"
 153     "SYMBOL: Jerry"
 154     "{ mouseo Jerry } fact"
 155     "{ mouseo X } query ."
 156     "{ H{ { X Jerry } } }"
 157   }
 158 }
 159 { $see-also \ LOGIC-VARS: } ;
 160
 161 HELP: LOGIC-VARS:
 162 { $description "Creates a new logic variable for every token until the ;." }
 163 { $syntax "LOGIC-VARS: vars... ;" }
 164 { $examples
 165   { $example
 166     "USING: logic prettyprint ;"
 167     "IN: scratchpad"
 168     ""
 169     "LOGIC-PRED: mouseo"
 170     "LOGIC-VARS: X ;"
 171     "SYMBOL: Jerry"
 172     "{ mouseo Jerry } fact"
 173     "{ mouseo X } query ."
 174     "{ H{ { X Jerry } } }"
 175   }
 176 }
 177 { $see-also \ LOGIC-VAR: } ;
 178
 179 HELP: %!
 180 { $description "A multiline comment. Despite being a Prolog single-line comment, " { $link % } " is already well-known in Factor, so this variant is given instead." }
 181 { $syntax "%! comment !%" }
 182 { $examples
 183     { $example
 184         "USE: logic"
 185         "%! I think that I shall never see"
 186         "   A proof lovely as a factlog. !%"
 187         ""
 188     }
 189 } ;
 190
 191 HELP: \+
 192 { $var-description "Express negation. \\+ acts on the goal immediately following it.\n" }
 193 { $examples
 194   { $example
 195     "USING: logic prettyprint ;"
 196     "IN: scratchpad"
 197     ""
 198     "LOGIC-PREDS: cato mouseo creatureo ;"
 199     "LOGIC-VARS: X Y ;"
 200     "SYMBOLS: Tom Jerry Nibbles ;"
 201     ""
 202     "{ cato Tom } fact"
 203     "{ mouseo Jerry } fact"
 204     "{ mouseo Nibbles } fact"
 205     "{ creatureo Y } {
 206     { cato Y } ;; { mouseo Y }
 207 } rule"
 208     ""
 209     "LOGIC-PREDS: likes-cheeseo dislikes-cheeseo ;"
 210     ""
 211     "{ likes-cheeseo X } { mouseo X } rule"
 212     "{ dislikes-cheeseo Y } {
 213     { creatureo Y }
 214     \\+ { likes-cheeseo Y }
 215     } rule"
 216     "{ dislikes-cheeseo Jerry } query ."
 217     "{ dislikes-cheeseo Tom } query ."
 218     "f\nt"
 219   }
 220 } ;
 221
 222 HELP: __
 223 { $var-description "An anonymous logic variable.\nUse in place of a regular logic variable when you do not need its name and value." }
 224 { $examples
 225   { $example
 226     "USING: logic prettyprint ;"
 227     "IN: scratchpad"
 228     ""
 229     "SYMBOLS: Tom Jerry Nibbles ;"
 230     "TUPLE: house living dining kitchen in-the-wall ;"
 231     "LOGIC-PRED: houseo"
 232     "LOGIC-VAR: X"
 233
 234     ""
 235     "{ houseo T{ house"
 236     "             { living Tom }"
 237     "             { dining f }"
 238     "             { kitchen Nibbles }"
 239     "             { in-the-wall Jerry }"
 240     "         }"
 241     "} fact"
 242     ""
 243     "{ houseo T{ house"
 244     "             { living __ }"
 245     "             { dining __ }"
 246     "             { kitchen X }"
 247     "             { in-the-wall __ }"
 248     "         }"
 249     "} query ."
 250     "{ H{ { X Nibbles } } }"
 251   }
 252 } ;
 253
 254 HELP: appendo
 255 { $var-description "A logic predicate. Concatenate two lists." }
 256 { $syntax "{ appendo List1 List2 List1+List2 }" }
 257 { $examples
 258   { $example
 259     "USING: logic lists prettyprint ;"
 260     "IN: scratchpad"
 261     ""
 262     "SYMBOLS: Tom Jerry Nibbles ;"
 263     "LOGIC-VARS: X Y ;"
 264     ""
 265     "{ appendo L{ Tom } L{ Jerry Nibbles } X } query ."
 266     "{ appendo L{ Tom } L{ Jerry Nibbles } L{ Jerry Nibbles Tom } } query ."
 267     "{ appendo X Y L{ Tom Jerry Nibbles } } query ."
 268     "{ H{ { X L{ Tom Jerry Nibbles } } } }\nf\n{\n    H{ { X L{ } } { Y L{ Tom Jerry Nibbles } } }\n    H{ { X L{ Tom } } { Y L{ Jerry Nibbles } } }\n    H{ { X L{ Tom Jerry } } { Y L{ Nibbles } } }\n    H{ { X L{ Tom Jerry Nibbles } } { Y L{ } } }\n}"
 269   }
 270 } ;
 271
 272 HELP: callback
 273 { $values
 274     { "head" array } { "quot" quotation }
 275 }
 276 { $description "Set the quotation to be called. Such quotations take an environment which holds the binding of logic variables, and returns t or " { $link f } " as a result of execution. To retrieve the values of logic variables in the environment, use " { $link of } " or " { $link at } "." }
 277 { $examples
 278   { $code
 279     "LOGIC-PRED: N_>_0"
 280     "{ N_>_0 N } [ N of 0 > ] callback"
 281   }
 282 }
 283 { $see-also callbacks } ;
 284
 285 HELP: callbacks
 286 { $values
 287     { "defs" array }
 288 }
 289 { $description "To collectively register a plurality of " { $link callback } "s." }
 290 { $examples
 291   { $code "LOGIC-PREDS: N_>_0  N2_is_N_-_1  F_is_F2_*_N ;
 292 {
 293     { { N_>_0 N } [ N of 0 > ] }
 294     { N2_is_N_-_1 N2 N } [ dup N of 1 - N2 unify ] }
 295     { F_is_F2_*_N F F2 N } [ dup [ F2 of ] [ N of ] bi * F unify ] }
 296 } callbacks" }
 297 }
 298 { $see-also callback } ;
 299
 300 HELP: clear-pred
 301 { $values
 302     { "pred" "a logic predicate" }
 303 }
 304 { $description "Clears all the definition information for the given logic predicate." }
 305 { $examples
 306   { $example
 307     "USING: logic prettyprint ;"
 308     "IN: scratchpad"
 309     ""
 310     "LOGIC-PRED: mouseo"
 311     "SYMBOLS: Jerry Nibbles ;"
 312     "LOGIC-VAR: X"
 313     ""
 314     "{ mouseo Jerry } fact"
 315     "{ mouseo Nibbles } fact"
 316     ""
 317     "{ mouseo X } query ."
 318     "mouseo clear-pred"
 319     "{ mouseo X } query ."
 320     "{ H{ { X Jerry } } H{ { X Nibbles } } }\nf"
 321   }
 322 }
 323 { $see-also retract retract-all } ;
 324
 325 HELP: fact
 326 { $values
 327     { "head" "an array representing a goal" }
 328 }
 329 { $description "Registers the fact to the end of the logic predicate that is in the head." }
 330 { $examples
 331   { $code
 332     "USE: logic"
 333     "IN: scratchpad"
 334     ""
 335     "LOGIC-PREDS: cato mouseo ;"
 336     "SYMBOLS: Tom Jerry ;"
 337     "{ cato Tom } fact"
 338     "{ mouseo Jerry } fact"
 339   }
 340 }
 341 { $see-also fact* facts } ;
 342
 343 HELP: fact*
 344 { $values
 345     { "head" "an array representing a goal" }
 346 }
 347 { $description "Registers the fact to the beginning of the logic predicate that is in the head." }
 348 { $see-also fact facts } ;
 349
 350 HELP: facts
 351 { $values
 352     { "defs" array }
 353 }
 354 { $description "Registers these facts to the end of the logic predicate that is in the head." }
 355 { $examples
 356   { $code
 357     "USE: logic"
 358     "IN: scratchpad"
 359     ""
 360     "LOGIC-PREDS: cato mouseo ;"
 361     ""
 362     "{ { cato Tom } { mouseo Jerry } } facts"
 363   }
 364 }
 365 { $see-also fact fact* } ;
 366
 367 HELP: failo
 368 { $var-description "A built-in logic predicate. { " { $snippet "failo" } " } is a goal that is always " { $link f } "." }
 369 { $syntax "{ failo }" }
 370 { $see-also trueo } ;
 371
 372 HELP: is
 373 { $values
 374     { "quot" quotation } { "dist" "a logic predicate" }
 375     { "goal" logic-goal }
 376 }
 377 { $description "Takes a quotation and a logic variable to be unified. Each of the two quotations takes an environment and returns a value. " { $snippet "is" } " returns the internal representation of the goal.\n" { $snippet "is" } " is intended to be used in a quotation. If there is a quotation in the definition of rule, " { $snippet "logic" } " uses the internal definition of the goal obtained by calling it." } ;
 378
 379 HELP: invoke
 380 { $values
 381     { "quot" quotation }
 382     { "goal" logic-goal }
 383 }
 384 { $description "Creates a goal which uses the values of obtained logic variables. It can be used to add new rules to or drop rules from the database while a " { $link query } " is running.\nThe argument " { $snippet "quot" } " must not return any values, the created goal always return " { $link t } ".\n" { $snippet "invoke" } " is intended to be used in a quotation. If there is a quotation in the definition of rule, " { $snippet "logic" } " uses the internal definition of the goal obtained by calling it." }
 385 { $examples
 386   "In this example, the calculated values are memorized to eliminate recalculation."
 387   { $example
 388     "USING: logic kernel lists assocs locals math prettyprint ;"
 389     "IN: scratchpad"
 390     ""
 391     "LOGIC-PRED: fibo"
 392     "LOGIC-VARS: F F1 F2 N N1 N2 ;"
 393     ""
 394     "{ fibo 1 1 } fact"
 395     "{ fibo 2 1 } fact"
 396     "{ fibo N F } {"
 397     "    { (>) N 2 }"
 398     "    [ [ N of 1 - ] N1 is ] { fibo N1 F1 }"
 399     "    [ [ N of 2 - ] N2 is ] { fibo N2 F2 }"
 400     "    [ [ [ F1 of ] [ F2 of ] bi + ] F is ]"
 401     "    ["
 402     "        ["
 403     "            [ N of ] [ F of ] bi"
 404     "            [let :> ( nv fv ) { fibo nv fv } !! rule* ]"
 405     "        ] invoke ]"
 406     "} rule"
 407     ""
 408     "{ fibo 10 F } query ."
 409     "{ H{ { F 55 } } }"
 410   }
 411 }
 412 { $see-also invoke* } ;
 413
 414 HELP: invoke*
 415 { $values
 416     { "quot" quotation }
 417     { "goal" logic-goal }
 418 }
 419 { $description "Creates a goal which uses the values of obtained logic variables. The difference with " { $link invoke } " is that " { $snippet "quot" } " returns " { $link t } " or " { $link f } ", and the created goal returns it.\n" { $snippet "invoke*" } " is intended to be used in a quotation. If there is a quotation in the definition of rule, " { $snippet "logic" } " uses the internal definition of the goal obtained by calling it." }
 420 { $see-also invoke } ;
 421
 422 HELP: lengtho
 423 { $var-description "A logic predicate. Instantiate the length of the list." }
 424 { $syntax "{ lengtho List X }" }
 425 { $examples
 426   { $example
 427     "USING: logic lists prettyprint ;"
 428     "IN: scratchpad"
 429     ""
 430     "SYMBOLS: Tom Jerry Nibbles ;"
 431     "LOGIC-VAR: X"
 432     ""
 433     "{ lengtho L{ Tom Jerry Nibbles } 3 } query ."
 434     "{ lengtho L{ Tom Jerry Nibbles } X } query ."
 435     "t\n{ H{ { X 3 } } }"
 436   }
 437 } ;
 438
 439 HELP: listo
 440 { $var-description "A logic predicate. Takes a single argument and checks to see if it is a list." }
 441 { $syntax "{ listo X }" }
 442 { $examples
 443   { $example
 444     "USING: logic lists prettyprint ;"
 445     "IN: scratchpad"
 446     ""
 447     "SYMBOLS: Tom Jerry Nibbles ;"
 448     ""
 449     "{ listo L{ Jerry Nibbles } } query ."
 450     "{ listo Tom } query ."
 451     "t\nf"
 452   }
 453 } ;
 454
 455 HELP: membero
 456 { $var-description "A logic predicate for the relationship an element is in a list." }
 457 { $syntax "{ membero X List }" }
 458 { $examples
 459   { $example
 460     "USING: logic lists prettyprint ;"
 461     "IN: scratchpad"
 462     ""
 463     "SYMBOLS: Tom Jerry Nibbles Spike ;"
 464     ""
 465     "{ membero Jerry L{ Tom Jerry Nibbles } } query ."
 466     "{ membero Spike L{ Tom Jerry Nibbles } } query ."
 467     "t\nf"
 468   }
 469 } ;
 470
 471 HELP: nlo
 472 { $var-description "A logic predicate. Print line breaks." }
 473 { $syntax "{ nlo }" }
 474 { $see-also writeo writenlo } ;
 475
 476 HELP: nonvaro
 477 { $var-description "A logic predicate. " { $snippet "nonvaro" } " takes a single argument and is true if its argument is not a logic variable or is a concrete logic variable." }
 478 { $syntax "{ nonvaro X }" }
 479 { $see-also varo } ;
 480
 481 HELP: notrace
 482 { $description "Stop tracing." }
 483 { $see-also trace } ;
 484
 485 HELP: query
 486 { $values
 487     { "goal-def/defs"  "a goal def or an array of goal defs" }
 488     { "bindings-array/success?" "anser" }
 489 }
 490 { $description
 491   "Inquire about the order of goals. The general form of a query is:
 492
 493     { G1 G2 ... Gn } query
 494
 495 This G1, G2, ... Gn is a conjunction. When all of them are satisfied, it becomes " { $link t } ".
 496
 497 If there is only one goal, you can use its abbreviation.
 498
 499     G1 query
 500
 501 When you query with logic variable(s), you will get the answer for the logic variable(s). For such queries, an array of hashtables with logic variables as keys is returned.
 502 "
 503 }
 504 { $examples
 505   { $example
 506     "USING: logic prettyprint ;"
 507     "IN: scratchpad"
 508     ""
 509     "LOGIC-PREDS: cato mouseo creatureo ;"
 510     "LOGIC-VARS: X Y ;"
 511     "SYMBOLS: Tom Jerry Nibbles ;"
 512     ""
 513     "{ cato Tom } fact"
 514     "{ mouseo Jerry } fact"
 515     "{ mouseo Nibbles } fact"
 516     ""
 517     "{ cato Tom } query ."
 518     "{ { cato Tom } { cato Jerry } } query ."
 519     "{ mouseo X } query ."
 520     "t\nf\n{ H{ { X Jerry } } H{ { X Nibbles } } }"
 521   }
 522 }
 523 { $see-also nquery } ;
 524
 525 HELP: nquery
 526 { $values
 527     { "goal-def/defs" "a goal def or an array of goal defs" } { "n/f" "the highest number of responses" }
 528     { "bindings-array/success?" "anser" }
 529 }
 530 { $description "The version of " { $link query } " that limits the number of responses. Specify a number greater than or equal to 1.
 531 If " { $link f } " is given instead of a number as " { $snippet "n/f" } ", there is no limit to the number of answers. That is, the behavior is the same as " { $link query } "." }
 532 { $see-also query } ;
 533
 534 HELP: retract
 535 { $values
 536     { "head-def" "a logic predicate" }
 537 }
 538 { $description "Removes the first definition that matches the given head information." }
 539 { $examples
 540   { $example
 541     "USING: logic prettyprint ;"
 542     "IN: scratchpad"
 543     ""
 544     "LOGIC-PRED: mouseo"
 545     "SYMBOLS: Jerry Nibbles ;"
 546     ""
 547     "{ mouseo Jerry } fact"
 548     "{ mouseo Nibbles } fact"
 549     ""
 550     "{ mouseo X } query ."
 551     "{ mouseo Jerry } retract"
 552     "{ mouseo X } query ."
 553     "{ H{ { X Jerry } } H{ { X Nibbles } } }\n{ H{ { X Nibbles } } }"
 554   }
 555 }
 556 { $see-also retract-all clear-pred } ;
 557
 558 HELP: retract-all
 559 { $values
 560     { "head-def" "a logic predicate" }
 561 }
 562 { $description "Removes all definitions that match a given head goal definition." }
 563 { $examples
 564   { $example
 565     "USING: logic prettyprint ;"
 566     "IN: scratchpad"
 567     ""
 568     "LOGIC-PRED: mouseo"
 569     "SYMBOLS: Jerry Nibbles ;"
 570     ""
 571     "{ mouseo Jerry } fact"
 572     "{ mouseo Nibbles } fact"
 573     ""
 574     "{ mouseo X } query ."
 575     "{ mouseo __ } retract-all"
 576     "{ mouseo X } query ."
 577     "{ H{ { X Jerry } } H{ { X Nibbles } } }\nf"
 578   }
 579 }
 580 { $see-also retract clear-pred } ;
 581
 582 HELP: rule
 583 { $values
 584     { "head" "an array representing a goal" } { "body" "an array of goals or a goal" }
 585 }
 586 { $description "Registers the rule to the end of the logic predicate that is in the head.
 587 The general form of rule is:
 588
 589     Gh { Gb1 Gb2 ... Gbn } rule
 590
 591 This means Gh when all goals of Gb1, Gb2, ..., Gbn are met. This Gb1 Gb2 ... Gbn is a conjunction.
 592 If the body array contains only one goal definition, you can write it instead of the body array. That is, they are equivalent.
 593
 594     Gh { Gb } rule
 595     Gh Gb rule" }
 596 { $examples
 597   { $example
 598     "USING: logic prettyprint ;"
 599     "IN: scratchpad"
 600     ""
 601     "LOGIC-PREDS: mouseo youngo young-mouseo ;"
 602     "SYMBOLS: Jerry Nibbles ;"
 603     ""
 604     "{ mouseo Jerry } fact"
 605     "{ mouseo Nibbles } fact"
 606     "{ youngo Nibbles } fact"
 607     ""
 608     "{ young-mouseo X } {"
 609     "    { mouseo X }"
 610     "    { youngo X }"
 611     "} rule"
 612     ""
 613     "{ young-mouseo X } query ."
 614     "{ H{ { X Nibbles } } }"
 615   }
 616 }
 617 { $see-also rule* rules } ;
 618
 619 HELP: rule*
 620 { $values
 621     { "head" "an array representing a goal" } { "body" "an array of goals or a goal" }
 622 }
 623 { $description "Registers the rule to the beginnung of the logic predicate that is in the head." }
 624 { $see-also rule rules } ;
 625
 626 HELP: rules
 627 { $values
 628   { "defs" "an array of rules" }
 629 }
 630 { $description "Registers these rules to the end of the logic predicate that is in these heads." }
 631 { $examples
 632   { $code
 633     "LOGIC-PREDS: is-ao consumeso ;"
 634     "SYMBOLS: Tom Jerry Nibbles ;"
 635     "SYMBOLS: mouse cat milk cheese fresh-milk Emmentaler ;"
 636     ""
 637     "{"
 638     "    { is-ao Tom cat }"
 639     "    { is-ao Jerry mouse }"
 640     "    { is-ao Nibbles mouse }"
 641     "    { is-ao fresh-milk milk }"
 642     "    { is-ao Emmentaler cheese }"
 643     "} facts"
 644     ""
 645     "{"
 646     "    {"
 647     "        { consumeso X milk } {"
 648     "            { is-ao X mouse } ;;"
 649     "            { is-ao X cat }"
 650     "        }"
 651     "    }"
 652     "    { { consumeso X cheese } { is-ao X mouse } }"
 653     "    { { consumeso X mouse } { is-ao X cat } }"
 654     "} rules"
 655   }
 656 }
 657 { $see-also rule rule* } ;
 658
 659 HELP: trace
 660 { $description "Start tracing." }
 661 { $see-also notrace } ;
 662
 663 HELP: trueo
 664 { $var-description "A logic predicate. { " { $snippet "trueo" } " } is a goal that is always " { $link t } "." }
 665 { $syntax "{ trueo }" }
 666 { $see-also failo } ;
 667
 668 HELP: unify
 669 { $values
 670     { "cb-env" callback-env } { "x" object } { "y" object }
 671     { "success?" boolean }
 672 }
 673 { $description "Unifies the two following the environment in that environment." } ;
 674
 675 HELP: varo
 676 { $var-description "A logic predicate. " { $snippet "varo" } " takes a argument and is true if it is a logic variable with no value." }
 677 { $syntax "{ varo X }" }
 678 { $see-also nonvaro } ;
 679
 680 HELP: writenlo
 681 { $var-description "A logic predicate. print a single sequence or string and return a new line." }
 682 { $syntax "{ writenlo X }" }
 683 { $see-also writeo nlo } ;
 684
 685 HELP: writeo
 686 { $var-description "A logic predicate. print a single sequence or string of characters." }
 687 { $syntax "{ writeo X }" }
 688 { $see-also writenlo nlo } ;
 689
 690 ARTICLE: "logic" "Logic"
 691 { $vocab-link "logic" }
 692 " is a vocab for an embedded language that runs on " { $url "https://github.com/factor/factor" "Factor" } " with the capabilities of a subset of Prolog." $nl
 693 "It is an extended port from tiny_prolog and its descendants, " { $url "https://github.com/preston/ruby-prolog" "ruby-prolog" } "." $nl
 694 { $code
 695 "USE: logic
 696
 697 LOGIC-PREDS: cato mouseo creatureo ;
 698 LOGIC-VARS: X Y ;
 699 SYMBOLS: Tom Jerry Nibbles ;"
 700 } $nl
 701 "In the DSL, words that represent relationships are called " { $strong "logic predicates" } ". Use " { $link \ LOGIC-PRED: } " or " { $link \ LOGIC-PREDS: } " to declare the predicates you want to use. " { $strong "Logic variables" } " are used to represent relationships. use " { $link \ LOGIC-VAR: } " or " { $link \ LOGIC-VARS: } " to declare the logic variables you want to use." $nl
 702 "In the above code, logic predicates end with the character 'o', which is a convention borrowed from miniKanren and so on, and means relation. This is not necessary, but it is useful for reducing conflicts with the words of, the parent language, Factor. We really want to write them as: " { $snippet "cat°" } ", " { $snippet "mouse°" } " and " { $snippet "creature°" } ", but we use 'o' because it's easy to type." $nl
 703 { $strong "Goals" } " are questions that " { $snippet "logic" } " tries to meet to be true. To represent a goal, write an array with a logic predicate followed by zero or more arguments. " { $snippet "logic" } " converts such definitions to internal representations." $nl
 704 { $code "{ LOGIC-PREDICATE ARG1 ARG2 ... }" }
 705 { $code "{ LOGIC-PREDICATE }" } $nl
 706 "We will write logic programs using these goals." $nl
 707 { $code
 708 "{ cato Tom } fact
 709 { mouseo Jerry } fact
 710 { mouseo Nibbles } fact"
 711 } $nl
 712 "The above code means that Tom is a cat and Jerry and Nibbles are mice. Use " { $link fact } " to describe the " { $strong "facts" } "." $nl
 713 { $unchecked-example
 714 "{ cato Tom } query ."
 715 "t"
 716 } $nl
 717 "The above code asks, \"Is Tom a cat?\". We said,\"Tom is a cat.\", so the answer is " { $link t } ". The general form of a query is:" $nl
 718 { $code "{ G1 G2 ... Gn } query" } $nl
 719 "The parentheses are omitted because there was only one goal to be satisfied earlier, but here is an example of two goals:" $nl
 720 { $unchecked-example
 721 "{ { cato Tom } { cato Jerry } } query ."
 722 "f"
 723 } $nl
 724 "Tom is a cat, but Jerry is not declared a cat, so " { $link f } " is returned in response to this query." $nl
 725 "If you query with logic variable(s), you will get the answer for the logic variable(s). For such queries, an array of hashtables with logic variables as keys is returned." $nl
 726 { $unchecked-example
 727 "{ mouseo X } query ."
 728 "{ H{ { X Jerry } } H{ { X Nibbles } } }"
 729 } $nl
 730 "The following code shows that if something is a cat, it's a creature. Use " { $link rule } " to write " { $strong "rules" } "." $nl
 731 { $code
 732   "{ creatureo X } { cato X } rule"
 733 } $nl
 734 "According to the rules above, \"Tom is a creature.\" is answered to the following questions:" $nl
 735 { $unchecked-example
 736 "{ creatureo Y } query ."
 737 "{ H{ { Y Tom } } }"
 738 } $nl
 739 "The general form of " { $link rule } " is:" $nl
 740 { $code "Gh { Gb1 Gb2 ... Gbn } rule" } $nl
 741 "This means " { $snippet "Gh" } " when all goals of " { $snippet "Gb1" } ", " { $snippet "Gb2" } ", ..., " { $snippet "Gbn" } " are met. This " { $snippet "Gb1 Gb2 ... Gbn" } " is a " { $strong "conjunction" } "." $nl
 742 { $unchecked-example
 743 "LOGIC-PREDS: youngo young-mouseo ;
 744
 745 { youngo Nibbles } fact
 746
 747 { young-mouseo X } {
 748     { mouseo X }
 749     { youngo X }
 750 } rule
 751
 752 { young-mouseo X } query ."
 753 "{ H{ { X Nibbles } } }"
 754 } $nl
 755 "This " { $snippet "Gh" } " is called " { $strong "head" } " and the " { $snippet "{ Gb 1Gb 2... Gbn }" } " is called " { $strong "body" } "." $nl
 756 "Facts are rules where its body is an empty array. So, the form of " { $link fact } " is:" $nl
 757 { $code "Gh fact" } $nl
 758 "Let's describe that mice are also creatures." $nl
 759 { $unchecked-example
 760 "{ creatureo X } { mouseo X } rule
 761
 762 { creatureo X } query ."
 763 "{ H{ { X Tom } } H{ { X Jerry } } H{ { X Nibbles } } }"
 764 } $nl
 765 "To tell the truth, we were able to describe at once that cats and mice were creatures by doing the following." $nl
 766 { $code
 767 "LOGIC-PRED: creatureo
 768
 769 { creatureo Y } {
 770     { cato Y } ;; { mouseo Y }
 771 } rule"
 772 } $nl
 773 { $link ;; } " is used to represent " { $strong "disjunction" } ". The following two forms are equivalent:" $nl
 774 { $code "Gh { Gb1 Gb2 Gb3 ;; Gb4 Gb5 ;; Gb6 } rule" }
 775 $nl
 776 { $code
 777   "Gh { Gb1 Gb2 Gb3 } rule"
 778   "Gh { Gb4 Gb5 } rule"
 779   "Gh { Gb6 } rule"
 780 } $nl
 781 { $snippet "logic" } " actually converts the disjunction in that way. You may need to be careful about that when deleting definitions that you registered using " { $link rule } ", etc." $nl
 782 "You can use " { $link nquery } " to limit the number of answers to a query. Specify a number greater than or equal to 1." $nl
 783 { $unchecked-example
 784 "{ creatureo Y } 2 nquery ."
 785 "{ H{ { Y Tom } } H{ { Y Jerry } } }"
 786 } $nl
 787 "Use " { $link \+ } " to express " { $strong "negation" } ". " { $link \+ } " acts on the goal immediately following it." $nl
 788 { $unchecked-example
 789 "LOGIC-PREDS: likes-cheeseo dislikes-cheeseo ;
 790
 791 { likes-cheeseo X } { mouseo X } rule
 792
 793 { dislikes-cheeseo Y } {
 794     { creatureo Y }
 795     \\+ { likes-cheeseo Y }
 796 } rule"
 797 "{ dislikes-cheeseo Jerry } query ."
 798 "{ dislikes-cheeseo Tom } query ."
 799 "f\nt"
 800 } $nl
 801 "Other creatures might also like cheese..." $nl
 802 "You can also use sequences, lists, and tuples as goal definition arguments." $nl
 803 "The syntax of list descriptions allows you to describe \"head\" and \"tail\" of a list." $nl
 804 { $code "L{ HEAD . TAIL }" }
 805 { $code "L{ ITEM1 ITEM2 ITEM3 . OTHERS }" } $nl
 806 "You can also write a quotation that returns an argument as a goal definition argument." $nl
 807 { $code "[ Tom Jerry Nibbles L{ } cons cons cons ]" } $nl
 808 "When written as an argument to a goal definition, the following lines have the same meaning as above:" $nl
 809 { $code "L{ Tom Jerry Nibbles }" }
 810 { $code "L{ Tom Jerry Nibbles . L{ } }" }
 811 { $code "[ { Tom Jerry Nibbles } >list } ]" } $nl
 812 "Such quotations are called only once when converting the goal definitions to internal representations." $nl
 813 { $link membero } " is a built-in logic predicate for the relationship an element is in a list." $nl
 814 { $unchecked-example
 815   "USE: lists
 816 SYMBOL: Spike
 817
 818 { membero Jerry L{ Tom Jerry Nibbles } } query .
 819 { membero Spike [ Tom Jerry Nibbles L{ } cons cons cons ] } query ."
 820 "t\nf"
 821 } $nl
 822 "Recently, they moved into a small house. The house has a living room, a dining room and a kitchen. Well, humans feel that way. Each of them seems to be in their favorite room." $nl
 823 { $code
 824 "TUPLE: house living dining kitchen in-the-wall ;
 825 LOGIC-PRED: houseo
 826
 827 { houseo T{ house { living Tom } { dining f } { kitchen Nibbles } { in-the-wall Jerry } } } fact"
 828 } $nl
 829 "Don't worry about not mentioning the bathroom." $nl
 830 "Let's ask who is in the kitchen." $nl
 831 { $unchecked-example
 832 "{ houseo T{ house { living __ } { dining __ } { kitchen X } { in-the-wall __ } } } query ."
 833 "{ H{ { X Nibbles } } }"
 834 } $nl
 835 "These two consecutive underbars are called " { $strong "anonymous logic variables" } ". Use in place of a regular logic variable when you do not need its name and value." $nl
 836 "It seems to be meal time. What do they eat?" $nl
 837 { $code
 838 "LOGIC-PREDS: is-ao consumeso ;
 839 SYMBOLS: mouse cat milk cheese fresh-milk Emmentaler ;
 840
 841 {
 842     { is-ao Tom cat }
 843     { is-ao Jerry mouse }
 844     { is-ao Nibbles mouse }
 845     { is-ao fresh-milk milk }
 846     { is-ao Emmentaler cheese }
 847 } facts
 848
 849 {
 850     {
 851         { consumeso X milk } {
 852             { is-ao X mouse } ;;
 853             { is-ao X cat }
 854         }
 855     }
 856     { { consumeso X cheese } { is-ao X mouse } }
 857     { { consumeso X mouse } { is-ao X cat } }
 858 } rules"
 859 } $nl
 860 "Here, " { $link facts } " and " { $link rules } " are used. They can be used for successive facts or rules." $nl
 861 "Let's ask what Jerry consumes." $nl
 862 { $unchecked-example
 863 "{ { consumeso Jerry X } { is-ao Y X } } query ."
 864 "{
 865     H{ { X milk } { Y fresh-milk } }
 866     H{ { X cheese } { Y Emmentaler } }
 867 }"
 868 } $nl
 869 "Well, what about Tom?" $nl
 870 { $unchecked-example
 871 "{ { consumeso Tom X } { is-ao Y X } } query ."
 872 "{
 873     H{ { X milk } { Y fresh-milk } }
 874     H{ { X mouse } { Y Jerry } }
 875     H{ { X mouse } { Y Nibbles } }
 876 }"
 877 } $nl
 878 "This is a problematical answer. We have to redefine " { $snippet "consumeso" } "." $nl
 879 { $code
 880 "LOGIC-PRED: consumeso
 881
 882 { consumeso X milk } {
 883     { is-ao X mouse } ;;
 884     { is-ao X cat }
 885 } rule
 886
 887 { consumeso X cheese } { is-ao X mouse } rule
 888 { consumeso Tom mouse } { !! f } rule
 889 { consumeso X mouse } { is-ao X cat } rule"
 890 } $nl
 891 "We wrote about Tom before about common cats. What two consecutive exclamation marks represent is called a " { $strong "cut" } " operator. Use the cut operator to suppress " { $strong "backtracking" } "." $nl
 892 "The next letter " { $link f } " is an abbreviation for goal { " { $link failo } " } using the built-in logic predicate " { $link failo } ". { " { $link failo } " } is a goal that is always " { $link f } ". Similarly, there is a goal { " { $link trueo } " } that is always " { $link t } ", and its abbreviation is " { $link t } "." $nl
 893 "By these actions, \"Tom consumes mice.\" becomes false and suppresses the examination of general eating habits of cats." $nl
 894 { $unchecked-example
 895 "{ { consumeso Tom X } { is-ao Y X } } query ."
 896 "{ H{ { X milk } { Y fresh-milk } } }"
 897 } $nl
 898 "It's OK. Let's check a cat that is not Tom." $nl
 899 { $unchecked-example
 900 "SYMBOL: a-cat
 901 { is-ao a-cat cat } fact
 902
 903 { { consumeso a-cat X } { is-ao Y X } } query ."
 904 "{
 905     H{ { X milk } { Y fresh-milk } }
 906     H{ { X mouse } { Y Jerry } }
 907     H{ { X mouse } { Y Nibbles } }
 908 }"
 909 } $nl
 910 "Jerry, watch out for the other cats." $nl
 911 "So far, we've seen how to define a logic predicate with " { $link fact } ", " { $link rule } ", " { $link facts } ", and " { $link rules } ". Each time you use those words for a logic predicate, information is added to it." $nl
 912 "You can clear these definitions with " { $link clear-pred } " for a logic predicate." $nl
 913 { $unchecked-example
 914 "cato clear-pred
 915 mouseo clear-pred
 916 { creatureo X } query ."
 917 "f"
 918 } $nl
 919 { $link fact } " and " { $link rule } " add a new definition to the end of a logic predicate, while " { $link fact* } " and " { $link rule* } " add them first. The order of the information can affect the results of a query." $nl
 920 { $unchecked-example
 921 "{ cato Tom } fact
 922 { mouseo Jerry } fact
 923 { mouseo Nibbles } fact*
 924
 925 { mouseo Y } query .
 926
 927 { creatureo Y } 2 nquery ."
 928 "{ H{ { Y Nibbles } } H{ { Y Jerry } } }\n{ H{ { Y Tom } } H{ { Y Nibbles } } }"
 929 } $nl
 930 "While " { $link clear-pred } " clears all the definition information for a given logic predicate, " { $link retract } " and " { $link retract-all } " provide selective clearing." $nl
 931 { $link retract } " removes the first definition that matches the given head information." $nl
 932 { $unchecked-example
 933 "{ mouseo Jerry } retract
 934 { mouseo X } query ."
 935 "{ H{ { X Nibbles } } }"
 936 } $nl
 937 "On the other hand, " { $link retract-all } " removes all definitions that match a given head goal definition. Logic variables, including anonymous logic variables, can be used as goal definition arguments in " { $link retract } " and " { $link retract-all } ". A logic variable match any argument." $nl
 938 { $unchecked-example
 939 "{ mouseo Jerry } fact
 940 { mouseo X } query .
 941
 942 { mouseo __ } retract-all
 943 { mouseo X } query ."
 944 "{ H{ { X Nibbles } } H{ { X Jerry } } }\nf"
 945 } $nl
 946 "let's have them come back." $nl
 947 { $unchecked-example
 948 "{ { mouseo Jerry } { mouseo Nibbles } } facts
 949 { creatureo X } query ."
 950 "{ H{ { X Tom } } H{ { X Jerry } } H{ { X Nibbles } } }"
 951 } $nl
 952 "Logic predicates that take different numbers of arguments are treated separately. The previously used " { $snippet "cato" } " took one argument. Let's define " { $snippet "cato" } " that takes two arguments." $nl
 953 { $unchecked-example
 954 "SYMBOLS: big small a-big-cat a-small-cat ;
 955
 956 { cato big a-big-cat } fact
 957 { cato small a-small-cat } fact
 958
 959 { cato X } query .
 960 { cato X Y } query .
 961 { creatureo X } query ."
 962 "{ H{ { X Tom } } }\n{ H{ { X big } { Y a-big-cat } } H{ { X small } { Y a-small-cat } } }\n{ H{ { X Tom } } H{ { X Jerry } } H{ { X Nibbles } }"
 963 } $nl
 964 "If you need to identify a logic predicate that has a different " { $strong "arity" } ", that is numbers of arguments, express it with a slash and an arity number. For example, " { $snippet "cato" } " with arity 1 is " { $snippet "cato/1" } ", " { $snippet "cato" } " with arity 2 is " { $snippet "cato/2" } ". But, note that " { $snippet "logic" } " does not recognize these names." $nl
 965 { $link clear-pred } " will clear all definitions of any arity. If you only want to remove the definition of a certain arity, you should use " { $link retract-all } " with logic variables." $nl
 966 { $unchecked-example
 967 "{ cato __ __ } retract-all
 968 { cato X Y } query ."
 969 "{ cato X } query ."
 970 "f\n{ H{ { X Tom } } }"
 971 } $nl
 972 "You can " { $strong "trace" } " " { $snippet "logic" } "'s execution. The word to do this is " { $link trace } "." $nl
 973 "The word to stop tracing is " { $link notrace } "." $nl
 974 "Here is a Prolog definition for the factorial predicate " { $snippet "factorial" } "." $nl
 975 "factorial(0, 1)." $nl
 976 "factorial(N, F) :- N > 0, N2 is N - 1, factorial(N2, F2), F is F2 * N." $nl
 977 "Let's think about how to do the same thing. It is mostly the following code, but is surrounded by backquotes where it has not been explained." $nl
 978 { $code
 979 "USE: logic
 980
 981 LOGIC-PRED: factorialo
 982 LOGIC-VARS: N N2 F F2 ;
 983
 984 { factorialo 0 1 } fact
 985 { factorialo N F } {
 986     `N > 0`
 987     `N2 is N - 1`
 988     { factorialo N2 F2 }
 989     `F is F2 * N`
 990 } rule"
 991 } $nl
 992 "Within these backquotes are comparisons, calculations, and assignments (to be precise, " { $strong "unifications" } "). " { $snippet "logic" } " has a mechanism to call Factor code to do these things. Here are some example." $nl
 993 { $code "LOGIC-PREDS: N_>_0  N2_is_N_-_1  F_is_F2_*_N ;" }
 994 { $code "{ N_>_0 N } [ N of 0 > ] callback" }
 995 { $code "{ N2_is_N_-_1 N2 N } [ dup N of 1 - N2 unify ] callback" }
 996 { $code "{ F_is_F2_*_N F F2 N } [ dup [ F2 of ] [ N of ] bi * F unify ] callback" } $nl
 997 "Use " { $link callback } " to set the quotation to be called. Such quotations take an " { $strong "environment" } " which holds the binding of logic variables, and returns " { $link t } " or " { $link f } " as a result of execution. To retrieve the values of logic variables in the environment, use " { $link of } " or " { $link at } "." $nl
 998 "The word " { $link unify } " unifies the two following the environment in that environment." $nl
 999 "Now we can rewrite the definition of factorialo to use them." $nl
1000 { $code
1001 "USE: logic
1002
1003 LOGIC-PREDS: factorialo N_>_0  N2_is_N_-_1  F_is_F2_*_N ;
1004 LOGIC-VARS: N N2 F F2 ;
1005
1006 { factorialo 0 1 } fact
1007 { factorialo N F } {
1008     { N_>_0 N }
1009     { N2_is_N_-_1 N2 N }
1010     { factorialo N2 F2 }
1011     { F_is_F2_*_N F F2 N }
1012 } rule
1013
1014 { N_>_0 N } [ N of 0 > ] callback
1015
1016 { N2_is_N_-_1 N2 N } [ dup N of 1 - N2 unify ] callback
1017
1018 { F_is_F2_*_N F F2 N } [ dup [ N of ] [ F2 of ] bi * F unify ] callback"
1019 } $nl
1020 "Let's try " { $snippet "factorialo" } "." $nl
1021 { $unchecked-example
1022 "{ factorialo 0 F } query ."
1023 "{ H{ { F 1 } } }"
1024 }
1025 { $unchecked-example
1026 "{ factorialo 1 F } query ."
1027 "{ H{ { F 1 } } }"
1028 }
1029 { $unchecked-example
1030 "{ factorialo 10 F } query ."
1031 "{ H{ { F 3628800 } } }"
1032 } $nl
1033 { $snippet "logic" } " has features that make it easier to meet the typical requirements shown here." $nl
1034 "There are the built-in logic predicates " { $link (<) } ", " { $link (>) } ", " { $link (>=) } ", and " { $link (=<) } " to compare numbers. There are also " { $link (==) } " and " { $link (\==) } " to test for equality and inequality of two arguments." $nl
1035 "The word " { $link is } " takes a quotation and a logic variable to be unified. The quotation takes an environment and returns a value. And " { $link is } " returns the internal representation of the goal. " { $link is } " is intended to be used in a quotation. If there is a quotation in the definition of " { $link rule } ", " { $snippet "logic" } " uses the internal definition of the goal obtained by calling it." $nl
1036 "If you use these features to rewrite the definition of " { $snippet "factorialo" } ":" $nl
1037 { $code
1038 "USE: logic
1039
1040 LOGIC-PRED: factorialo
1041 LOGIC-VARS: N N2 F F2 ;
1042
1043 { factorialo 0 1 } fact
1044 { factorialo N F } {
1045     { (>) N 0 }
1046     [ [ N of 1 - ] N2 is ]
1047     { factorialo N2 F2 }
1048     [ [ [ F2 of ] [ N of ] bi * ] F is ]
1049 } rule"
1050 } $nl
1051 "Use the built-in logic predicate " { $link (=) } " for unification that does not require processing with a quotation. " { $link (\=) } " will be true when such a unification fails. Note that " { $link (\=) } " does not actually do the unification." $nl
1052 { $link varo } " takes a argument and is true if it is a logic variable with no value. On the other hand, " { $link nonvaro } " is true if its argument is not a logic variable or is a concrete logic variable." $nl
1053 "Now almost everything about " { $snippet "logic" } " is explained."
1054 ;
1055
1056 ABOUT: "logic"