fluidB
/
fluidb
1
0
Fork 0
Code Pull Requests Activity
You cannot select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
main
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '50d7410fa1'
${ noResults }
fluidb/tutorial/1-acrobatics.ipynb

2197 lines
72 KiB
Plaintext
Raw Blame History Unescape Escape

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Air-data acrobatics"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [],
"source": [
"%reload_ext pycozo.ipyext_direct"
]
},
{
"cell_type": "markdown",
"metadata": {
"tags": []
},
"source": [
"## Hello, world!"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Let's start exploring the Cozo database by following the \"hello world\" tradition:"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 1 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_f3564_row0_col0, #T_f3564_row0_col1, #T_f3564_row0_col2 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_f3564\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_f3564_level0_col0\" class=\"col_heading level0 col0\" >a</th>\n",
" <th id=\"T_f3564_level0_col1\" class=\"col_heading level0 col1\" >b</th>\n",
" <th id=\"T_f3564_level0_col2\" class=\"col_heading level0 col2\" >c</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_f3564_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_f3564_row0_col0\" class=\"data row0 col0\" >hello</td>\n",
" <td id=\"T_f3564_row0_col1\" class=\"data row0 col1\" >world</td>\n",
" <td id=\"T_f3564_row0_col2\" class=\"data row0 col2\" >Cozo!</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x10338c280>"
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"?[a, b, c] <- [['hello', 'world', 'Cozo!']]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Let's break that down. This query consists of two parts, the part before `<-` is called its _head_, and the part after is called its _body_. The symbol `<-` itself denotes that this is a _constant rule_, or a declaration of _facts_.\n",
"\n",
"The head has the special name `?`, indicating the _entry_ of the query, which has three _arguments_ `a`, `b`, and `c`.\n",
"\n",
"The body consists of a list of lists (in this case a list of a single inner list). Each inner list represents a _tuple_, which is similar to a row in a relational database. The length of the inner list must match the number of arguments of the head, and each argument is then _bound_ to the corresponding value in the inner list by position.\n",
"\n",
"Of course more than one inner list is allowed:"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_625f4_row0_col0, #T_625f4_row0_col1, #T_625f4_row0_col2, #T_625f4_row1_col0, #T_625f4_row1_col1, #T_625f4_row1_col2 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_625f4\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_625f4_level0_col0\" class=\"col_heading level0 col0\" >a</th>\n",
" <th id=\"T_625f4_level0_col1\" class=\"col_heading level0 col1\" >b</th>\n",
" <th id=\"T_625f4_level0_col2\" class=\"col_heading level0 col2\" >c</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_625f4_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_625f4_row0_col0\" class=\"data row0 col0\" >hello</td>\n",
" <td id=\"T_625f4_row0_col1\" class=\"data row0 col1\" >world</td>\n",
" <td id=\"T_625f4_row0_col2\" class=\"data row0 col2\" >Cozo!</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_625f4_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_625f4_row1_col0\" class=\"data row1 col0\" >hello</td>\n",
" <td id=\"T_625f4_row1_col1\" class=\"data row1 col1\" >world</td>\n",
" <td id=\"T_625f4_row1_col2\" class=\"data row1 col2\" >database!</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x10338fdf0>"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"?[a, b, c] <- [['hello', 'world', 'Cozo!'],\n",
" ['hello', 'world', 'database!']]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Let's try the following:"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_2d238_row0_col0, #T_2d238_row1_col0, #T_2d238_row2_col0 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_2d238\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_2d238_level0_col0\" class=\"col_heading level0 col0\" >a</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_2d238_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_2d238_row0_col0\" class=\"data row0 col0\" >Cozo!</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_2d238_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_2d238_row1_col0\" class=\"data row1 col0\" >hello</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_2d238_level0_row2\" class=\"row_heading level0 row2\" >2</th>\n",
" <td id=\"T_2d238_row2_col0\" class=\"data row2 col0\" >world</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x110b44730>"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"?[a] <- [['hello'], ['world'], ['Cozo!']]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now we have three inner lists of length 1 each. The returned results is also _sorted_: all relations in Cozo are sorted lexicographically by position.\n",
"\n",
"Cozo operates on _set semantics_ instead of _bag semantics_: observe"
]
},
{
"cell_type": "code",
"execution_count": 6,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_79f6a_row0_col0, #T_79f6a_row1_col0, #T_79f6a_row2_col0, #T_79f6a_row3_col0 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_79f6a\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_79f6a_level0_col0\" class=\"col_heading level0 col0\" >a</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_79f6a_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_79f6a_row0_col0\" class=\"data row0 col0\" >Cozo!</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_79f6a_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_79f6a_row1_col0\" class=\"data row1 col0\" >Cozo.</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_79f6a_level0_row2\" class=\"row_heading level0 row2\" >2</th>\n",
" <td id=\"T_79f6a_row2_col0\" class=\"data row2 col0\" >hello</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_79f6a_level0_row3\" class=\"row_heading level0 row3\" >3</th>\n",
" <td id=\"T_79f6a_row3_col0\" class=\"data row3 col0\" >world</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x10338feb0>"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"?[a] <- [['hello'], ['world'], ['Cozo!'], ['hello'], ['world'], ['Cozo.']]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"`'hello'` and `'world'` both appear only once in the result, even though they appear twice each in the input. Set semantics automatically de-duplicates based on the whole tuple."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Values and expressions"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The list of lists in the body of the rules certainly look familiar to anyone who have used languages such as JavaScript or Python. In fact, with the exception of the map `{}`, valid JSON values represent valid Cozo values.\n",
"\n",
"As sorting is important in Cozo, study the following example, which demonstrates how different values are sorted:"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_29547_row0_col0, #T_29547_row10_col0 {\n",
" color: #bf5b3d;\n",
"}\n",
"#T_29547_row1_col0, #T_29547_row2_col0, #T_29547_row3_col0, #T_29547_row4_col0, #T_29547_row5_col0, #T_29547_row6_col0 {\n",
" color: #307fc1;\n",
"}\n",
"#T_29547_row7_col0, #T_29547_row8_col0, #T_29547_row9_col0 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_29547\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_29547_level0_col0\" class=\"col_heading level0 col0\" >a</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_29547_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_29547_row0_col0\" class=\"data row0 col0\" >None</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_29547_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_29547_row1_col0\" class=\"data row1 col0\" >False</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_29547_level0_row2\" class=\"row_heading level0 row2\" >2</th>\n",
" <td id=\"T_29547_row2_col0\" class=\"data row2 col0\" >True</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_29547_level0_row3\" class=\"row_heading level0 row3\" >3</th>\n",
" <td id=\"T_29547_row3_col0\" class=\"data row3 col0\" >-0.000000</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_29547_level0_row4\" class=\"row_heading level0 row4\" >4</th>\n",
" <td id=\"T_29547_row4_col0\" class=\"data row4 col0\" >1.000000</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_29547_level0_row5\" class=\"row_heading level0 row5\" >5</th>\n",
" <td id=\"T_29547_row5_col0\" class=\"data row5 col0\" >3.141590</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_29547_level0_row6\" class=\"row_heading level0 row6\" >6</th>\n",
" <td id=\"T_29547_row6_col0\" class=\"data row6 col0\" >1234567</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_29547_level0_row7\" class=\"row_heading level0 row7\" >7</th>\n",
" <td id=\"T_29547_row7_col0\" class=\"data row7 col0\" >A</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_29547_level0_row8\" class=\"row_heading level0 row8\" >8</th>\n",
" <td id=\"T_29547_row8_col0\" class=\"data row8 col0\" >Apple juice</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_29547_level0_row9\" class=\"row_heading level0 row9\" >9</th>\n",
" <td id=\"T_29547_row9_col0\" class=\"data row9 col0\" >apple</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_29547_level0_row10\" class=\"row_heading level0 row10\" >10</th>\n",
" <td id=\"T_29547_row10_col0\" class=\"data row10 col0\" >['apple', 1, [2, 3]]</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x10338c910>"
]
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"?[a] <- [[true],\n",
" [false], \n",
" [null],\n",
" [\"A\"], \n",
" ['apple'], # single or double quotes are both OK \n",
" [\"Apple juice\"], \n",
" [['apple', 1, [2, 3]]], # this row consists of a list consisting of heterogeneous items!\n",
" [1.0], \n",
" [1_234_567], # you can separate digits with underscores for clarity\n",
" [3.14159], \n",
" [-8e-99]]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Notice how comments are entered, just like in JavaScript. `/* ... */` also works.\n",
"\n",
"Even though the kind of rule we have been using is called the _constant rule_, you can in fact compute in them:"
]
},
{
"cell_type": "code",
"execution_count": 8,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_0c01c_row0_col0, #T_0c01c_row0_col1, #T_0c01c_row1_col0, #T_0c01c_row1_col1, #T_0c01c_row2_col0, #T_0c01c_row2_col1, #T_0c01c_row3_col0, #T_0c01c_row3_col1, #T_0c01c_row4_col0, #T_0c01c_row5_col0, #T_0c01c_row5_col1 {\n",
" color: #307fc1;\n",
"}\n",
"#T_0c01c_row4_col1 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_0c01c\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_0c01c_level0_col0\" class=\"col_heading level0 col0\" >i</th>\n",
" <th id=\"T_0c01c_level0_col1\" class=\"col_heading level0 col1\" >a</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_0c01c_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_0c01c_row0_col0\" class=\"data row0 col0\" >1</td>\n",
" <td id=\"T_0c01c_row0_col1\" class=\"data row0 col1\" >3</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_0c01c_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_0c01c_row1_col0\" class=\"data row1 col0\" >2</td>\n",
" <td id=\"T_0c01c_row1_col1\" class=\"data row1 col1\" >12</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_0c01c_level0_row2\" class=\"row_heading level0 row2\" >2</th>\n",
" <td id=\"T_0c01c_row2_col0\" class=\"data row2 col0\" >3</td>\n",
" <td id=\"T_0c01c_row2_col1\" class=\"data row2 col1\" >0.833333</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_0c01c_level0_row3\" class=\"row_heading level0 row3\" >3</th>\n",
" <td id=\"T_0c01c_row3_col0\" class=\"data row3 col0\" >4</td>\n",
" <td id=\"T_0c01c_row3_col1\" class=\"data row3 col1\" >1096.633158</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_0c01c_level0_row4\" class=\"row_heading level0 row4\" >4</th>\n",
" <td id=\"T_0c01c_row4_col0\" class=\"data row4 col0\" >5</td>\n",
" <td id=\"T_0c01c_row4_col1\" class=\"data row4 col1\" >NUMBER 10</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_0c01c_level0_row5\" class=\"row_heading level0 row5\" >5</th>\n",
" <td id=\"T_0c01c_row5_col0\" class=\"data row5 col0\" >6</td>\n",
" <td id=\"T_0c01c_row5_col1\" class=\"data row5 col1\" >3.141593</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x110b447c0>"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"?[i, a] <- [[1, 1 + 2], \n",
" [2, 3 * 4], \n",
" [3, 5 / 6], \n",
" [4, exp(7)], \n",
" [5, uppercase('number ') ++ to_string(10)], # string concatenation\n",
" [6, to_float('PI')]]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"for clarity we have used the index `i` to force the result to show in this order.\n",
"\n",
"For the full list of functions you can use in expressions, consult the Manual."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"There is one thing we need to make clear at this point. In CozoScript, only `true` is true, and only `false` is false. This is not a tautology: every other value, including `null`, produces error when put in a position requiring a truthy value. In this sense, `null` in CosoScript is only a _marker_. It has no inherent logical semantics associated with it, unlike `NULL` in SQL, `null` and `undefeined` in Javascript, and `None` in Python. An example:"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"\u001b[31meval::throw\u001b[0m\n",
"\n",
" \u001b[31m×\u001b[0m Evaluation of expression failed\n",
" ╭────\n",
" \u001b[2m1\u001b[0m │ ?[a] <- [[!null]]\n",
" · \u001b[35;1m ─────\u001b[0m\n",
" ╰────\n",
"\u001b[36m help: \u001b[0m'negate' requires booleans\n"
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"?[a] <- [[!null]]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In this case you really need to write"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_607dd_row0_col0 {\n",
" color: #307fc1;\n",
"}\n",
"</style>\n",
"<table id=\"T_607dd\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_607dd_level0_col0\" class=\"col_heading level0 col0\" >a</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_607dd_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_607dd_row0_col0\" class=\"data row0 col0\" >False</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x116f07af0>"
]
},
"execution_count": 10,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"?[a] <- [[!is_null(null)]]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"This may seem a nuisance in trivial cases, but will save you a lot of hair in hairy situations. Believe me."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Horn-clause rules"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Usually constant rules are used to define ad-hoc facts useful for subsequent queries:"
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_c721a_row0_col0, #T_c721a_row0_col1, #T_c721a_row1_col0, #T_c721a_row1_col1, #T_c721a_row2_col0, #T_c721a_row2_col1, #T_c721a_row3_col0, #T_c721a_row3_col1, #T_c721a_row4_col0, #T_c721a_row4_col1, #T_c721a_row5_col0, #T_c721a_row5_col1, #T_c721a_row6_col0, #T_c721a_row6_col1, #T_c721a_row7_col0, #T_c721a_row7_col1 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_c721a\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_c721a_level0_col0\" class=\"col_heading level0 col0\" >loving</th>\n",
" <th id=\"T_c721a_level0_col1\" class=\"col_heading level0 col1\" >loved</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_c721a_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_c721a_row0_col0\" class=\"data row0 col0\" >alice</td>\n",
" <td id=\"T_c721a_row0_col1\" class=\"data row0 col1\" >eve</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_c721a_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_c721a_row1_col0\" class=\"data row1 col0\" >bob</td>\n",
" <td id=\"T_c721a_row1_col1\" class=\"data row1 col1\" >alice</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_c721a_level0_row2\" class=\"row_heading level0 row2\" >2</th>\n",
" <td id=\"T_c721a_row2_col0\" class=\"data row2 col0\" >charlie</td>\n",
" <td id=\"T_c721a_row2_col1\" class=\"data row2 col1\" >eve</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_c721a_level0_row3\" class=\"row_heading level0 row3\" >3</th>\n",
" <td id=\"T_c721a_row3_col0\" class=\"data row3 col0\" >david</td>\n",
" <td id=\"T_c721a_row3_col1\" class=\"data row3 col1\" >george</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_c721a_level0_row4\" class=\"row_heading level0 row4\" >4</th>\n",
" <td id=\"T_c721a_row4_col0\" class=\"data row4 col0\" >eve</td>\n",
" <td id=\"T_c721a_row4_col1\" class=\"data row4 col1\" >alice</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_c721a_level0_row5\" class=\"row_heading level0 row5\" >5</th>\n",
" <td id=\"T_c721a_row5_col0\" class=\"data row5 col0\" >eve</td>\n",
" <td id=\"T_c721a_row5_col1\" class=\"data row5 col1\" >bob</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_c721a_level0_row6\" class=\"row_heading level0 row6\" >6</th>\n",
" <td id=\"T_c721a_row6_col0\" class=\"data row6 col0\" >eve</td>\n",
" <td id=\"T_c721a_row6_col1\" class=\"data row6 col1\" >charlie</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_c721a_level0_row7\" class=\"row_heading level0 row7\" >7</th>\n",
" <td id=\"T_c721a_row7_col0\" class=\"data row7 col0\" >george</td>\n",
" <td id=\"T_c721a_row7_col1\" class=\"data row7 col1\" >george</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x10338c190>"
]
},
"execution_count": 11,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"?[loving, loved] := loves[loving, loved] # Yes, this is the 'subsequent query'. In a logical sense. \n",
" # The order of rules has no significance whatsoever.\n",
"\n",
"loves[] <- [['alice', 'eve'],\n",
" ['bob', 'alice'],\n",
" ['eve', 'alice'],\n",
" ['eve', 'bob'],\n",
" ['eve', 'charlie'],\n",
" ['charlie', 'eve'],\n",
" ['david', 'george'],\n",
" ['george', 'george']]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The constant rule is now named `loves`, denoting a rather complicated relationship network (aren't 'relationship' and 'network' synonyms?). It reads like \"Alice loves Eve, Bob loves Alice\", \"nobody loves David, David loves George, but George only loves himself\", and so on. Note that for constant rules we can actually omit the arguments (but if explicitly given, the arity must match the actual data).\n",
"\n",
"The entry `?` is now a _Horn-clause rule_, signified by the symbol `:=`. Its body has a single _application_ of the rule we have just defined, with _bindings_ `loving` and `loved` for the arguments. These bindings are then carried to the output via the arguments of the entry rule.\n",
"\n",
"Here both bindings to the rule application of `loves` are initially _unbound_, in which case all tuples of `loves` are returned. To _bind_ an argument simply pass a constant in:"
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_3f63d_row0_col0, #T_3f63d_row1_col0, #T_3f63d_row2_col0 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_3f63d\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_3f63d_level0_col0\" class=\"col_heading level0 col0\" >loved_by_eve</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_3f63d_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_3f63d_row0_col0\" class=\"data row0 col0\" >alice</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_3f63d_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_3f63d_row1_col0\" class=\"data row1 col0\" >bob</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_3f63d_level0_row2\" class=\"row_heading level0 row2\" >2</th>\n",
" <td id=\"T_3f63d_row2_col0\" class=\"data row2 col0\" >charlie</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x116f048b0>"
]
},
"execution_count": 12,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"loves[] <- [['alice', 'eve'],\n",
" ['bob', 'alice'],\n",
" ['eve', 'alice'],\n",
" ['eve', 'bob'],\n",
" ['eve', 'charlie'],\n",
" ['charlie', 'eve'],\n",
" ['david', 'george'],\n",
" ['george', 'george']]\n",
"\n",
"?[loved_by_eve] := loves['e' ++ 'v' ++ 'e', loved_by_eve] # Eve loves dramatic entrance"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Every argument position can be bound:"
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_588de_row0_col0, #T_588de_row1_col0 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_588de\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_588de_level0_col0\" class=\"col_heading level0 col0\" >loves_eve</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_588de_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_588de_row0_col0\" class=\"data row0 col0\" >alice</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_588de_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_588de_row1_col0\" class=\"data row1 col0\" >charlie</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x116f07f40>"
]
},
"execution_count": 13,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"loves[] <- [['alice', 'eve'],\n",
" ['bob', 'alice'],\n",
" ['eve', 'alice'],\n",
" ['eve', 'bob'],\n",
" ['eve', 'charlie'],\n",
" ['charlie', 'eve'],\n",
" ['david', 'george'],\n",
" ['george', 'george']]\n",
"\n",
"?[loves_eve] := loves[loves_eve, 'eve']"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Multiple clauses can appear in the body, in which case an implicit conjunction is implied, meaning that all clauses\n",
"must bind for a result to return:"
]
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_e24ea_row0_col0 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_e24ea\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_e24ea_level0_col0\" class=\"col_heading level0 col0\" >loved_by_b_e</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_e24ea_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_e24ea_row0_col0\" class=\"data row0 col0\" >alice</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x110b447f0>"
]
},
"execution_count": 14,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"loves[] <- [['alice', 'eve'],\n",
" ['bob', 'alice'],\n",
" ['eve', 'alice'],\n",
" ['eve', 'bob'],\n",
" ['eve', 'charlie'],\n",
" ['charlie', 'eve'],\n",
" ['david', 'george'],\n",
" ['george', 'george']]\n",
"\n",
"?[loved_by_b_e] := loves['eve', loved_by_b_e], loves['bob', loved_by_b_e]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We see that Alice is loved by both Bob and Eve. The variable `loved_by_b_e` appears in both clauses, in which case they are _unified_, meaning that they must bind to the _same_ value for a tuple to return."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Disjunction, meaning that _any_ clause with successful binding potentially contribute to results, must be specified explicitly:"
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_d09d6_row0_col0, #T_d09d6_row1_col0 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_d09d6\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_d09d6_level0_col0\" class=\"col_heading level0 col0\" >loved_by_b_e</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_d09d6_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_d09d6_row0_col0\" class=\"data row0 col0\" >alice</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_d09d6_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_d09d6_row1_col0\" class=\"data row1 col0\" >charlie</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x116f068c0>"
]
},
"execution_count": 15,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"loves[] <- [['alice', 'eve'],\n",
" ['bob', 'alice'],\n",
" ['eve', 'alice'],\n",
" ['eve', 'bob'],\n",
" ['eve', 'charlie'],\n",
" ['charlie', 'eve'],\n",
" ['david', 'george'],\n",
" ['george', 'george']]\n",
"\n",
"?[loved_by_b_e] := loves['eve', loved_by_b_e] or loves['bob', loved_by_b_e], \n",
" loved_by_b_e != 'bob', \n",
" loved_by_b_e != 'eve'"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"As we can see, disjunctive clauses are connected by `or`. It binds more strongly than the implicit conjunction `,`."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Horn clause rules (and Horn clause rules only) may have multiple definitions _having equivalent heads_. The above query is identical in every way to the following:"
]
},
{
"cell_type": "code",
"execution_count": 16,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_7a5cb_row0_col0, #T_7a5cb_row1_col0 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_7a5cb\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_7a5cb_level0_col0\" class=\"col_heading level0 col0\" >loved_by_b_e</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_7a5cb_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_7a5cb_row0_col0\" class=\"data row0 col0\" >alice</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_7a5cb_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_7a5cb_row1_col0\" class=\"data row1 col0\" >charlie</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x116f04e80>"
]
},
"execution_count": 16,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"loves[] <- [['alice', 'eve'],\n",
" ['bob', 'alice'],\n",
" ['eve', 'alice'],\n",
" ['eve', 'bob'],\n",
" ['eve', 'charlie'],\n",
" ['charlie', 'eve'],\n",
" ['david', 'george'],\n",
" ['george', 'george']]\n",
"\n",
"?[loved_by_b_e] := loves['eve', loved_by_b_e], loved_by_b_e != 'bob', loved_by_b_e != 'eve'\n",
"?[loved_by_b_e] := loves['bob', loved_by_b_e], loved_by_b_e != 'bob', loved_by_b_e != 'eve'"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"If a Horn clause rule is not the entry, even the _names_ given to the arguments can differ. The bodies are not required to be of the same form, as long as they produce compatible outputs."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Besides rule applications, _filters_ can also appear in the body:"
]
},
{
"cell_type": "code",
"execution_count": 17,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_072ec_row0_col0, #T_072ec_row0_col1, #T_072ec_row1_col0, #T_072ec_row1_col1 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_072ec\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_072ec_level0_col0\" class=\"col_heading level0 col0\" >person</th>\n",
" <th id=\"T_072ec_level0_col1\" class=\"col_heading level0 col1\" >loved</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_072ec_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_072ec_row0_col0\" class=\"data row0 col0\" >bob</td>\n",
" <td id=\"T_072ec_row0_col1\" class=\"data row0 col1\" >alice</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_072ec_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_072ec_row1_col0\" class=\"data row1 col0\" >david</td>\n",
" <td id=\"T_072ec_row1_col1\" class=\"data row1 col1\" >george</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x116f071c0>"
]
},
"execution_count": 17,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"loves[] <- [['alice', 'eve'],\n",
" ['bob', 'alice'],\n",
" ['eve', 'alice'],\n",
" ['eve', 'bob'],\n",
" ['eve', 'charlie'],\n",
" ['charlie', 'eve'],\n",
" ['david', 'george'],\n",
" ['george', 'george']]\n",
"\n",
"?[person, loved] := loves[person, loved], !ends_with(person, 'e')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In this case only people with name not ending in `'e'` are considered for the loving position.\n",
"\n",
"By the way, if you are not interested in who the person in the loving position is, you can just omit it in the arguments to the entry:"
]
},
{
"cell_type": "code",
"execution_count": 18,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_00d9f_row0_col0, #T_00d9f_row1_col0 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_00d9f\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_00d9f_level0_col0\" class=\"col_heading level0 col0\" >loved</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_00d9f_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_00d9f_row0_col0\" class=\"data row0 col0\" >alice</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_00d9f_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_00d9f_row1_col0\" class=\"data row1 col0\" >george</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x116f074f0>"
]
},
"execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"loves[] <- [['alice', 'eve'],\n",
" ['bob', 'alice'],\n",
" ['eve', 'alice'],\n",
" ['eve', 'bob'],\n",
" ['eve', 'charlie'],\n",
" ['charlie', 'eve'],\n",
" ['david', 'george'],\n",
" ['george', 'george']]\n",
"\n",
"?[loved] := loves[person, loved], !ends_with(person, 'e')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"... but every argument in the head of any Horn-clause rule must appear in the body, of course:"
]
},
{
"cell_type": "code",
"execution_count": 19,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"\u001b[31meval::unbound_symb_in_head\u001b[0m\n",
"\n",
" \u001b[31m×\u001b[0m Symbol 'the_alien' in rule head is unbound\n",
" ╭─[9:1]\n",
" \u001b[2m 9\u001b[0m │ \n",
" \u001b[2m10\u001b[0m │ ?[the_alien, loved] := loves[person, loved], !ends_with(person, 'e')\n",
" · \u001b[35;1m ─────────\u001b[0m\n",
" ╰────\n",
"\u001b[36m help: \u001b[0mNote that symbols occurring only in negated positions are not considered bound\n"
]
},
"execution_count": 19,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"loves[] <- [['alice', 'eve'],\n",
" ['bob', 'alice'],\n",
" ['eve', 'alice'],\n",
" ['eve', 'bob'],\n",
" ['eve', 'charlie'],\n",
" ['charlie', 'eve'],\n",
" ['david', 'george'],\n",
" ['george', 'george']]\n",
"\n",
"?[the_alien, loved] := loves[person, loved], !ends_with(person, 'e')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Negation"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The next query finds those who are loved by Eve, but not by Bob:"
]
},
{
"cell_type": "code",
"execution_count": 20,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_9049a_row0_col0, #T_9049a_row1_col0 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_9049a\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_9049a_level0_col0\" class=\"col_heading level0 col0\" >loved_by_e_not_b</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_9049a_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_9049a_row0_col0\" class=\"data row0 col0\" >bob</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_9049a_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_9049a_row1_col0\" class=\"data row1 col0\" >charlie</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x116f052a0>"
]
},
"execution_count": 20,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"loves[] <- [['alice', 'eve'],\n",
" ['bob', 'alice'],\n",
" ['eve', 'alice'],\n",
" ['eve', 'bob'],\n",
" ['eve', 'charlie'],\n",
" ['charlie', 'eve'],\n",
" ['david', 'george'],\n",
" ['george', 'george']]\n",
"\n",
"?[loved_by_e_not_b] := loves['eve', loved_by_e_not_b], not loves['bob', loved_by_e_not_b]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Here we are using the `not` keyword to _negate_ the rule application `loves`. This negation is at the level of Horn-clauses, which is not the same as the level of expressions. In fact, there are two sets of related but inequivalent operators:\n",
"\n",
"* For Horn clauses: `,` (conjunction), `or` (disjunction), `not` (negation)\n",
"* For boolean expressions: `&&` (conjunction), `||` (disjunction), `!` (negation)\n",
"\n",
"Hopefully you are already familiar with the boolean set of operators. If you use them in the wrong way, the query compiler will yell at you. And you will comply."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Negation has to abide by the _safety rule_. Let's violate it:"
]
},
{
"cell_type": "code",
"execution_count": 21,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"\u001b[31meval::unbound_symb_in_head\u001b[0m\n",
"\n",
" \u001b[31m×\u001b[0m Symbol 'not_loved_by_b' in rule head is unbound\n",
" ╭─[9:1]\n",
" \u001b[2m 9\u001b[0m │ \n",
" \u001b[2m10\u001b[0m │ ?[not_loved_by_b] := not loves['bob', not_loved_by_b]\n",
" · \u001b[35;1m ──────────────\u001b[0m\n",
" ╰────\n",
"\u001b[36m help: \u001b[0mNote that symbols occurring only in negated positions are not considered bound\n"
]
},
"execution_count": 21,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"loves[] <- [['alice', 'eve'],\n",
" ['bob', 'alice'],\n",
" ['eve', 'alice'],\n",
" ['eve', 'bob'],\n",
" ['eve', 'charlie'],\n",
" ['charlie', 'eve'],\n",
" ['david', 'george'],\n",
" ['george', 'george']]\n",
"\n",
"?[not_loved_by_b] := not loves['bob', not_loved_by_b]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Oh no! The query compiler rejects our perfectly reasonable query trying to determine those poor souls not loved by Bob!\n",
"\n",
"But is our query really reasonable? For example, should the query return a tuple containing 'gold', since according to facts at hand, Bob clearly has no interest in 'gold'? So should our query return every possible string except a select few? Do you want your computer to handle such a query?\n",
"\n",
"Now you understand what the help message above is trying to tell you."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"To make our query really reasonable, we have to explicitly give our query a _closed world_ in which to operate the negation:"
]
},
{
"cell_type": "code",
"execution_count": 22,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_4f125_row0_col0, #T_4f125_row1_col0, #T_4f125_row2_col0, #T_4f125_row3_col0, #T_4f125_row4_col0 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_4f125\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_4f125_level0_col0\" class=\"col_heading level0 col0\" >not_loved_by_b</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_4f125_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_4f125_row0_col0\" class=\"data row0 col0\" >bob</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_4f125_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_4f125_row1_col0\" class=\"data row1 col0\" >charlie</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_4f125_level0_row2\" class=\"row_heading level0 row2\" >2</th>\n",
" <td id=\"T_4f125_row2_col0\" class=\"data row2 col0\" >david</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_4f125_level0_row3\" class=\"row_heading level0 row3\" >3</th>\n",
" <td id=\"T_4f125_row3_col0\" class=\"data row3 col0\" >eve</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_4f125_level0_row4\" class=\"row_heading level0 row4\" >4</th>\n",
" <td id=\"T_4f125_row4_col0\" class=\"data row4 col0\" >george</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x116f05f60>"
]
},
"execution_count": 22,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"loves[] <- [['alice', 'eve'],\n",
" ['bob', 'alice'],\n",
" ['eve', 'alice'],\n",
" ['eve', 'bob'],\n",
" ['eve', 'charlie'],\n",
" ['charlie', 'eve'],\n",
" ['david', 'george'],\n",
" ['george', 'george']]\n",
" \n",
"the_population[p] := loves[p, _a]\n",
"the_population[p] := loves[_a, p]\n",
"\n",
"?[not_loved_by_b] := the_population[not_loved_by_b], not loves['bob', not_loved_by_b]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now the query understands that we are asking our question _within_ the people in the love network. It then proceeds without complaints.\n",
"\n",
"Let's state the **safety rule for negation**: _at least one_ argument of the rule application must be bound elsewhere (otherwise the clause will produce an infinity of candidate tuples), and _all arguments_ to negated clauses are _not_ considered bound, _unless_ they also appear elsewhere in a positive context.\n",
"\n",
"If you can't wrap your head around the rule yet, don't worry. Just write your query. Return here and reread this section when you encounter some error messages similar to the above."
]
},
{
"cell_type": "markdown",
"metadata": {
"tags": []
},
"source": [
"## Unification"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We have seen that variables with repeated appearance in rule applications and predicates are implicitly unified. You can also _explicitly_ unify a variable with the unify operator `=`:"
]
},
{
"cell_type": "code",
"execution_count": 23,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_2ec77_row0_col0, #T_2ec77_row1_col0 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_2ec77\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_2ec77_level0_col0\" class=\"col_heading level0 col0\" >loves_eve</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_2ec77_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_2ec77_row0_col0\" class=\"data row0 col0\" >alice</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_2ec77_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_2ec77_row1_col0\" class=\"data row1 col0\" >charlie</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x116f06920>"
]
},
"execution_count": 23,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"loves[] <- [['alice', 'eve'],\n",
" ['bob', 'alice'],\n",
" ['eve', 'alice'],\n",
" ['eve', 'bob'],\n",
" ['eve', 'charlie'],\n",
" ['charlie', 'eve'],\n",
" ['david', 'george'],\n",
" ['george', 'george']]\n",
"\n",
"?[loves_eve] := eve = 'eve', loves[loves_eve, eve]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"By the way, the _order_ a clause appears in a Horn-clause rule can never affect the result in any way (provided your queries do not contain random functions):"
]
},
{
"cell_type": "code",
"execution_count": 24,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_979ad_row0_col0, #T_979ad_row1_col0 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_979ad\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_979ad_level0_col0\" class=\"col_heading level0 col0\" >loves_eve</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_979ad_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_979ad_row0_col0\" class=\"data row0 col0\" >alice</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_979ad_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_979ad_row1_col0\" class=\"data row1 col0\" >charlie</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x116f06c20>"
]
},
"execution_count": 24,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"loves[] <- [['alice', 'eve'],\n",
" ['bob', 'alice'],\n",
" ['eve', 'alice'],\n",
" ['eve', 'bob'],\n",
" ['eve', 'charlie'],\n",
" ['charlie', 'eve'],\n",
" ['david', 'george'],\n",
" ['george', 'george']]\n",
"\n",
"?[loves_eve] := loves[loves_eve, eve], eve = 'eve'"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"... but the performance might vary, sometimes greatly. This is an advanced topic that we will come back to in a later session. For trivial examples like ours it doesn't matter. In your own explorations, just try to put more 'restrictive' rules first (meaning that they filter out a greater number of tuples), and you will be fine most of the time."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"There is also the spread-unify operator `in`, which unifies the left hand side with values in a list one at a time:"
]
},
{
"cell_type": "code",
"execution_count": 25,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_a532a_row0_col0, #T_a532a_row1_col0, #T_a532a_row2_col0 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_a532a\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_a532a_level0_col0\" class=\"col_heading level0 col0\" >u</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_a532a_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_a532a_row0_col0\" class=\"data row0 col0\" >a</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_a532a_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_a532a_row1_col0\" class=\"data row1 col0\" >b</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_a532a_level0_row2\" class=\"row_heading level0 row2\" >2</th>\n",
" <td id=\"T_a532a_row2_col0\" class=\"data row2 col0\" >c</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x110cb5ba0>"
]
},
"execution_count": 25,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"?[u] := u in ['a', 'b', 'c']"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Another example: this is the \"Cartesian product\""
]
},
{
"cell_type": "code",
"execution_count": 26,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_7aec9_row0_col0, #T_7aec9_row0_col1, #T_7aec9_row1_col0, #T_7aec9_row1_col1, #T_7aec9_row2_col0, #T_7aec9_row2_col1, #T_7aec9_row3_col0, #T_7aec9_row3_col1, #T_7aec9_row4_col0, #T_7aec9_row4_col1, #T_7aec9_row5_col0, #T_7aec9_row5_col1 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_7aec9\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_7aec9_level0_col0\" class=\"col_heading level0 col0\" >u</th>\n",
" <th id=\"T_7aec9_level0_col1\" class=\"col_heading level0 col1\" >v</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_7aec9_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_7aec9_row0_col0\" class=\"data row0 col0\" >a</td>\n",
" <td id=\"T_7aec9_row0_col1\" class=\"data row0 col1\" >x</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_7aec9_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_7aec9_row1_col0\" class=\"data row1 col0\" >a</td>\n",
" <td id=\"T_7aec9_row1_col1\" class=\"data row1 col1\" >y</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_7aec9_level0_row2\" class=\"row_heading level0 row2\" >2</th>\n",
" <td id=\"T_7aec9_row2_col0\" class=\"data row2 col0\" >b</td>\n",
" <td id=\"T_7aec9_row2_col1\" class=\"data row2 col1\" >x</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_7aec9_level0_row3\" class=\"row_heading level0 row3\" >3</th>\n",
" <td id=\"T_7aec9_row3_col0\" class=\"data row3 col0\" >b</td>\n",
" <td id=\"T_7aec9_row3_col1\" class=\"data row3 col1\" >y</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_7aec9_level0_row4\" class=\"row_heading level0 row4\" >4</th>\n",
" <td id=\"T_7aec9_row4_col0\" class=\"data row4 col0\" >c</td>\n",
" <td id=\"T_7aec9_row4_col1\" class=\"data row4 col1\" >x</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_7aec9_level0_row5\" class=\"row_heading level0 row5\" >5</th>\n",
" <td id=\"T_7aec9_row5_col0\" class=\"data row5 col0\" >c</td>\n",
" <td id=\"T_7aec9_row5_col1\" class=\"data row5 col1\" >y</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x110cb4eb0>"
]
},
"execution_count": 26,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"?[u, v] := u in ['a', 'b', 'c'], v in ['x', 'y']"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"You may notice that paired with functions extracting elements from lists, we don't actually need constant rules anymore. But constant rules are more explicit when you really have _facts_ as inputs."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Recursion"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now we come to the \"poster boy\" query of classical Datalog: let's find out all the people loved by Alice, or loved by someone loved by Alice, or loved by someone loved by someone loved by Alice, _ad infinitum_:"
]
},
{
"cell_type": "code",
"execution_count": 27,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"#T_5f393_row0_col0, #T_5f393_row1_col0, #T_5f393_row2_col0, #T_5f393_row3_col0 {\n",
" color: black;\n",
"}\n",
"</style>\n",
"<table id=\"T_5f393\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_5f393_level0_col0\" class=\"col_heading level0 col0\" >chained</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" <tr>\n",
" <th id=\"T_5f393_level0_row0\" class=\"row_heading level0 row0\" >0</th>\n",
" <td id=\"T_5f393_row0_col0\" class=\"data row0 col0\" >alice</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_5f393_level0_row1\" class=\"row_heading level0 row1\" >1</th>\n",
" <td id=\"T_5f393_row1_col0\" class=\"data row1 col0\" >bob</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_5f393_level0_row2\" class=\"row_heading level0 row2\" >2</th>\n",
" <td id=\"T_5f393_row2_col0\" class=\"data row2 col0\" >charlie</td>\n",
" </tr>\n",
" <tr>\n",
" <th id=\"T_5f393_level0_row3\" class=\"row_heading level0 row3\" >3</th>\n",
" <td id=\"T_5f393_row3_col0\" class=\"data row3 col0\" >eve</td>\n",
" </tr>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x110cb6710>"
]
},
"execution_count": 27,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"loves[] <- [['alice', 'eve'],\n",
" ['bob', 'alice'],\n",
" ['eve', 'alice'],\n",
" ['eve', 'bob'],\n",
" ['eve', 'charlie'],\n",
" ['charlie', 'eve'],\n",
" ['david', 'george'],\n",
" ['george', 'george']]\n",
"\n",
"alice_love_chain[person] := loves['alice', person]\n",
"alice_love_chain[person] := alice_love_chain[in_person], loves[in_person, person]\n",
"\n",
"?[chained] := alice_love_chain[chained]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Someone \"chained\" is either loved by Alice directly, or loved by someone already in the chain. The query as written reads very naturally. This is why this \"transitive closure\" type of query is the poster-boy query of classical Datalog. \n",
"\n",
"Writing the same thing in SQL requires recursive CTE, and those CTEs escalate pretty quickly. On the other hand, if well written, Datalog queries can weather very demanding situations and remain readable.\n",
"\n",
"Recursive queries are an essential part for graphs (networks). So they had better be easy to write _and_ read in a database claiming to be optimized for graphs."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We've talked about the safety rule for negation above. You may suspect that something similar is at play here. Let's retry the above query, but omit the starting condition `alice_love_chain[person] := loves['alice', person]`:"
]
},
{
"cell_type": "code",
"execution_count": 33,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"<p style=\"font-size: 75%\">Completed in 0 ms</p>"
],
"text/plain": [
"<IPython.core.display.HTML object>"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
"<style type=\"text/css\">\n",
"</style>\n",
"<table id=\"T_1e2e1\">\n",
" <thead>\n",
" <tr>\n",
" <th class=\"blank level0\" >&nbsp;</th>\n",
" <th id=\"T_1e2e1_level0_col0\" class=\"col_heading level0 col0\" >chained</th>\n",
" </tr>\n",
" </thead>\n",
" <tbody>\n",
" </tbody>\n",
"</table>\n"
],
"text/plain": [
"<pandas.io.formats.style.Styler at 0x110cb65f0>"
]
},
"execution_count": 33,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"loves[] <- [['alice', 'eve'],\n",
" ['bob', 'alice'],\n",
" ['eve', 'alice'],\n",
" ['eve', 'bob'],\n",
" ['eve', 'charlie'],\n",
" ['charlie', 'eve'],\n",
" ['david', 'george'],\n",
" ['george', 'george']]\n",
"\n",
"alice_love_chain[person] := alice_love_chain[in_person], loves[in_person, person]\n",
"\n",
"?[chained] := alice_love_chain[chained]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Are you surprised that the compiler did not complain? Are you surprised that it returned no results? This is the _closed-world assumption_ hinted above at play again. If there is no way to _deduce_ a fact from the given facts, _then_ the fact itself is false.\n",
"\n",
"This so called \"least fixed point\" semantics is the semantics of Datalog queries. This semantics is actually subtly different from SQL, due to the existence of `UNKNOWN` in SQL, usually manifesting as `NULL`. In other worlds, SQL operates on [ternary logic](https://en.wikipedia.org/wiki/Three-valued_logic) whereas Datalog stays boolean all the way (under the protection of the closed world assumptions)."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Still, there are _rules_ with respect to recursion. [Bertrand Russell](https://en.wikipedia.org/wiki/Russell%27s_paradox) would rush to write:"
]
},
{
"cell_type": "code",
"execution_count": 32,
"metadata": {},
"outputs": [
{
"data": {
"text/plain": [
"\u001b[31meval::unstratifiable\u001b[0m\n",
"\n",
" \u001b[31m×\u001b[0m Query is unstratifiable\n",
"\u001b[36m help: \u001b[0mThe rule 'q' is in the strongly connected component [\"p\", \"q\"],\n",
" and is involved in at least one forbidden dependency\n",
" (negation, non-meet aggregation, or algorithm-application).\n"
]
},
"execution_count": 32,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"world[a] := a in [1, 2]\n",
"\n",
"p[a] := world[a], not q[a]\n",
"q[a] := world[a], not p[a]\n",
"\n",
"?[a] := p[a]"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The above query does not violate the safety rule of negation (because he put a `world` in front of each negation), but the compiler still rejects it. Don't worry about the unworldly incantation the error makes. Instead, think for a moment what the result _could_ be."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"You can verify that the result could be the single tuple `[1]` with the assignment `p[a] <- [[1]]` and `q[a] <- [[2]]`, _or_ the single tuple `['q']` with the assignment `p[a] <- [[2]]` and `q[a] <- [[1]]`. The problem is, these answers contradict each other, and neither can be deduced _constructively_. So under the least fixed point semantics, this program has no _meaning_, and the compiler rejects it.\n",
"\n",
"Again, don't worry if you can't exactly follow what is going on. Just trust that the compiler is trying to prevent your computer from imploding. Real applications don't tend to produce these kinds of contrived, paradoxical queries anyway."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Conclusion"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"That's it! You have learned the basics of Datalog in the dialect CozoScript!\n",
"\n",
"If you want to play more without going further for the moment, it is recommended that you skim through the list of functions in the Manual. Those functions allow you to do much more acrobatics with pure Datalog."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3 (ipykernel)",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.10.6"
}
},
"nbformat": 4,
"nbformat_minor": 4
}
View Git Blame Copy Permalink