XSB Mister X - Revision history

John at 20:42, 1 March 2024

2024-03-01T20:42:01Z

← Older revision		Revision as of 20:42, 1 March 2024
Line 86:		Line 86:
	<pre class="prolog">integer_sqrt( N, Sqrt ) :-		<pre class="prolog">integer_sqrt( N, Sqrt ) :-
	Sqrt is floor(sqrt(N)).</pre>		Sqrt is floor(sqrt(N)).</pre>
			== Utility Predicates ==
	Load a small library of [[Puzzle Utilities]].		Load a small library of [[Puzzle Utilities]].

John: /* Tabling */

2024-03-01T20:17:50Z

Tabling

← Older revision		Revision as of 20:17, 1 March 2024
Line 92:		Line 92:
	== Result ==		== Result ==
	This program finds X and Y as '''4''' and '''13'''.		This program finds X and Y as '''4''' and '''13'''.
	~~== Tabling ==~~
	~~Using tabling, rather than explicit lemmas, can simplify code. [https://binding-time.co.uk/download/xsb_mister_x.txt A version adapted for XSB Prolog is available here.]~~

John: /* integer_sqrt( +N, ?Sqrt ) */

2024-03-01T20:17:11Z

integer_sqrt( +N, ?Sqrt )

← Older revision		Revision as of 20:17, 1 March 2024
Line 85:		Line 85:
	when <var>Sqrt</var><sup>2</sup> ≤ <var>N</var> < (<var>Sqrt</var>+1)<sup>2</sup>.		when <var>Sqrt</var><sup>2</sup> ≤ <var>N</var> < (<var>Sqrt</var>+1)<sup>2</sup>.
	<pre class="prolog">integer_sqrt( N, Sqrt ) :-		<pre class="prolog">integer_sqrt( N, Sqrt ) :-
	~~Float~~ is ~~N * 1.0,~~		Sqrt is floor(sqrt(N)).</pre>
	sqrt( ~~Float, FSqrt~~ ),
	~~Sqrt is integer(FSqrt~~).</pre>
	Load a small library of [[Puzzle Utilities]].		Load a small library of [[Puzzle Utilities]].

	<pre class="prolog">:- ensure_loaded( misc ).</pre>		<pre class="prolog">:- ensure_loaded( misc ).</pre>
	~~The code is available as plain text [https://binding-time.co.uk/download/mister_x.txt here].~~

	== Result ==		== Result ==

John: /* Lemmas */

2024-03-01T20:15:01Z

Lemmas

@@ Line 57: / Line 57: @@
      peter2( Product ),
      susan2( Sum ).</pre>
 == Supporting Predicates ==

John: /* Macros */

2024-03-01T20:14:34Z

Macros

@@ Line 57: / Line 57: @@
      peter2( Product ),
      susan2( Sum ).</pre>
 == Lemmas ==

John: /* SUSAN2: exactly one pair of summands giving Sum has a product with the property PETER2 */

2024-03-01T20:13:55Z

SUSAN2: exactly one pair of summands giving Sum has a product with the property PETER2

← Older revision		Revision as of 20:13, 1 March 2024
Line 39:		Line 39:

	=====SUSAN2: ''exactly one'' pair of summands giving Sum has a product with the property PETER2=====		=====SUSAN2: ''exactly one'' pair of summands giving Sum has a product with the property PETER2=====
	<pre class="prolog">~~property~~( ~~susan2,~~ Sum ) :-		<pre class="prolog">:- table susan2/1.

			susan2( Sum ) :-
	unique_solution( (ordered_summands(Sum, X, Y), peter2(X * Y)) ).</pre>		unique_solution( (ordered_summands(Sum, X, Y), peter2(X * Y)) ).</pre>
	<blockquote>Question: What are the two numbers that Mister X thought of?</blockquote>		<blockquote>Question: What are the two numbers that Mister X thought of?</blockquote>

	=====Unique solution=====		=====Unique solution=====
	<pre class="prolog">solve( X, Y ) :-		<pre class="prolog">solve( X, Y ) :-

John: /* PETER2: exactly one pair of factors giving Product gives a sum with the property SUSAN1 */

2024-03-01T20:13:11Z

PETER2: exactly one pair of factors giving Product gives a sum with the property SUSAN1

← Older revision		Revision as of 20:13, 1 March 2024
Line 31:		Line 31:

	=====PETER2: ''exactly one'' pair of factors giving Product gives a sum with the property SUSAN1=====		=====PETER2: ''exactly one'' pair of factors giving Product gives a sum with the property SUSAN1=====
	<pre class="prolog">~~property~~( ~~peter2,~~ Product ) :-		<pre class="prolog">:- table peter2/1.

			peter2( Product ) :-
	unique_solution( (ordered_factors(Product, X, Y), susan1(X+Y)) ).</pre>		unique_solution( (ordered_factors(Product, X, Y), susan1(X+Y)) ).</pre>

	<blockquote>Susan: “Now I know them too”.</blockquote>		<blockquote>Susan: “Now I know them too”.</blockquote>

	=====SUSAN2: ''exactly one'' pair of summands giving Sum has a product with the property PETER2=====		=====SUSAN2: ''exactly one'' pair of summands giving Sum has a product with the property PETER2=====
	<pre class="prolog">property( susan2, Sum ) :-		<pre class="prolog">property( susan2, Sum ) :-

John: /* SUSAN1: The product of every pair of summands giving Sum has the property PETER1 */

2024-03-01T20:12:28Z

SUSAN1: The product of every pair of summands giving Sum has the property PETER1

← Older revision		Revision as of 20:12, 1 March 2024
Line 22:		Line 22:

	=====SUSAN1: The product of ''every'' pair of summands giving Sum has the property PETER1=====		=====SUSAN1: The product of ''every'' pair of summands giving Sum has the property PETER1=====
	<pre class="prolog">~~property~~( ~~susan1,~~ Sum ) :-		<pre class="prolog">:- table susan1/1.
	forall( ordered_summands(Sum, X, Y), peter1(X * Y) ).</pre>
			susan1( Sum ) :-
			forall( ordered_summands(Sum, X, Y), peter1(X * Y) ).
			</pre>

	<blockquote>Peter: “Really? So now I know the original numbers”.</blockquote>		<blockquote>Peter: “Really? So now I know the original numbers”.</blockquote>

	=====PETER2: ''exactly one'' pair of factors giving Product gives a sum with the property SUSAN1=====		=====PETER2: ''exactly one'' pair of factors giving Product gives a sum with the property SUSAN1=====
	<pre class="prolog">property( peter2, Product ) :-		<pre class="prolog">property( peter2, Product ) :-

John: /* PETER1: There is more than one pair of factors giving Product */

2024-03-01T20:11:50Z

PETER1: There is more than one pair of factors giving Product

← Older revision		Revision as of 20:11, 1 March 2024
Line 14:		Line 14:
	“I can't say definitively which are the original numbers.”</blockquote>		“I can't say definitively which are the original numbers.”</blockquote>
	=====PETER1: There is more than one pair of factors giving Product=====		=====PETER1: There is more than one pair of factors giving Product=====
	<pre class="prolog">~~property~~( ~~peter1,~~ Product ) :-		<pre class="prolog">:- table peter1/1.
	\+ unique_factors( Product ).</pre>
			peter1( Product ) :-
			\+ unique_factors( Product ).
			</pre>
	<blockquote>Then Susan responds: “Neither can I, but I knew that you couldn't know it.”</blockquote>		<blockquote>Then Susan responds: “Neither can I, but I knew that you couldn't know it.”</blockquote>

John: Created page with "NOTOC Although this problem has a straightforward solution, it does demonstrate the value of thinking deductively to understand the problem, which relates to “don't know” nondeterminism, and an appropriate use of lemmas. == Problem: == [https://groups.google.com/forum/#!msg/de.comp.lang.java/xQ6T3kZGqcE/-OTNgyB8yxIJ Problem as posted to comp.lang.prolog] by Thorsten Seelend. Also known as Hans Freudenthal's [[wikipedia:Impossible Puzzle|Impossible Puzzle]..."

2024-03-01T20:11:14Z

Created page with "__NOTOC__ Although this problem has a straightforward solution, it does demonstrate the value of thinking deductively to understand the problem, which relates to “don't know” nondeterminism, and an appropriate use of lemmas. == Problem: == [https://groups.google.com/forum/#!msg/de.comp.lang.java/xQ6T3kZGqcE/-OTNgyB8yxIJ Problem as posted to comp.lang.prolog] by Thorsten Seelend. Also known as Hans Freudenthal's [[wikipedia:Impossible Puzzle|Impossible Puzzle]..."

New page

__NOTOC__
Although this problem has a straightforward solution, it does demonstrate the value of thinking deductively to understand the problem, which relates to “don't know” nondeterminism, and an appropriate use of lemmas.
== Problem: ==
[https://groups.google.com/forum/#!msg/de.comp.lang.java/xQ6T3kZGqcE/-OTNgyB8yxIJ Problem as posted to comp.lang.prolog] by Thorsten Seelend. Also known as Hans Freudenthal's [[wikipedia:Impossible Puzzle|Impossible Puzzle]].

<blockquote>Mister X thinks about two integers between 1 and 100 excluding:
</blockquote>
=====MISTERX: Two integers, X and Y between 2 and 99 (My formalization of the given information)=====
<pre class="prolog">two_integers( X, Y ) :-
between( 2, 98, X ),
between( X, 99, Y ).</pre>
He tells Susan the Sum of them and Peter their Product. Their task is to get the two original values without telling each other the numbers that Mister X told them.
<blockquote>After some time Peter says:
“I can't say definitively which are the original numbers.”</blockquote>
=====PETER1: There is more than one pair of factors giving Product=====
<pre class="prolog">property( peter1, Product ) :-
\+ unique_factors( Product ).</pre>
<blockquote>Then Susan responds: “Neither can I, but I knew that you couldn't know it.”</blockquote>

=====SUSAN1: The product of ''every'' pair of summands giving Sum has the property PETER1=====
<pre class="prolog">property( susan1, Sum ) :-
forall( ordered_summands(Sum, X, Y), peter1(X * Y) ).</pre>

<blockquote>Peter: “Really? So now I know the original numbers”.</blockquote>
=====PETER2: ''exactly one'' pair of factors giving Product gives a sum with the property SUSAN1=====
<pre class="prolog">property( peter2, Product ) :-
unique_solution( (ordered_factors(Product, X, Y), susan1(X+Y)) ).</pre>

<blockquote>Susan: “Now I know them too”.</blockquote>
=====SUSAN2: ''exactly one'' pair of summands giving Sum has a product with the property PETER2=====
<pre class="prolog">property( susan2, Sum ) :-
unique_solution( (ordered_summands(Sum, X, Y), peter2(X * Y)) ).</pre>
<blockquote>Question: What are the two numbers that Mister X thought of?</blockquote>
=====Unique solution=====
<pre class="prolog">solve( X, Y ) :-
unique_solution( mister_x(X, Y) ).

mister_x( X, Y ) :-
two_integers( X, Y ),
Sum is X + Y,
Product is X * Y,
peter1( Product ),
susan1( Sum ),
peter2( Product ),
susan2( Sum ).</pre>

== Macros ==
<pre class="prolog">peter1( Product ) :-
lemma( peter1, Product ).

peter2( Product ) :-
lemma( peter2, Product ).

susan1( Sum ) :-
lemma( susan1, Sum ).

susan2( Sum ) :-
lemma( susan2, Sum ).</pre>

== Lemmas ==
====lemma( +Property, +Expression )====
holds wherever <var>Property</var> holds for <var>Expression</var>.

Asserted facts are used to record successful (''positive'') or failed (''negative'') demonstrations. This saves recomputation without changing the meaning of the pure program.

Although the use of side-effects is generally undesirable, the use of lemmas is justified when the alternative is to compromise performance or clarity.

Using lemmas or tabling to cache results is an order of magnitude faster than recalculating each property every time it is used.
<pre class="prolog">:- dynamic positive/2, negative/2.

lemma( Name, Expression ) :-
Value is Expression,
( positive( Value, Name ) ->
true
; \+ negative( Value, Name ) ->
( property(Name, Value) ->
assert( positive(Value, Name) )
; otherwise ->
assert( negative(Value, Name) ),
fail
)
).</pre>

== Supporting Predicates ==
====ordered_summands( +Sum, ?X, ?Y )====
when <var>X</var> ≤ <var>Y</var> and Sum = <var>X</var>+<var>Y</var>.
NB: Since <var>X</var>≤<var>Y</var> it follows that <var>X</var> ≤ <var>Sum</var>/2.
<pre class="prolog">ordered_summands( Z, X, Y ) :-
Half is Z//2,
between( 2, Half, X ),
Y is Z - X,
between( X, 98, Y ).</pre>
====ordered_factors( +Product, ?X, ?Y )====
when <var>X</var> ≤ <var>Y</var> and <var>Product</var> = <var>X</var> × <var>Y</var>.
NB: Since <var>X</var>≤<var>Y</var> it follows that
<var>X</var> ≤ √<var>Product</var>.
<pre class="prolog">ordered_factors( Z, X, Y ) :-
integer_sqrt( Z, SqrtZ ),
between( 2, SqrtZ, X ),
Y is Z // X,
between( X, 99, Y ),
Z =:= X * Y.</pre>
====unique_factors( +Product )====
when <var>Product</var> has exactly one pair of factors.
<pre class="prolog">unique_factors( Product ) :-
ordered_factors( Product, X, _Y ),
\+ (ordered_factors(Product, X1, _Y1), X1 =\= X).</pre>
====integer_sqrt( +N, ?Sqrt )====
when <var>Sqrt</var><sup>2</sup> ≤ <var>N</var> < (<var>Sqrt</var>+1)<sup>2</sup>.
<pre class="prolog">integer_sqrt( N, Sqrt ) :-
Float is N * 1.0,
sqrt( Float, FSqrt ),
Sqrt is integer(FSqrt).</pre>
Load a small library of [[Puzzle Utilities]].

<pre class="prolog">:- ensure_loaded( misc ).</pre>
The code is available as plain text [https://binding-time.co.uk/download/mister_x.txt here].

== Result ==
This program finds X and Y as '''4''' and '''13'''.
== Tabling ==
Using tabling, rather than explicit lemmas, can simplify code. [https://binding-time.co.uk/download/xsb_mister_x.txt A version adapted for XSB Prolog is available here.]