(hak) 136> fff /cygdrive/d/hak/hlt/src/hlt/fot/fuz/syntax *** Running FFF... *** Run of Wed Sep 12 16:43:56 CEST 2018 *** *** Welcome to FFF, a facility (under development) for fuzzy lattice operations on first-order terms *** *** Type '#help;' for help or 'quit;' to quit (if no prompt upon an error, type ';') *** FFF> #load "ex10.fff"; #load "ex10.fff"; FFF> #fun a/0 b/0 c/0 d/0 f/2 g/2 l/2 h/3; *** The current signature has 8 functors: {a/0, b/0, c/0, d/0, f/2, g/2, l/2, h/3} FFF> #sim a b 0.7 c d 0.6 f g 0.8 l h 0.9; *** Declared similarities: a b 0.7 c d 0.6 f g 0.8 l h 0.9 FFF> #close; *** Computed similarity closure (enter '#show;' to see it) FFF> #trace 2; @@@ tracing in now turned ON at level 2 FFF> h(g(b,Y),f(Y,c),X) \/ l(f(a,Z),g(c,d)); @@@ process the arguments of a term with functor l/2 @@@ argument 1 @@@ unapplying lhs term g(b,Y) and rhs term f(a,Z) at degree 0.9 @@@ there is no similar unapplication for g(b,Y) and f(a,Z) at degree 0.9 @@@ the final unapplied fuzzy pair is the original unchanged @@@ process the arguments of a term with functor g/2 @@@ argument 1 @@@ unapplying lhs term b and rhs term a at degree 0.8 @@@ there is no similar unapplication for b and a at degree 0.8 @@@ the final unapplied fuzzy pair is the original unchanged @@@ argument 2 @@@ unapplying lhs term Y and rhs term Z at degree 0.7 @@@ there is no similar unapplication for Y and Z at degree 0.7 @@@ the final unapplied fuzzy pair is the original unchanged @@@ finished processsing the arguments of g(b,_0) @@@ argument 2 @@@ unapplying lhs term f(Y,c) and rhs term g(c,d) at degree 0.7 @@@ computing similarity degree of f(Y,c) and Y @@@ results in 0.0 @@@ the lhs argument 0's unapplied variable _0 gives term: Y resulting in degree 0.0 @@@ computing similarity degree of g(c,d) and Z @@@ results in 0.0 @@@ the rhs argument 0's unapplied variable _0 gives term: Z resulting in degree 0.0 @@@ so the resulting unapplication degree is 0.0 @@@ there is no similar unapplication for f(Y,c) and g(c,d) at degree 0.7 @@@ the final unapplied fuzzy pair is the original unchanged @@@ process the arguments of a term with functor f/2 @@@ argument 1 @@@ unapplying lhs term Y and rhs term c at degree 0.7 @@@ computing similarity degree of Y and Y @@@ results in 1.0 @@@ the lhs argument 0's unapplied variable _0 gives term: Y resulting in degree 1.0 @@@ computing similarity degree of c and Z @@@ results in 0.0 @@@ the rhs argument 0's unapplied variable _0 gives term: Z resulting in degree 0.0 @@@ so the resulting unapplication degree is 0.0 @@@ there is no similar unapplication for Y and c at degree 0.7 @@@ the final unapplied fuzzy pair is the original unchanged @@@ argument 2 @@@ unapplying lhs term c and rhs term d at degree 0.7 @@@ computing similarity degree of c and Y @@@ results in 0.0 @@@ the lhs argument 0's unapplied variable _0 gives term: Y resulting in degree 0.0 @@@ computing similarity degree of d and Z @@@ results in 0.0 @@@ the rhs argument 0's unapplied variable _0 gives term: Z resulting in degree 0.0 @@@ so the resulting unapplication degree is 0.0 @@@ computing similarity degree of c and Y @@@ results in 0.0 @@@ the lhs argument 1's unapplied variable _1 gives term: Y resulting in degree 0.0 @@@ computing similarity degree of d and c @@@ results in 0.6 @@@ the rhs argument 1's unapplied variable _1 gives term: c resulting in degree 0.6 @@@ so the resulting unapplication degree is 0.0 @@@ there is no similar unapplication for c and d at degree 0.7 @@@ the final unapplied fuzzy pair is the original unchanged @@@ finished processsing the arguments of f(_1,c) @@@ finished processsing the arguments of l(g(b,_0),f(_1,c)) *** The fuzzy lub is l(g(b,_0),f(_1,c)) *** Its approximation degree is 0.6 @@@ partitioning for index 1 corresponding to degree 0.6 @@@ created an array of similarity classes for 8 functors: [a, b, c, d, f, g, l, h] at approximation degree 0.6 (degreeIndex 1) @@@ @@@ computed class of functor a: {a, b} @@@ recording it as a new signature class {a, b} in classes [] @@@ now classes = [{a, b}] @@@ @@@ computed class of functor b: {a, b} @@@ found canonical class for {a, b} in known classes [{a, b}] at index 0: {a, b} @@@ @@@ computed class of functor c: {c, d} @@@ recording it as a new signature class {c, d} in classes [{a, b}] @@@ now classes = [{a, b}, {c, d}] @@@ @@@ computed class of functor d: {c, d} @@@ found canonical class for {c, d} in known classes [{a, b}, {c, d}] at index 1: {c, d} @@@ @@@ computed class of functor f: {f, g} @@@ recording it as a new signature class {f, g} in classes [{a, b}, {c, d}] @@@ now classes = [{a, b}, {c, d}, {f, g}] @@@ @@@ computed class of functor g: {f, g} @@@ found canonical class for {f, g} in known classes [{a, b}, {c, d}, {f, g}] at index 2: {f, g} @@@ @@@ computed class of functor l: {l, h} @@@ recording it as a new signature class {l, h} in classes [{a, b}, {c, d}, {f, g}] @@@ now classes = [{a, b}, {c, d}, {f, g}, {l, h}] @@@ @@@ computed class of functor h: {l, h} @@@ found canonical class for {l, h} in known classes [{a, b}, {c, d}, {f, g}, {l, h}] at index 3: {l, h} @@@ partition(0.6) : @@@ @@@ the set of functors 0.6-similar to a is {a, b} @@@ @@@ the set of functors 0.6-similar to b is {a, b} @@@ @@@ the set of functors 0.6-similar to c is {c, d} @@@ @@@ the set of functors 0.6-similar to d is {c, d} @@@ @@@ the set of functors 0.6-similar to f is {f, g} @@@ @@@ the set of functors 0.6-similar to g is {f, g} @@@ @@@ the set of functors 0.6-similar to l is {l, h} @@@ @@@ the set of functors 0.6-similar to h is {l, h} *** Its 0.6-similar term representative is l(f(a,_0),f(_1,c)) @@@ registered variables: [Y, X, Z, _0, _1] *** Left substitution: *** _0 = Y *** _1 = Y *** Right substitution: *** _0 = Z @@@ partitioning for index 5 corresponding to degree 1.0 @@@ created an array of similarity classes for 8 functors: [a, b, c, d, f, g, l, h] at approximation degree 1.0 (degreeIndex 5) @@@ @@@ computed class of functor a: {a} @@@ recording it as a new signature class {a} in classes [{a, b}, {c, d}, {f, g}, {l, h}] @@@ now classes = [{a, b}, {c, d}, {f, g}, {l, h}, {a}] @@@ @@@ computed class of functor b: {b} @@@ recording it as a new signature class {b} in classes [{a, b}, {c, d}, {f, g}, {l, h}, {a}] @@@ now classes = [{a, b}, {c, d}, {f, g}, {l, h}, {a}, {b}] @@@ @@@ computed class of functor c: {c} @@@ recording it as a new signature class {c} in classes [{a, b}, {c, d}, {f, g}, {l, h}, {a}, {b}] @@@ now classes = [{a, b}, {c, d}, {f, g}, {l, h}, {a}, {b}, {c}] @@@ @@@ computed class of functor d: {d} @@@ recording it as a new signature class {d} in classes [{a, b}, {c, d}, {f, g}, {l, h}, {a}, {b}, {c}] @@@ now classes = [{a, b}, {c, d}, {f, g}, {l, h}, {a}, {b}, {c}, {d}] @@@ @@@ computed class of functor f: {f} @@@ recording it as a new signature class {f} in classes [{a, b}, {c, d}, {f, g}, {l, h}, {a}, {b}, {c}, {d}] @@@ now classes = [{a, b}, {c, d}, {f, g}, {l, h}, {a}, {b}, {c}, {d}, {f}] @@@ @@@ computed class of functor g: {g} @@@ recording it as a new signature class {g} in classes [{a, b}, {c, d}, {f, g}, {l, h}, {a}, {b}, {c}, {d}, {f}] @@@ now classes = [{a, b}, {c, d}, {f, g}, {l, h}, {a}, {b}, {c}, {d}, {f}, {g}] @@@ @@@ computed class of functor l: {l} @@@ recording it as a new signature class {l} in classes [{a, b}, {c, d}, {f, g}, {l, h}, {a}, {b}, {c}, {d}, {f}, {g}] @@@ now classes = [{a, b}, {c, d}, {f, g}, {l, h}, {a}, {b}, {c}, {d}, {f}, {g}, {l}] @@@ @@@ computed class of functor h: {h} @@@ recording it as a new signature class {h} in classes [{a, b}, {c, d}, {f, g}, {l, h}, {a}, {b}, {c}, {d}, {f}, {g}, {l}] @@@ now classes = [{a, b}, {c, d}, {f, g}, {l, h}, {a}, {b}, {c}, {d}, {f}, {g}, {l}, {h}] @@@ partition(1.0) : @@@ @@@ the set of functors 1.0-similar to a is {a} @@@ @@@ the set of functors 1.0-similar to b is {b} @@@ @@@ the set of functors 1.0-similar to c is {c} @@@ @@@ the set of functors 1.0-similar to d is {d} @@@ @@@ the set of functors 1.0-similar to f is {f} @@@ @@@ the set of functors 1.0-similar to g is {g} @@@ @@@ the set of functors 1.0-similar to l is {l} @@@ @@@ the set of functors 1.0-similar to h is {h} *** _1 = c FFF> exit; *** So long - and thanks for playing with FFF... *** We hope that you had some FFFuzzy FFFun! 8^D /cygdrive/d/hak/hlt/src/hlt/fot/fuz/syntax (hak) 137> fff /cygdrive/d/hak/hlt/src/hlt/fot/fuz/syntax *** Running FFF... *** Run of Sat Sep 15 07:29:54 CEST 2018 *** *** Welcome to FFF, a facility (under development) for fuzzy lattice operations on first-order terms *** *** Type '#help;' for help or 'quit;' to quit (if no prompt upon an error, type ';') *** FFF> #load "slidesex.fff"; #load "slidesex.fff"; FFF> #fun a/0 b/0 c/0 d/0 f/2 g/2 h/3; *** The current signature has 7 functors: {a/0, b/0, c/0, d/0, f/2, g/2, h/3} FFF> #sim a b 0.7 c d 0.6 f g 0.9; *** Declared similarities: a b 0.7 c d 0.6 f g 0.9 FFF> #close; *** Computed similarity closure (enter '#show;' to see it) FFF> h(f(a,X1),g(X1,b),f(Y1,Y1)) \/ h(X2,X2,g(c,d)); *** The fuzzy lub is h(_0,_1,f(_2,_3)) *** Its approximation degree is 0.9 *** Its 0.9-similar term representative is h(_0,_1,f(_2,_3)) *** Left substitution: *** _0 = f(a,X1) *** _1 = g(X1,b) *** _2 = Y1 *** _3 = Y1 *** Right substitution: *** _0 = X2 *** _1 = X2 *** _2 = c *** _3 = d FFF> f(Y1,Y1) \/ g(c,d); f(Y1,Y1) \/ g(c,d); *** The fuzzy lub is f(_0,_0) *** Its approximation degree is 0.6 *** Its 0.6-similar term representative is f(_0,_0) *** Left substitution: *** _0 = Y1 *** Right substitution: *** _0 = c FFF> h(f(a,X1),g(X1,b),f(Y1,Y1)) ~ h(X2,X2,g(c,d)); h(f(a,X1),g(X1,b),f(Y1,Y1)) ~ h(X2,X2,g(c,d)); *** These terms' similarity degree is 0.0 FFF> h(f(a,X1),g(X1,b),f(Y1,Y1)) /\ h(X2,X2,g(c,d)); h(f(a,X1),g(X1,b),f(Y1,Y1)) /\ h(X2,X2,g(c,d)); *** The fuzzy glb is h(f(a,b),g(b,b),f(d,d)) *** Its approximation degree is 0.6 *** Its 0.6-similar term representative is h(f(a,a),f(a,a),f(c,c)) *** Unifying substitution: *** X1 = a *** Y1 = c *** X2 = f(a,a) FFF> h(f(a,a),g(a,b),f(c,c)) ~ h(f(a,a),f(a,a),g(c,d)); h(f(a,a),g(a,b),f(c,c)) ~ h(f(a,a),f(a,a),g(c,d)); *** These terms' similarity degree is 0.6 FFF>