Changeset 40402 in project


Ignore:
Timestamp:
08/29/21 23:24:48 (3 weeks ago)
Author:
Jeremy Steward
Message:

Actually useful miniKanren documentation

File:
1 edited

Legend:

Unmodified
Added
Removed
  • wiki/eggref/5/mini-kanren

    r39483 r40402  
    55This repository provides the [[https://github.com/miniKanren/miniKanren|canonical miniKanren
    66implementation]], wrapped as an egg
    7 for CHICKEN Scheme. The egg also includes extensions originally provided by
    8 Alex Shinn and modified to work with this version of miniKanren, which
    9 represent code and relations from *The Reasoned Schemer* (Dan Friedman, William
    10 Byrd, and Oleg Kiselyov, MIT Press.).
    11 
    12 '''Note''': This repository is mirrored on both
    13 [[https://bitbucket.org/ThatGeoGuy/chicken-minikanren/|Bitbucket]] and
    14 [[https://github.com/ThatGeoGuy/chicken-miniKanren|Github]]. To avoid
    15 duplication of effort, please submit issues via Bitbucket. I have enabled
    16 anonymous issue reporting in case you do not wish to create a Bitbucket account
    17 for the sake of uploading an issue.
    18 
    19 === From the miniKanren implementation
    20 
    21 Canonical miniKanren implementation.
    22 
    23 Implements the language described in the paper:
    24 
    25 William E. Byrd, Eric Holk, and Daniel P. Friedman. miniKanren, Live and Untagged: Quine Generation via Relational Interpreters (Programming Pearl). To appear in the Proceedings of the 2012 Workshop on Scheme and Functional Programming, Copenhagen, Denmark, 2012.
    26 
    27 ==== CORE LANGUAGE
    28 
    29 '''Logical operators:'''
    30 
    31 <constant>fresh</constant>
    32 <constant>conde</constant>
    33 
    34 '''Interface operators:'''
    35 
    36 <constant>run</constant>
    37 <constant>run\*</constant>
    38 
    39 ==== EXTENDED LANGUAGE
    40 
    41 '''Constraint operators:'''
    42 
    43 <constant>=/=</constant>
    44 <constant>symbolo</constant>
    45 <constant>numbero</constant>
    46 <constant>absento</constant>
     7for CHICKEN Scheme. The egg also includes extensions originally provided by Alex Shinn and modified
     8to work with this version of miniKanren, which represent code and relations from *The Reasoned
     9Schemer 2nd Ed.* (Dan Friedman, William Byrd, and Oleg Kiselyov, MIT Press.).
     10
     11[[toc:]]
     12
     13== Installation
     14
     15 $ chicken-install -s mini-kanren
     16
     17Or
     18
     19 $ chicken-install -s -test mini-kanren
     20
     21== Modules
     22
     23To get started with this egg, you can import {{mini-kanren}} module:
     24
     25 #;1> (import mini-kanren)
     26
     27== miniKanren Language
     28
     29The miniKanren language is a relational programming language described in the book
     30"[[https://mitpress.mit.edu/books/reasoned-schemer-second-edition|The Reasoned Schemer]]." For a
     31complete understanding of the language and how to use the various procedures provided by this egg,
     32it is suggested that one work through the Reasoned Schemer.
     33
     34If you cannot obtain a copy of the book, or simply wish to learn miniKanren through different means,
     35the official language page has a host of useful
     36[[http://minikanren.org/#writtenTutorials|tutorials]] for getting started.
     37
     38== Glossary
     39
     40Here is a list of terms that may pop up often in the documentation.
     41
     42; Succeed / success : A condition in which a goal has completed and unified any and all symbols relevant to the goal's definition.
     43; Fail / failure : A condition in which a goal has completed and has not unified all symbols passed to that goal.
     44; Goal : A statement within the miniKanren language that seeks to unify zero or more logic variables relevant to its definition. A goal can be thought of as a statment about some entity or entities, e.g. The goal {{(caro l a)}} unifies the variable {{a}} with the {{car}} of list {{l}}. A goal can be thought of as any relational procedure that returns a success or failure.
     45; Logic variable : A symbol representing some quantity (known or unknown) to be related by some goal(s). A variable is '''ground''' if-and-only-if it represents a single possible value. Otherwise, the variable is considered '''fresh'''
     46; Unification : the process in which a logic variable is ground to a value. E.g. the goal {{(== q 1)}} unifies the variable {{q}} to the value {{1}}. If {{q}} is already ground, this goal must fail.  However, if {{q}} is fresh, then this goal succeeds and the logic variable {{q}} is thereafter ground.
     47
     48== Egg / Language API
     49
     50=== Core Language
     51
     52==== Interface operators
     53
     54<macro>(run* (x) goal0 goal ...)</macro>
     55
     56Primary interface operator for miniKanren. {{run*}} instantiates a fresh variable {{x}}, and runs
     57through each subsequent goal provided. It returns a list of all possible unifications of {{x}} where
     58goals {{goal0}}, {{goal}}, and so on succeed.
     59
     60'''Note''': As long as there are a finite number of possible values that can be unified with {{x}},
     61then {{run*}} is guaranteed to terminate. However, this importantly doesn't make two guarantees:
     62
     63*# The speed at which the answers will be found. The runtime is generally fast, but miniKanren, and more generally relational and logic programming necessarily requires one to think about the best way to prune the search space of possible answers.
     64*# The order of answers in {{x}} that satisfy the goals.
     65
     66<macro>(run n (x) goal0 goal ...)</macro>
     67
     68Interface operator for miniKanren. Behaves like {{run*}}, except that it will only provide up to
     69{{n}} possible unifications of {{x}}. This is useful if there are a finite number of solutions and
     70one wants to merely ''take'' the first {{n}} possible solutions.
     71
     72==== Logical Operators
     73
     74<constant>succeed</constant>
     75
     76A goal that is always successful. Equivalent to {{(== #f #f)}}.
     77
     78<constant>fail</constant>
     79
     80A goal that always fails. Equivalent to {{(== #t #f)}}.
     81
     82<macro>(fresh (a ...) goal0 goal ...)</macro>
     83
     84Creates a logic variable bound to each of the symbol(s) {{(a ...)}}. These logic variables are then
     85lexically scoped within this macro, whereupon each of the subsequent goals can be evaluated.
     86
     87Example:
     88
     89<enscript highlight="scheme">
     90(run* (q)
     91  (fresh (a d)
     92    (== a 1)
     93    (nullo d)
     94    (conso a d q)))
     95; => ((1))
     96</enscript>
     97
     98<macro>(conde (goal0 goal ...) (goal0^ goal^ ...) ...)</macro>
     99
     100Conditional performing logical disjunction over each set of {{(goal0 goal ...)}} clauses. The first
     101goal in each clause (i.e. {{goal0}} or {{goal0^}}) is considered the head of that clause. Behaves
     102similarly to {{cond}} in regular Scheme, except that each clause provides one possible path to
     103unification through the subsequent goals.
     104
     105In the first edition of miniKanren, {{conde}} was separate from {{condi}}, which is no longer
     106provided as part of the language. {{conde}} now interleaves each of the possible clauses on
     107recursive calls, so {{condi}} (which used to stand for interleaving-conditional) is no longer
     108needed.
     109
     110<macro>(conda (goal0 goal ...) (goal0^ goal^ ...) ...)</macro>
     111
     112Conditional behaving much like {{conde}}, except that {{conda}} does a soft-cut over the remaining
     113goals. That is to say, if any of the heads of the clauses succeed, then the remaining clauses will
     114all be ''cut'' (i.e. ignored) from future searches.
     115
     116<macro>(ifa (goal0 goal ...) b ...)</macro>
     117
     118Single-branch version of {{conda}}. {{ifa}} relates to {{conda}} the way that {{if}} relates to
     119{{cond}} in regular Scheme.
     120
     121<macro>(condu (goal0 goal ...) (goal0^ goal^ ...) ...)</macro>
     122
     123Conditional behaving much like {{conde}}, except that {{condu}} performs a ''committed choice''.
     124What that means is that if the head of any goal succeeds, then the remaining goals of that clause
     125will only be run once thereafter.
     126
     127<macro>(ifu (goal0 goal ...) b ...)</macro>
     128
     129Single-branch version of {{condu}}. {{ifu}} relates to {{condu}} the way that {{if}} relates to
     130{{cond}} in regular Scheme.
     131
     132<procedure>(== u v)</procedure>
     133
     134Primary unification goal. {{u}} and {{v}} are either logic variables or values. If the two can
     135be unified (i.e. if the two logic variables hold the same value, or if two values are the same) then
     136this goal succeeds. When used on fresh variables, guarantees that the two logic variables will always
     137be unified.
     138
     139<procedure>(=/= u v)</procedure>
     140
     141Disequality goal. This goal succeeds if-and-only-if {{u}} and {{v}} are not unified. When used on
     142fresh variables, ensures that {{u}} and {{v}} never unify.
     143
     144<procedure>(var? v)</procedure>
     145
     146Predicate procedure (not a goal) that returns true if-and-only-if {{v}} is a logic variable.
     147
     148<macro>(project (x ...) goal0 goal ...)</macro>
     149
     150Extracts the value of zero or more logic variables into lexical variables of the same name, and
     151executes the goals within the body of the {{project}} call.
     152
     153Example:
     154
     155<enscript highlight="scheme">
     156;; The following code will fail because `+` is not relational.
     157(run 1 (q)
     158  (fresh (a b)
     159    (== a 1)
     160    (== b 2)
     161    (== q (+ a b))))
     162
     163; => Error: (+) bad argument type - not a number: #(a)
     164
     165
     166;; However, if we use project to get the values of the logic variables,
     167;; we can use those directly.
     168(run 1 (q)
     169  (fresh (a b)
     170    (== a 1)
     171    (== b 1)
     172    (project (a b)
     173      (== q (+ a b)))))
     174
     175; => (3)
     176</enscript>
     177
     178{{project}} can be though of as an escape hatch to break out of miniKanren. It will give you the
     179values of the variables, but it only works if the variables are grounded. In the above example, if
     180the logic variable {{b}} is not ground, then the {{b}} inside the body of {{project}} will not be
     181lexically bound to anything, and will still be a fresh logic variable.
     182
     183In most cases it is advised to avoid {{project}} when you can. It can be a powerful tool for
     184debugging the values of logic variables when writing miniKanren code; however, excessive use will
     185lead to extremely non-relational code that will be hard to work with in miniKanren.
     186
     187<procedure>(onceo goal)</procedure>
     188
     189A procedure that ensures that {{goal}} executes exactly one time.
     190
     191==== Predicate Goals
     192
     193<procedure>(make-tag-A tag pred)</procedure>
     194
     195Constructs a goal that succeeds whenever {{pred}} returns {{#t}} for a single value, and fails if
     196{{pred}} returns {{#f}} for that value. This creates a predicate-goal that tags the logic variable
     197with the tag name {{tag}}.
     198
     199'''Note''': This is primarily useful for atomic-type predicates, i.e. predicates for atomic types
     200that do not have explicit constructors. This is what is used to implement {{symbolo}}, for example:
     201
     202<enscript highlight"scheme">
     203(define symbolo (make-tag-A 'sym symbol?))
     204</enscript>
     205
     206One should avoid using this for types that have constructors (e.g. pairs have {{cons}}, lists have
     207{{list}}), and should instead prefer creating relational constructors for such types. This egg
     208provides {{symbolo}}, {{numbero}}, {{booleano}}, {{charo}}, and {{atomo}} using this method.
     209However, {{make-tag-A}} is highlighted here in case users have new atomic types that they wish to
     210extend miniKanren with.
     211
     212<procedure>(symbolo s)</procedure>
     213
     214A tagged constraint goal that succeeds if-and-only-if {{s}} can be unified with a symbol.
     215
     216<procedure>(numbero n)</procedure>
     217
     218A tagged constraint goal that succeeds if-and-only-if {{n}} can be unified with a number.
     219
     220<procedure>(booleano b)</procedure>
     221
     222Predicate goal that succeeds if-and-only-if {{b}} can be unified with a boolean. When {{b}} is
     223fresh, this guarantees that {{b}} can only be unified with {{#t}} or {{#f}}.
     224
     225<procedure>(charo c)</procedure>
     226
     227A tagged constraint goal that succeeds if-and-only-if {{c}} can be unified with a character.
     228
     229<procedure>(atomo a)</procedure>
     230
     231A tagged constraint goal that succeeds if-and-only-if {{a}} can be unified with an atom.
     232
     233<procedure>(nullo p)</procedure>
     234
     235Predicate goal that succeeds if-and-only-if {{p}} is the null list. When {{p}} is fresh, it
     236guarantees that {{p}} can only unify with the null list {{'()}}.
     237
     238<procedure>(pairo p)</procedure>
     239
     240Predicate goal that succeeds if-and-only-if {{p}} unifies with any pair. When {{p}} is fresh, it
     241guarantees that {{p}} can only unify with a pair.
     242
     243<procedure>(listo l)</procedure>
     244
     245Predicate goal that succeeds if-and-only-if {{l}} unifies with any list. When {{l}} is fresh, it
     246guarantees that {{l}} can only unify with a proper list.
     247
     248=== Numbers in miniKanren
     249
     250The procedures defined here are largely the same as in ''The Reasoned Schemer''. As it turns out,
     251constructing relations over numbers is very hard. Specifically, relations involving decimal number
     252systems are very hard. It is much easier when representing numbers as bits, where operations on each
     253bit can be performed relationally.
     254
     255While individual numbers can be unified in the miniKanren language, doing any kind of arithmetic on
     256them will be quite difficult if you want to keep everything relational. To get around this, we first
     257convert numbers into a list of bits in little-endian order, and perform relations on those lists.
     258From there, we can convert to / from bit-lists in order to switch between decimal representations
     259(e.g 1, 2, 7, 42, ...) and bit representations (e.g. 0 is {{'()}}, 1 is {{(1)}}, 2 is {{(0 1)}},
     260etc.).
     261
     262As you might guess, this can end up making many numerical operations quite slow, especially for
     263large numbers. There are some ways to get around this by introducing finite domains, but this egg
     264does not currently provide operations on finite domains of numbers. Likewise, {{project}} is always
     265an option, but remember: it is an escape hatch and is not generally recommended.
     266
     267Floating point / inexact numbers are not supported in miniKanren.
     268
     269Negative numbers are not supported in miniKanren.
     270
     271<procedure>(build-num n)</procedure>
     272
     273Constructs a bit-list to represent a number given a positive exact number.
     274
     275Example:
     276
     277<enscript highlight="scheme">
     278(build-num 0) ; => ()
     279(build-num 1) ; => (1)
     280(build-num 2) ; => (0 1)
     281</enscript>
     282
     283<procedure>(little-endian->number b)</procedure>
     284
     285Procedure that converts a bit-list in little-endian form back into a Scheme number. The opposite of
     286{{build-num}}.
     287
     288<procedure>(zeroo n)</procedure>
     289
     290A goal that succeeds if-and-only-if the logic variable {{n}} is zero (i.e. null bit list). When
     291{{n}} is fresh, this guarantees that it can only ever be bound to the null list. This makes it
     292equivalent to {{(nullo n)}}.
     293
     294<procedure>(poso n)</procedure>
     295
     296A goal that succeeds if-and-only-if the logic variable {{n}} is a positive number (i.e. non-null bit
     297list). When {{n}} is fresh, this guarantees that it can only ever be bound to a non-null bit list.
     298This makes it equivalent to {{(listo n)}}.
     299
     300<procedure>(pluso n m k)</procedure>
     301<procedure>(+o n m k)</procedure>
     302
     303A goal that unifies two logic variables {{n}} and {{m}} such that the bit-lists they represent sum
     304to {{k}} when added. Think of this as if you were doing {{(define k (+ n m))}}, except that it is
     305relational.
     306
     307Example:
     308
     309<enscript highlight="scheme">
     310(run 1 (q)
     311  (let ((a (build-num 4))
     312        (b (build-num 3)))
     313    (fresh (n k)
     314      (== k a)
     315      (== n b)
     316      (pluso n q k))))
     317; => (1)
     318</enscript>
     319
     320<procedure>(minuso n m k)</procedure>
     321<procedure>(-o n m k)</procedure>
     322
     323A goal that unifies two logic variables {{n}} and {{m}} such that the bit-lists they represent
     324subtract to {{k}}. Think of this as if you were doing {{define k (- n m))}}, except that it is
     325relational.
     326
     327<procedure>(*o n m p)</procedure>
     328
     329A goal that unifies two logic variables {{n}} and {{m}} such that the bit-lists they represent
     330multiply to {{k}}. Think of this as if you were doing {{(define k (* n m))}}, except that it is
     331relational.
     332
     333<procedure>(/o n m q r)</procedure>
     334
     335A goal that unifies two logic variables {{n}} and {{m}} such that the bit-lists they represent
     336divide to the quotient {{q}} with remainder {{r}}.
     337
     338<procedure>(<o n m)</procedure>
     339<procedure>(<=o n m)</procedure>
     340
     341Predicate goals that succeed if-and-only-if {{n}} is less than (or equal to, in the latter case)
     342{{m}}.
     343
     344<procedure>(logo n b q r)</procedure>
     345
     346Goal that unifies two logic variables {{n}} (number) and {{b}} (base) such that they form the
     347logarithm with power {{q}} and remainder {{r}}.
     348
     349<procedure>(expo b q n)</procedure>
     350
     351Goal that unifies the two logic variables {{b}} and {{q}} such that they form the exponential {{n}}.
     352Think of this as doing {{(define n (expt b q))}}, except that it is relational.
     353
     354=== Extras
     355
     356<procedure>(caro p a)</procedure>
     357
     358Goal that unifies a logic variable representing a pair {{p}} with the car of that pair, {{a}}.
     359
     360<procedure>(cdro p d)</procedure>
     361
     362Goal that unifies a logic variable representing a pair {{p}} with the cdr of that pair, {{d}}.
     363
     364<procedure>(conso a d p)</procedure>
     365
     366Goal that unifies two logic variables {{a}} and {{d}}, representing the car and cdr of a pair, with
     367the logic variable representing the pair {{p}}.
     368
     369<procedure>(membero x l)</procedure>
     370
     371Goal that unifies {{x}} with any member of the list {{l}}.
     372
     373<procedure>(rembero x l out)</procedure>
     374
     375Goal that unifies {{out}} with a list where {{x}} has been removed from {{l}}.
     376
     377<procedure>(appendo l s out)</procedure>
     378
     379Goal that unifies two lists {{l}} and {{s}} with a list {{out}}, which is the two lists appended to
     380one another.
     381
     382<procedure>(flatteno s out)</procedure>
     383
     384Goal that unifies a list {{s}} with {{out}}, where {{out}} represents a list with the same elements
     385of {{s}}, except that {{out}} is flattened (i.e. only contains atoms, not pairs).
     386
     387<procedure>(lengtho s n)</procedure>
     388
     389Goal that unifies a list {{s}} with the length of that list {{k}}.
     390
     391<procedure>(anyo goal)</procedure>
     392
     393Goal that succeeds if {{goal}} succeeds.
     394
     395<constant>nevero</constant>
     396
     397Goal that always fails. Equivalent to {{(anyo fail)}}.
     398
     399<constant>alwayso</constant>
     400
     401Goal that always succeeds.
     402
     403<procedure>(distincto s)</procedure>
     404
     405Goal that guarantees that no element of the list {{s}} will ever unify with another element of
     406{{s}}.
     407
     408<procedure>(permuteo xl yl)</procedure>
     409
     410Goal that permutes {{xl}} into {{yl}}. It may not terminate if {{xl}} is not ground.
     411
     412Example:
     413
     414<enscript highlight="scheme">
     415;; Get 5-permute-2, i.e. all 2 permutations of the numbers 1 through 5.
     416(run* (q)
     417  (lengtho q (build-num 2))
     418  (permuteo '(1 2 3 4 5) q))
     419
     420; => (1 2) (2 1) (2 3) (1 3) (3 1) (3 2) (3 4) (2 4) (1 4) (4 1) (4 2)
     421;    (4 3) (3 5) (4 5) (2 5) (1 5) (5 1) (5 2) (5 3) (5 4))
     422</enscript>
     423
     424== Repository
     425
     426Find the project on [[https://github.com/ThatGeoGuy/chicken-miniKanren|Github]].
     427
     428== Version History
     429
     430; 1.2.0 : Adds {{flatteno}}, {{lengtho}}, {{distincto}}, and {{permuteo}}
     431; 1.1.1 : Removes {{test}} egg from test-dependencies.
     432; 1.1 : CHICKEN 5 support
     433
     434== License
     435
     436<enscript highlight="none">
     437The MIT License (MIT)
     438
     439Copyright (c) 2014 Daniel P. Friedman, Oleg Kiselyov, and William E. Byrd
     440Modifications Copyright (c) 2016 Alex Shinn, Jeremy Steward
     441
     442Permission is hereby granted, free of charge, to any person obtaining a copy
     443of this software and associated documentation files (the "Software"), to deal
     444in the Software without restriction, including without limitation the rights
     445to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
     446copies of the Software, and to permit persons to whom the Software is
     447furnished to do so, subject to the following conditions:
     448
     449The above copyright notice and this permission notice shall be included in all
     450copies or substantial portions of the Software.
     451
     452THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
     453IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
     454FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
     455AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
     456LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
     457OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
     458SOFTWARE.
     459</enscript>
Note: See TracChangeset for help on using the changeset viewer.