Finding algorithm to seek argument to satisfy given function's return

Question

I have this particular problem for which I don't have a solution yet. I think it would help if I know it exists a related algorithm.

The algorithm I'm looking for is one that helps find an argument that satisfies a goal returned by a function.

For example, a works for b is denoted as (a,b)

Given: [ (a,b); (b,c) ]

Function works will assure their relationship with boolean values

let works a b -> true
let works b c -> true

Now I'm given

[ (a, "x"); ("x", c) ]

If I want these 2 bindings are true, then this function must be true

let works a "x" -> true
let works "x" c -> true

Now I'm trying to write a function/algorithm that helps me achieve such "x" = b

I was thinking of backtracking, but not yet know how to implement it. I would appreciate if anyone could offer me a hint.

As a side note, I'm implementing the algorithm in F# with functional programming paradigm.

Answer 1

You are correct that you need backward chaining and Jack is correct that you need Unification, but specifically you need syntactic unification with backward chaining.

Your question is not new but has been more thoroughly answered on CS:StackExchange as How to implement a prolog interpreter in a purely functional language?

While this will put you on the right path, depending on the problems you want to solve, you may find that this may not be as easy as it seems.

EDIT

I tested your example on some working F# code I have and it does work, however I can not release the code to the public, sorry.

For your given example, it can be done with just unification without backward chaining.

You will need to create facts for

works(a,b).
works(b,c).

and a query

works(a,X),works(X,c).

with the answer being

X = b

If you want to extend this for more than one person in the middle, then you will need to use backward chaining because you will have to create a recursive subordinate rule.

You will need to create facts for

works(a,b).
works(b,c).
works(c,d).

and rules

subordinate(X,Z) :- works(X,Z).
subordinate(X,Z) :- works(X,Y), subordinate(Y,Z).

and a query

subordinate(a,X),subordinate(X,d).

with the answer being

X = b,c

You will have to create the types, unification and backward chaining algorithm. You may choose to create a parser and pretty printer and layer on a REPL, but it is not needed.

The facts, rules, and queries are show in human terms, but if you skip the parser and pretty printer you will have to code them up as an AST. i.e.

("works", [Const "a", Const "b"]) 

The uppercase letters represent Prolog variables. i.e. X Y Z
The lowercase letters represent Prolog constants. i.e. a b c

Your works problem is just a variation of the classic ancestor example. See: Prolog/Recursive Rules

Answer 2

The algorithm you're describing is Unification -- it's the basis of Prolog, and it's not terribly difficult to implement in F#.

I'd recommend reading the Handbook of Practical Logic and Automated Reasoning (Amazon, Safari Books) by John Harrison; section 3.9 covers the unification algorithm. Two other F#'ers and I ported the code from the book to F# last year if you want to have a look: fsharp-logic-examples.

Given your description of the problem, you could probably solve it with some simple Constraint Logic Programming (CLP), but AFAIK no one's implemented a CLP library for F# yet. miniKanren and cKanren are two popular, simple examples of such systems, and I doubt they'd take much time to port to F# if you were interested in doing so.