diff options
| -rw-r--r-- | prolog/README.html | 453 | ||||
| -rw-r--r-- | prolog/README.md | 148 | ||||
| -rw-r--r-- | prolog/star-wars.jpg | bin | 0 -> 530628 bytes | |||
| -rw-r--r-- | prolog/workbench.jpg | bin | 0 -> 1815874 bytes |
4 files changed, 590 insertions, 11 deletions
diff --git a/prolog/README.html b/prolog/README.html new file mode 100644 index 0000000..e521647 --- /dev/null +++ b/prolog/README.html @@ -0,0 +1,453 @@ +<!DOCTYPE html> +<html> +<head> + <meta charset="utf-8"> + <meta name="generator" content="pandoc"> + <meta name="author" content="arnaud@pankzsoft.com - @abailly.bsky.social"> + <meta name="dcterms.date" content="2025-12-10"> + <title>Implementing Prolog</title> + <meta name="apple-mobile-web-app-capable" content="yes"> + <meta name="apple-mobile-web-app-status-bar-style" content="black-translucent"> + <meta name="viewport" content="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no, minimal-ui"> + <link rel="stylesheet" href="https://unpkg.com/reveal.js@^5/dist/reset.css"> + <link rel="stylesheet" href="https://unpkg.com/reveal.js@^5/dist/reveal.css"> + <style> + .reveal .sourceCode { /* see #7635 */ + overflow: visible; + } + /* Default styles provided by pandoc. + ** See https://pandoc.org/MANUAL.html#variables-for-html for config info. + */ + code{white-space: pre-wrap;} + span.smallcaps{font-variant: small-caps;} + div.columns{display: flex; gap: min(4vw, 1.5em);} + div.column{flex: auto; overflow-x: auto;} + div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;} + /* The extra [class] is a hack that increases specificity enough to + override a similar rule in reveal.js */ + ul.task-list[class]{list-style: none;} + ul.task-list li input[type="checkbox"] { + font-size: inherit; + width: 0.8em; + margin: 0 0.8em 0.2em -1.6em; + vertical-align: middle; + } + .display.math{display: block; text-align: center; margin: 0.5rem auto;} + /* CSS for syntax highlighting */ + html { -webkit-text-size-adjust: 100%; } + pre > code.sourceCode { white-space: pre; position: relative; } + pre > code.sourceCode > span { display: inline-block; line-height: 1.25; } + pre > code.sourceCode > span:empty { height: 1.2em; } + .sourceCode { overflow: visible; } + code.sourceCode > span { color: inherit; text-decoration: inherit; } + div.sourceCode { margin: 1em 0; } + pre.sourceCode { margin: 0; } + @media screen { + div.sourceCode { overflow: auto; } + } + @media print { + pre > code.sourceCode { white-space: pre-wrap; } + pre > code.sourceCode > span { text-indent: -5em; padding-left: 5em; } + } + pre.numberSource code + { counter-reset: source-line 0; } + pre.numberSource code > span + { position: relative; left: -4em; counter-increment: source-line; } + pre.numberSource code > span > a:first-child::before + { content: counter(source-line); + position: relative; left: -1em; text-align: right; vertical-align: baseline; + border: none; display: inline-block; + -webkit-touch-callout: none; -webkit-user-select: none; + -khtml-user-select: none; -moz-user-select: none; + -ms-user-select: none; user-select: none; + padding: 0 4px; width: 4em; + } + pre.numberSource { margin-left: 3em; padding-left: 4px; } + div.sourceCode + { color: #cccccc; background-color: #303030; } + @media screen { + pre > code.sourceCode > span > a:first-child::before { text-decoration: underline; } + } + code span.al { color: #ffcfaf; } /* Alert */ + code span.an { color: #7f9f7f; font-weight: bold; } /* Annotation */ + code span.at { } /* Attribute */ + code span.bn { color: #dca3a3; } /* BaseN */ + code span.bu { } /* BuiltIn */ + code span.cf { color: #f0dfaf; } /* ControlFlow */ + code span.ch { color: #dca3a3; } /* Char */ + code span.cn { color: #dca3a3; font-weight: bold; } /* Constant */ + code span.co { color: #7f9f7f; } /* Comment */ + code span.cv { color: #7f9f7f; font-weight: bold; } /* CommentVar */ + code span.do { color: #7f9f7f; } /* Documentation */ + code span.dt { color: #dfdfbf; } /* DataType */ + code span.dv { color: #dcdccc; } /* DecVal */ + code span.er { color: #c3bf9f; } /* Error */ + code span.ex { } /* Extension */ + code span.fl { color: #c0bed1; } /* Float */ + code span.fu { color: #efef8f; } /* Function */ + code span.im { } /* Import */ + code span.in { color: #7f9f7f; font-weight: bold; } /* Information */ + code span.kw { color: #f0dfaf; } /* Keyword */ + code span.op { color: #f0efd0; } /* Operator */ + code span.ot { color: #efef8f; } /* Other */ + code span.pp { color: #ffcfaf; font-weight: bold; } /* Preprocessor */ + code span.sc { color: #dca3a3; } /* SpecialChar */ + code span.ss { color: #cc9393; } /* SpecialString */ + code span.st { color: #cc9393; } /* String */ + code span.va { } /* Variable */ + code span.vs { color: #cc9393; } /* VerbatimString */ + code span.wa { color: #7f9f7f; font-weight: bold; } /* Warning */ + </style> + <link rel="stylesheet" href="https://unpkg.com/reveal.js@^5/dist/theme/black.css" id="theme"> +</head> +<body> + <div class="reveal"> + <div class="slides"> + +<section id="title-slide"> + <h1 class="title">Implementing Prolog</h1> + <p class="subtitle">A λ-Nantes Workshop</p> + <p class="author">arnaud@pankzsoft.com - <span class="citation" +data-cites="abailly.bsky.social">@abailly.bsky.social</span></p> + <p class="date">2025-12-10</p> +</section> + +<section> +<section id="usage" class="title-slide slide level1"> +<h1>Usage</h1> +<p><img data-src="star-wars.jpg" /></p> +</section> +<section id="example" class="slide level2"> +<h2>Example</h2> +<p>A <em>program</em> about Star Wars characters (including the crappy +recent ones)</p> +</section> +<section id="example---facts" class="slide level2"> +<h2>Example - Facts</h2> +<p>Simple facts asserting the gender of some characters.</p> +<div class="sourceCode" id="cb1"><pre +class="sourceCode prolog"><code class="sourceCode prolog"><span id="cb1-1"><a href="#cb1-1" aria-hidden="true" tabindex="-1"></a>female(leia)<span class="kw">.</span></span> +<span id="cb1-2"><a href="#cb1-2" aria-hidden="true" tabindex="-1"></a>male(vader)<span class="kw">.</span></span> +<span id="cb1-3"><a href="#cb1-3" aria-hidden="true" tabindex="-1"></a>male(luke)<span class="kw">.</span></span> +<span id="cb1-4"><a href="#cb1-4" aria-hidden="true" tabindex="-1"></a>male(kylo)<span class="kw">.</span></span></code></pre></div> +</section> +<section id="example---facts-1" class="slide level2"> +<h2>Example - Facts</h2> +<p>More complex facts asserting a <code>child</code>hood +<em>relation</em> between some characters.</p> +<div class="sourceCode" id="cb2"><pre +class="sourceCode prolog"><code class="sourceCode prolog"><span id="cb2-1"><a href="#cb2-1" aria-hidden="true" tabindex="-1"></a>child(luke<span class="kw">,</span> vader)<span class="kw">.</span></span> +<span id="cb2-2"><a href="#cb2-2" aria-hidden="true" tabindex="-1"></a>child(leia<span class="kw">,</span> vader)<span class="kw">.</span></span> +<span id="cb2-3"><a href="#cb2-3" aria-hidden="true" tabindex="-1"></a>child(kylo<span class="kw">,</span> leia)<span class="kw">.</span></span></code></pre></div> +</section> +<section id="example---rules" class="slide level2"> +<h2>Example - Rules</h2> +<p><em>Rules</em> (or <em>Clauses</em>) allowing to infer some relation +from other relations.</p> +<div class="sourceCode" id="cb3"><pre +class="sourceCode prolog"><code class="sourceCode prolog"><span id="cb3-1"><a href="#cb3-1" aria-hidden="true" tabindex="-1"></a>son(<span class="dt">X</span><span class="kw">,</span><span class="dt">Y</span>) <span class="kw">:-</span> male(<span class="dt">X</span>)<span class="kw">,</span> child(<span class="dt">X</span><span class="kw">,</span><span class="dt">Y</span>)<span class="kw">.</span></span> +<span id="cb3-2"><a href="#cb3-2" aria-hidden="true" tabindex="-1"></a>daughter(<span class="dt">X</span><span class="kw">,</span><span class="dt">Y</span>) <span class="kw">:-</span> female(<span class="dt">X</span>)<span class="kw">,</span> child(<span class="dt">X</span><span class="kw">,</span><span class="dt">Y</span>)<span class="kw">.</span></span></code></pre></div> +</section> +<section id="example---rules-1" class="slide level2"> +<h2>Example - Rules</h2> +<p>More complex rules asserting a transitive relation</p> +<div class="sourceCode" id="cb4"><pre +class="sourceCode prolog"><code class="sourceCode prolog"><span id="cb4-1"><a href="#cb4-1" aria-hidden="true" tabindex="-1"></a>grandchild(<span class="dt">X</span><span class="kw">,</span><span class="dt">Z</span>) <span class="kw">:-</span> child(<span class="dt">X</span><span class="kw">,</span><span class="dt">Y</span>)<span class="kw">,</span> child(<span class="dt">Y</span><span class="kw">,</span><span class="dt">Z</span>)<span class="kw">.</span></span></code></pre></div> +</section> +<section id="example---query" class="slide level2"> +<h2>Example - Query</h2> +<p>We can <em>query</em> this program, for example asking who is a +grandchild of Darth Vader</p> +<div class="sourceCode" id="cb5"><pre +class="sourceCode prolog"><code class="sourceCode prolog"><span id="cb5-1"><a href="#cb5-1" aria-hidden="true" tabindex="-1"></a><span class="dt">></span> <span class="fu">?-</span> grandchild(<span class="dt">X</span><span class="er">,</span> vader)<span class="kw">.</span></span> +<span id="cb5-2"><a href="#cb5-2" aria-hidden="true" tabindex="-1"></a>success<span class="kw">.</span> <span class="dt">Type</span> [<span class="dt">Enter</span>] to list solutions<span class="kw">.</span></span> +<span id="cb5-3"><a href="#cb5-3" aria-hidden="true" tabindex="-1"></a><span class="dt">></span></span> +<span id="cb5-4"><a href="#cb5-4" aria-hidden="true" tabindex="-1"></a><span class="er">[</span><span class="dt">X</span> <span class="kw">-></span> kylo<span class="er">]</span></span></code></pre></div> +</section> +<section id="example---query-1" class="slide level2"> +<h2>Example - Query</h2> +<p>A Prolog query can have several answers:</p> +<div class="sourceCode" id="cb6"><pre +class="sourceCode prolog"><code class="sourceCode prolog"><span id="cb6-1"><a href="#cb6-1" aria-hidden="true" tabindex="-1"></a><span class="dt">></span> <span class="fu">?-</span> child(<span class="dt">X</span><span class="er">,</span> vader)<span class="kw">.</span></span> +<span id="cb6-2"><a href="#cb6-2" aria-hidden="true" tabindex="-1"></a>success<span class="kw">.</span> <span class="dt">Type</span> [<span class="dt">Enter</span>] to list solutions<span class="kw">.</span></span> +<span id="cb6-3"><a href="#cb6-3" aria-hidden="true" tabindex="-1"></a><span class="dt">></span></span> +<span id="cb6-4"><a href="#cb6-4" aria-hidden="true" tabindex="-1"></a><span class="er">[</span><span class="dt">X</span> <span class="kw">-></span> luke<span class="er">]</span></span> +<span id="cb6-5"><a href="#cb6-5" aria-hidden="true" tabindex="-1"></a><span class="dt">></span></span> +<span id="cb6-6"><a href="#cb6-6" aria-hidden="true" tabindex="-1"></a><span class="er">[</span><span class="dt">X</span> <span class="kw">-></span> leia<span class="er">]</span></span></code></pre></div> +</section> +<section id="example---query-2" class="slide level2"> +<h2>Example - Query</h2> +<p>Or no answer:</p> +<div class="sourceCode" id="cb7"><pre +class="sourceCode prolog"><code class="sourceCode prolog"><span id="cb7-1"><a href="#cb7-1" aria-hidden="true" tabindex="-1"></a><span class="dt">></span> <span class="fu">?-</span> grandchild(leia<span class="er">,</span> <span class="dt">X</span>)<span class="kw">.</span></span> +<span id="cb7-2"><a href="#cb7-2" aria-hidden="true" tabindex="-1"></a>failure</span></code></pre></div> +</section></section> +<section> +<section id="implementation" class="title-slide slide level1"> +<h1>Implementation</h1> + +</section> +<section id="terms" class="slide level2"> +<h2>Terms</h2> +<ul> +<li class="fragment">variables start with upper casae: <code>X</code>, +<code>Y</code>…</li> +<li class="fragment">symbols start with lower case: <code>s</code>, +<code>z</code>, <code>child</code>, …</li> +<li class="fragment">symbols have 0 or more arguments, e.g an +<em>arity</em> : <code>bob</code>, <code>child(X, Y)</code>, +<code>father(bob, Z)</code>…</li> +</ul> +</section> +<section id="clauses" class="slide level2"> +<h2>Clauses</h2> +<ul> +<li class="fragment"><em>head</em>: a single term</li> +<li class="fragment"><em>premises</em>: a (possibly empty) list of +terms</li> +<li class="fragment">a <em>data set</em> (or a <em>program</em>) is a +list of clauses or <em>facts</em></li> +<li class="fragment">a <em>query</em> is a term introduced with +<code>?-</code></li> +</ul> +</section> +<section id="basic-algorithm" class="slide level2"> +<h2>Basic algorithm</h2> +<p>Given a query and a set of clauses, a Prolog interpreter loop goes +like:</p> +<ol type="1"> +<li class="fragment">Push <em>query</em> on its goal stack</li> +<li class="fragment">Pop up current <em>goal</em> from the stack</li> +<li class="fragment">Try to match <em>goal</em> with each +<em>clause</em>: +<ol type="a"> +<li class="fragment"><em>Unify</em> goal with the <em>head</em> of +<em>clause</em> with <em>fresh</em> variables</li> +<li class="fragment">If unification succeeds, push <em>premises</em> of +clause onto goals stack</li> +</ol></li> +<li class="fragment">Query succeeds if stack is empty with a successful +match</li> +</ol> +</section> +<section id="unification" class="slide level2"> +<h2>Unification</h2> +<p>Given two terms <span +class="math inline"><em>t</em><sub>1</sub></span> and <span +class="math inline"><em>t</em><sub>2</sub></span> with <em>free +variables</em> <span +class="math inline"><em>f</em><em>v</em>(<em>t</em><sub>1</sub>)</span>, +<span +class="math inline"><em>f</em><em>v</em>(<em>t</em><sub>2</sub>)</span>, +unification is the process of defining a <em>substitution</em> between +variables and <em>terms</em></p> +<p><span +class="math display"><em>σ</em> : <em>f</em><em>v</em>(<em>t</em><sub>1</sub>) ∪ <em>f</em><em>v</em>(<em>t</em><sub>2</sub>) → <em>T</em></span></p> +</section> +<section id="unification-1" class="slide level2"> +<h2>Unification</h2> +<ul> +<li class="fragment">Two variables unify with each other</li> +<li class="fragment">A variable unifies with a term if not already +mapped</li> +<li class="fragment">Two relations unify with each other iff +<ul> +<li class="fragment">Their symbol is the same</li> +<li class="fragment">Their arguments unify with each other</li> +</ul></li> +</ul> +</section> +<section id="unification-2" class="slide level2"> +<h2>Unification</h2> +<ul> +<li class="fragment"><span +class="math inline"><em>σ</em>(<em>X</em>, <em>Y</em>) = {<em>X</em> ↦ <em>Y</em>}</span></li> +<li class="fragment"><span +class="math inline"><em>σ</em>(<em>X</em>, <em>f</em><em>o</em><em>o</em>) = {<em>X</em> ↦ <em>f</em><em>o</em><em>o</em>}</span></li> +<li class="fragment"><span +class="math inline"><em>σ</em>(<em>f</em><em>o</em><em>o</em>, <em>X</em>) = {<em>X</em> ↦ <em>f</em><em>o</em><em>o</em>}</span></li> +<li class="fragment"><span +class="math inline"><em>σ</em>(<em>f</em><em>o</em><em>o</em>(<em>b</em><em>a</em><em>r</em>, <em>Y</em>), <em>f</em><em>o</em><em>o</em>(<em>X</em>, <em>Z</em>)) = {<em>X</em> ↦ <em>b</em><em>a</em><em>r</em>, <em>Y</em> ↦ <em>Z</em>}</span></li> +</ul> +</section></section> +<section> +<section id="practice" class="title-slide slide level1"> +<h1>Practice</h1> +<p><img data-src="workbench.jpg" /></p> +</section> +<section id="references" class="slide level2"> +<h2>References</h2> +<ul> +<li class="fragment"><a +href="https://github.com/norm2782/NanoProlog">NanoProlog</a></li> +<li class="fragment"><a +href="https://github.com/abailly/hslogic">hslogic</a></li> +<li class="fragment"><a +href="https://github.com/andrejbauer/plzoo/tree/master/src/miniprolog">miniprolog</a></li> +</ul> +</section></section> + </div> + </div> + + <script src="https://unpkg.com/reveal.js@^5/dist/reveal.js"></script> + + <!-- reveal.js plugins --> + <script src="https://unpkg.com/reveal.js@^5/plugin/notes/notes.js"></script> + <script src="https://unpkg.com/reveal.js@^5/plugin/search/search.js"></script> + <script src="https://unpkg.com/reveal.js@^5/plugin/zoom/zoom.js"></script> + + <script> + + // Full list of configuration options available at: + // https://revealjs.com/config/ + Reveal.initialize({ + // Display controls in the bottom right corner + controls: true, + + // Help the user learn the controls by providing hints, for example by + // bouncing the down arrow when they first encounter a vertical slide + controlsTutorial: true, + + // Determines where controls appear, "edges" or "bottom-right" + controlsLayout: 'bottom-right', + + // Visibility rule for backwards navigation arrows; "faded", "hidden" + // or "visible" + controlsBackArrows: 'faded', + + // Display a presentation progress bar + progress: true, + + // Display the page number of the current slide + slideNumber: false, + + // 'all', 'print', or 'speaker' + showSlideNumber: 'all', + + // Add the current slide number to the URL hash so that reloading the + // page/copying the URL will return you to the same slide + hash: true, + + // Start with 1 for the hash rather than 0 + hashOneBasedIndex: false, + + // Flags if we should monitor the hash and change slides accordingly + respondToHashChanges: true, + + // Push each slide change to the browser history + history: false, + + // Enable keyboard shortcuts for navigation + keyboard: true, + + // Enable the slide overview mode + overview: true, + + // Disables the default reveal.js slide layout (scaling and centering) + // so that you can use custom CSS layout + disableLayout: false, + + // Vertical centering of slides + center: true, + + // Enables touch navigation on devices with touch input + touch: true, + + // Loop the presentation + loop: false, + + // Change the presentation direction to be RTL + rtl: false, + + // see https://revealjs.com/vertical-slides/#navigation-mode + navigationMode: 'default', + + // Randomizes the order of slides each time the presentation loads + shuffle: false, + + // Turns fragments on and off globally + fragments: true, + + // Flags whether to include the current fragment in the URL, + // so that reloading brings you to the same fragment position + fragmentInURL: true, + + // Flags if the presentation is running in an embedded mode, + // i.e. contained within a limited portion of the screen + embedded: false, + + // Flags if we should show a help overlay when the questionmark + // key is pressed + help: true, + + // Flags if it should be possible to pause the presentation (blackout) + pause: true, + + // Flags if speaker notes should be visible to all viewers + showNotes: false, + + // Global override for autoplaying embedded media (null/true/false) + autoPlayMedia: null, + + // Global override for preloading lazy-loaded iframes (null/true/false) + preloadIframes: null, + + // Number of milliseconds between automatically proceeding to the + // next slide, disabled when set to 0, this value can be overwritten + // by using a data-autoslide attribute on your slides + autoSlide: 0, + + // Stop auto-sliding after user input + autoSlideStoppable: true, + + // Use this method for navigation when auto-sliding + autoSlideMethod: null, + + // Specify the average time in seconds that you think you will spend + // presenting each slide. This is used to show a pacing timer in the + // speaker view + defaultTiming: null, + + // Enable slide navigation via mouse wheel + mouseWheel: false, + + // The display mode that will be used to show slides + display: 'block', + + // Hide cursor if inactive + hideInactiveCursor: true, + + // Time before the cursor is hidden (in ms) + hideCursorTime: 5000, + + // Opens links in an iframe preview overlay + previewLinks: false, + + // Transition style (none/fade/slide/convex/concave/zoom) + transition: 'slide', + + // Transition speed (default/fast/slow) + transitionSpeed: 'default', + + // Transition style for full page slide backgrounds + // (none/fade/slide/convex/concave/zoom) + backgroundTransition: 'fade', + + // Number of slides away from the current that are visible + viewDistance: 3, + + // Number of slides away from the current that are visible on mobile + // devices. It is advisable to set this to a lower number than + // viewDistance in order to save resources. + mobileViewDistance: 2, + + // reveal.js plugins + plugins: [ + RevealNotes, + RevealSearch, + RevealZoom + ] + }); + </script> + </body> +</html> diff --git a/prolog/README.md b/prolog/README.md index d9d6ca0..2501090 100644 --- a/prolog/README.md +++ b/prolog/README.md @@ -1,16 +1,142 @@ -# Implementing Prolog +--- +title: Implementing Prolog +subtitle: A λ-Nantes Workshop +author: arnaud@pankzsoft.com - @abailly.bsky.social +date: 2025-12-10 +--- -## Basics +# Usage -* terms: - * variables start with upper casae: `X`, `Y`... - * symbols start with lower case: `s`, `z`, `child`, ... - * symbols have arity 0 or more : `bob`, `child(X, Y)`, `father(bob, Z)`... -* clauses: - * _head_: a single term - * _premises_: a (possibly empty) list of terms -* a _data set_ is a list of clauses -* _queries_ are + + +## Example + +A _program_ about Star Wars characters (including the crappy recent ones) + +## Example - Facts + +Simple facts asserting the gender of some characters. + +```prolog +female(leia). +male(vader). +male(luke). +male(kylo). +``` + +## Example - Facts + +More complex facts asserting a `child`hood _relation_ between some characters. + +```prolog +child(luke, vader). +child(leia, vader). +child(kylo, leia). +``` + +## Example - Rules + +_Rules_ (or _Clauses_) allowing to infer some relation from other relations. + +```prolog +son(X,Y) :- male(X), child(X,Y). +daughter(X,Y) :- female(X), child(X,Y). +``` + +## Example - Rules + +More complex rules asserting a transitive relation + +```prolog +grandchild(X,Z) :- child(X,Y), child(Y,Z). +``` + +## Example - Query + +We can _query_ this program, for example asking who is a grandchild of Darth Vader + +```prolog +> ?- grandchild(X, vader). +success. Type [Enter] to list solutions. +> +[X -> kylo] +``` + +## Example - Query + +A Prolog query can have several answers: + +```prolog +> ?- child(X, vader). +success. Type [Enter] to list solutions. +> +[X -> luke] +> +[X -> leia] +``` + +## Example - Query + +Or no answer: + +```prolog +> ?- grandchild(leia, X). +failure +``` + +# Implementation + +## Terms + +* variables start with upper casae: `X`, `Y`... +* symbols start with lower case: `s`, `z`, `child`, ... +* symbols have 0 or more arguments, e.g an _arity_ : `bob`, `child(X, Y)`, `father(bob, Z)`... + +## Clauses + +* _head_: a single term +* _premises_: a (possibly empty) list of terms +* a _data set_ (or a _program_) is a list of clauses or _facts_ +* a _query_ is a term introduced with `?-` + +## Basic algorithm + +Given a query and a set of clauses, a Prolog interpreter loop goes like: + +1. Push _query_ on its goal stack +2. Pop up current _goal_ from the stack +3. Try to match _goal_ with each _clause_: + a. _Unify_ goal with the _head_ of _clause_ with _fresh_ variables + b. If unification succeeds, push _premises_ of clause onto goals stack +4. Query succeeds if stack is empty with a successful match + +## Unification + +Given two terms $t_1$ and $t_2$ with _free variables_ $fv(t_1)$, $fv(t_2)$, +unification is the process of defining a _substitution_ between variables and _terms_ + +$$ +\sigma : fv(t_1) \cup fv(t_2) \rightarrow T +$$ + +## Unification + +* Two variables unify with each other +* A variable unifies with a term if not already mapped +* Two relations unify with each other iff + * Their symbol is the same + * Their arguments unify with each other + +## Unification + +* $\sigma(X, Y) = \{ X \mapsto Y \}$ +* $\sigma(X, foo) = \{ X \mapsto foo \}$ +* $\sigma(foo, X) = \{ X \mapsto foo \}$ +* $\sigma(foo(bar, Y), foo(X, Z)) = \{ X \mapsto bar, Y \mapsto Z \}$ + +# Practice + + ## References diff --git a/prolog/star-wars.jpg b/prolog/star-wars.jpg Binary files differnew file mode 100644 index 0000000..1b9561f --- /dev/null +++ b/prolog/star-wars.jpg diff --git a/prolog/workbench.jpg b/prolog/workbench.jpg Binary files differnew file mode 100644 index 0000000..f81de1a --- /dev/null +++ b/prolog/workbench.jpg |
