El camino a Prolog: obtener soluciones y no determinismo (parte II)
En el artículo anterior dejamos un algoritmo de unificación escrito en Rust. Ahora, y siguiendo también el libro de Peter Norvig, debemos implementar algo que pruebe las reglas que tenemos definidas para la query que insertemos.
Database
Lo primero que vamos a implementar es una base de datos donde almacenamos todos nuestros predicados. En esencia, la base de datos será un HashMap donde la clave es Predicate (nombre + aridad) y el contenido un listado de Clause. Cada Clause tiene que tener un Term como cabeza de la regla y opcionalmente un listado de Terms que serán la parte del cuerpo. Dentro de ese listado se tienen que cumplir todo, es decir, es un AND. Para implementar los OR, simplemente usaremos las N cláusulas.
Con este código podemos implementar una base de datos que permite añadir Clauses (y las almacena en el Predicate correcto), obtiene todas las Clauses de un Predicate y permite borrados.
use std::collections::HashMap;
use crate::term::Term;
#[derive(PartialEq, Debug)]
pub struct Clause {
pub head: Term,
pub body: Vec,
}
#[derive(PartialEq, Eq, Hash, Clone)]
pub struct Predicate {
pub name: String,
arity: usize,
}
impl Predicate {
pub fn from_clause(clause: &Clause) -> Option<Predicate> {
Self::from_term(&clause.head)
}
pub fn from_term(term: &Term) -> Option<Predicate> {
match term.clone() {
Term::Str(f, args) => Some(Predicate {
name: f.clone(),
arity: args.len(),
}),
Term::Atom(f) => Some(Predicate {
name: f.clone(),
arity: 0,
}),
_ => None
}
}
}
pub struct Database {
data: HashMap>
}
impl Database {
pub fn new() -> Self {
Database {
data: HashMap::new()
}
}
pub fn add_clause(&mut self, clause: Clause) {
if let Some(predicate_key) = Predicate::from_clause(&clause) {
{
self.data.entry(predicate_key.clone()).or_insert(Vec::new());
}
{
let predicate = self.data.get_mut(&predicate_key).unwrap();
predicate.push(clause);
}
}
}
pub fn get_clauses(&self, predicate: &Predicate) -> Option<&Vec<Clause>> {
self.data.get(predicate)
}
pub fn clear_all(&mut self) {
self.data = HashMap::new();
}
pub fn clear_predicate(&mut self, predicate: &Predicate) {
self.data.remove(predicate);
}
}
Ejecutar código
Vamos a añadir una función llamada prove que servirá para probar un Term. ¿Cómo se prueba un Term? Se obtiene el predicado al que hace referencia y sobre las cláusulas que tiene el predicado, probamos si alguna de las cabezas de esas cláusulas unifica con el Term. Eso nos dará unos bindings, parte de la solución. Si la cláusula que ha unificado no tiene términos en el cuerpo, no hay que hacer nada más, esa sería una solución que prueba Term. Pero si sí lo tiene, llamaremos a prove_all para probar la conjunción de los términos del cuerpo.
En esta primera versión analizamos todas las posibles ramas, es decir, si hay varias cláusulas que unifican, estas generarán dos bindings diferentes y a su vez, prove_all puede devolver N bindings.
fn prove(goal: Term, bindings: Bindings, database: &Database) -> Option<Vec<Bindings>> {
if let Some(predicate) = Predicate::from_term(&goal) {
if let Some(clauses) = database.get_clauses(&predicate) {
let mut solutions = Vec::new();
for clause in clauses {
let renamed_clause = rename_variables(&clause);
let bindings = unify(goal.clone(), renamed_clause.head, bindings.clone(), false);
if bindings.is_none() {
// do nothing
} else if renamed_clause.body.len() == 0 {
solutions.push(bindings);
} else {
if let Some(mut all_solutions) = prove_all(renamed_clause.body, vec![bindings], database) {
solutions.append(&mut all_solutions);
}
}
}
if solutions.len() == 0 {
None
} else {
Some(solutions)
}
} else {
None
}
} else {
None
}
}
Un paso que no hemos mencionado, pero es importante, es el renombrado de variables. Y es que un término y otro pueden tener los mismos nombres de variables, pero en este paso, deberían ser consideradas variables diferentes. La función rename_variables nos permite generar una Clause nueva con nombres de variables aleatorios (en este caso mediante UUID, aunque lo ideal es un contador sin más).
fn rename_variables(clause: &Clause) -> Clause {
let mut bindings = HashMap::new();
Clause {
head: rename_term(&clause.head, &mut bindings),
body: clause.body.iter().map(|term| rename_term(term, &mut bindings)).collect(),
}
}
fn rename_term(term: &Term, bindings: &mut HashMap<String, String>) -> Term {
match term {
Term::Atom(f) => Term::Atom(f.clone()),
Term::Var(var) => {
if let Some(subst) = bindings.get(var) {
Term::Var(subst.clone())
} else {
let id = Uuid::now_v1(&[1, 2, 3, 4, 5, 6]).to_string();
bindings.insert(var.clone(), id.clone());
Term::Var(id)
}
},
Term::Str(f, args) => {
Term::Str(f.clone(), args.iter().map(|arg| rename_term(arg, bindings)).collect())
}
}
}
¿Y como será prove_all? Sencillamente vamos term por term, intentando probarlo con un listado de bindings que tenemos en ese momento, así hasta que ya no queden terms por probar.
fn prove_all(mut goals: Vec<Term>, bindings: Vec<Bindings>, database: &Database) -> Option<Vec<Bindings>> {
if let Some(goal) = goals.pop() {
let mut solutions = Vec::new();
for binding in bindings {
if let Some(mut goal_solutions) = prove(goal.clone(), binding, database) {
solutions.append(&mut goal_solutions);
}
}
if solutions.len() == 0 {
None
} else {
prove_all(goals, solutions, database)
}
} else {
Some(bindings)
}
}
Con esto, dado una query (que será una conjunción de Term) llamaremos a prove_all y obtendremos todas las soluciones. No obstante no serán fáciles de leer ya que lo que vamos a devolver es un listado de sustituciones. Un sistema Prolog real, para facilitar la interpretación de las respuestas, da las soluciones en base al valor que deben adoptar las variables originales de la query, incluso resolviendo de forma recursiva las variables.
Así pues necesitamos dos funciones extra: find_variables_in_goals va a obtener un listado de las variables que aparecen en la query original y subst_bindings aplicará las sustituciones de forma recursiva.
fn subst_bindings(bindings: Bindings, term: Term) -> Term {
let bindings = bindings.expect("Only can be called when bindings are OK");
match term {
Term::Atom(x) => Term::Atom(x.clone()),
Term::Var(ref x) => {
if let Some(value) = bindings.get(x) {
subst_bindings(Some(bindings.clone()), value.clone())
} else {
Term::Var(x.clone())
}
}
Term::Str(f, args) => {
Term::Str(f.clone(), args.iter().map(|t| subst_bindings(Some(bindings.clone()), t.clone())).collect())
}
}
}
pub fn find_variables_in_goals(goals: &Vec<Term>) -> HashSet<String> {
let mut vars = HashSet::new();
for goal in goals {
match goal {
Term::Var(var) => {
vars.insert(var.clone());
},
Term::Atom(_) => (),
Term::Str(_, args) => vars.extend(find_variables_in_goals(&args))
}
}
vars
}
Una vez ya tenemos esto, podemos hacer una función top_level_prove que admita una query e imprima por pantalla los resultados.
fn top_level_prove(goals: Vec<Term>, database: &Database) {
let vars_in_goals = find_variables_in_goals(&goals);
let solutions = prove_all(goals, vec![Some(HashMap::new())], database);
if let Some(solutions) = solutions {
let mut output = Vec::new();
for solution in solutions {
let mut line = Vec::new();
for var in &vars_in_goals {
line.push(format!("{} = {}", var, subst_bindings(solution.clone(), Term::Var(var.clone()))));
}
output.push(line.join(","));
}
println!("{}", output.join(";\n"));
} else {
println!("false.")
}
}
Backtracking
Esto funciona pero Prolog no funciona así. Prolog no analiza todas las ramificaciones de query a no ser que se le pida expresamente. Por defecto, Prolog va a intentar solo una solución, hasta que no pueda seguir con ella. En ese caso, vuelve atrás y toma otro camino. Al llegar a una solución, se pregunta al usuario si quiere más soluciones o no.
Una forma se solucionarlo es 1) hacer que prove y prove_all solo devuelvan una solución, aunque se quedan en memoria al resto de posibilidades y 2) introducir en todas las queries un term especial al final (solo se llegará cuando el resto de goals ya han sido probados). Este term provocará una pregunta al usuario que dependiendo de su respuesta lo haremos que se pruebe (y acabaremos) o que no se pruebe y el sistema tenga que probar otras alternativas.
fn prove(goal: Term, bindings: Bindings, database: &Database, other_goals: VecDeque<Term>, vars_in_goals: &HashSet<String>) -> Bindings {
if let Some(predicate) = Predicate::from_term(&goal) {
if &predicate.name == "__backtracking?" {
let mut line = Vec::new();
for var in vars_in_goals {
line.push(format!("{} = {}", var, subst_bindings(bindings.clone(), Term::Var(var.clone()))));
}
if line.len() == 0 {
println!("true");
} else {
println!("{}", line.join(","));
}
if ask_confirm() {
None
} else {
bindings
}
} else {
if let Some(clauses) = database.get_clauses(&predicate) {
for clause in clauses {
let renamed_clause = rename_variables(&clause);
let bindings = unify(goal.clone(), renamed_clause.head, bindings.clone(), false);
if bindings.is_none() {
// do nothing
} else {
let mut goals = VecDeque::from(renamed_clause.body.clone());
goals.append(&mut other_goals.clone());
let new_bindings = prove_all(goals, bindings, database, vars_in_goals);
if new_bindings.is_some() {
return new_bindings;
}
}
}
None
} else {
None
}
}
} else {
None
}
}
pub fn prove_all(mut goals: VecDeque<Term>, bindings: Bindings, database: &Database, vars_in_goals: &HashSet<String>) -> Bindings {
if let Some(goal) = goals.pop_front() {
prove(goal, bindings, database, goals, vars_in_goals)
} else {
bindings
}
}
fn ask_confirm() -> bool {
let mut input = String::new();
std::io::stdin().read_line(&mut input).unwrap();
match input.chars().nth(0).unwrap() {
';' => return true,
_ => return false,
}
}
Con esto ya tendremos un sistema similar a Prolog. Pero nos ha faltado algo muy importante. ¡Leer la sintaxis! En el siguiente post veremos como leer la sintaxis simplificada de Prolog y como juntar todo. Además resolveremos el puzzle de la Zebra con nuestro nuevo sistema.