Merge pull request #152 from engboris/fix

Implement ~= as term unifiability instead of ray compatibility

Author: engboris

BASICS.md

@@ -77,14 +77,15 @@ a $ :b c
 
 **Unification** = finding substitutions that make two terms identical.
 
+You can check if two terms are matchable with the term `(~= t u)` where `t` and
+`u` are terms.
+
 For example:
 
 ```stellogen
-'''
-(f X)  ~  (f (h a))    =>  they match with {X := (h a)}
-(f X)  ~  X            =>  ❌ (circular)
-(f X)  ~  (g X)        =>  ❌ (they don't match because different head symbol)
-'''
+(~= (f X)  (f (h a)))  '  =>  they match with {X := (h a)}
+(~= (f X)  X)          '  =>  ❌ (circular)
+(~= (f X)  (g X))      '  =>  ❌ (they don't match because different head symbol)
 ```
 
 A **ray** is a term with polarity:
@@ -94,12 +95,13 @@ A **ray** is a term with polarity:
 * `(f X)`  → neutral (does not interact)
 
 Two rays and **compatible** and can interact if they have opposite polarities
-**and** their terms unify. You can check compatibility with the term
-`(~= t u)` with arguments `t` and `u` which are rays.
+**and** their terms unify.
 
 ```stellogen
-(~= (+f X) (-f (h a)))   ' =>  succeeds with {X := (h a)}
-' (~= (+f X) (+f a))     ' =>  ❌ (fails because same polarity)
+'''
+(+f X) and (-f (h a)))  are compatible with {X := (h a)}
+(+f X) and (+f a))      are incompatible because they have same head polarity
+'''
 ```
 
 ---

examples/proofnets/mll.sg

@@ -115,11 +115,11 @@
 '
 '   [3, 6]
 '
-' This corresponds to the following executio in stellogen
+' This corresponds to the following execution in stellogen
 ' in which [] is a way to initiate a starting point in computation
 (:= comp (exec #x @[(-3 X) (+3 X)]))
-(:= res { [(+3 X9) (+6 X9)] })
-' (== #comp #res)
+(:= res { [(+3 X) (+6 X)] })
+(~= #comp #res)
 
 ' as for the proof of identity (A ⊗ B) -o (A ⊗ B):
 '

src/lsc_ast.ml

@@ -27,7 +27,25 @@ module StellarSig = struct
     | _ -> false
 end
 
+module MatchableSig = struct
+  type idvar = string * int option
+
+  type idfunc = polarity * string
+
+  let string_of_idvar (s, index_opt) =
+    match index_opt with None -> s | Some j -> s ^ Int.to_string j
+
+  let equal_idvar x y = String.equal (string_of_idvar x) (string_of_idvar y)
+
+  let equal_idfunc (p1, f1) (p2, f2) =
+    equal_polarity p1 p2 && String.equal f1 f2
+
+  (* Matchable: only checks function name equality, ignores polarity *)
+  let compatible (_p1, f1) (_p2, f2) = String.equal f1 f2
+end
+
 module StellarRays = Unification.Make (StellarSig)
+module MatchableRays = Unification.Make (MatchableSig)
 open StellarRays
 
 (* ---------------------------------------
@@ -98,6 +116,18 @@ let replace_indices (i : int) : ray -> ray =
 let raymatcher r r' : substitution option =
   if is_polarised r && is_polarised r' then solution [ (r, r') ] else None
 
+(* Convert StellarRays.term to MatchableRays.term *)
+let rec to_matchable_term : StellarRays.term -> MatchableRays.term = function
+  | StellarRays.Var x -> MatchableRays.Var x
+  | StellarRays.Func (f, ts) ->
+    MatchableRays.Func (f, List.map ~f:to_matchable_term ts)
+
+(* Check if two rays can unify using term unification (ignoring polarity) *)
+let terms_unifiable r r' =
+  let r_match = to_matchable_term r in
+  let r'_match = to_matchable_term r' in
+  MatchableRays.solution [ (r_match, r'_match) ] |> Option.is_some
+
 let fresh_var vars =
   let rec find_fresh_index i =
     if List.mem vars ("X", Some i) ~equal:StellarSig.equal_idvar then

src/sgen_eval.ml

@@ -9,9 +9,9 @@ let ( let* ) x f = Result.bind x ~f
 
 let unifiable r r' = StellarRays.solution [ (r, r') ] |> Option.is_some
 
-let constellations_compatible c1 c2 =
-  (* Check if two constellations are compatible for Match (~=) *)
-  (* Uses unifiable which requires opposite polarities for interaction *)
+let constellations_matchable c1 c2 =
+  (* Check if two constellations are matchable for Match (~=) *)
+  (* Uses term unification (ignoring polarity, only checking function name equality) *)
   let open Lsc_ast in
   (* Extract all rays from both constellations *)
   let rays_from_constellation c =
@@ -20,9 +20,9 @@ let constellations_compatible c1 c2 =
   let rays1 = rays_from_constellation c1 in
   let rays2 = rays_from_constellation c2 in
 
-  (* Check if any ray from c1 is unifiable with any ray from c2 *)
+  (* Check if any ray from c1 can unify with any ray from c2 (ignoring polarity) *)
   List.exists rays1 ~f:(fun r1 ->
-    List.exists rays2 ~f:(fun r2 -> unifiable r1 r2) )
+    List.exists rays2 ~f:(fun r2 -> terms_unifiable r1 r2) )
 
 let rec find_with_solution env x =
   let rec search_objs = function
@@ -32,7 +32,12 @@ let rec find_with_solution env x =
       let value_normalized = map_ray env ~f:(replace_indices 0) value in
       let x_normalized = replace_indices 1 x in
       match StellarRays.solution [ (key_normalized, x_normalized) ] with
-      | Some substitution -> Some (value_normalized, substitution)
+      | Some substitution ->
+        (* Only use renamed value if there's actual parameter substitution *)
+        let result_value =
+          if List.is_empty substitution then value else value_normalized
+        in
+        Some (result_value, substitution)
       | None -> search_objs rest )
   in
   search_objs env.objs
@@ -299,7 +304,7 @@ let rec eval_sgen_expr (env : env) :
     let* env2, eval2 = eval_sgen_expr env1 expr2 in
     let const1 = List.map eval1 ~f:Marked.remove in
     let const2 = List.map eval2 ~f:Marked.remove in
-    if constellations_compatible const1 const2 then Ok (env2, [])
+    if constellations_matchable const1 const2 then Ok (env2, [])
     else Error (MatchError { term1 = eval1; term2 = eval2; message; location })
   | Use path -> (
     let open Lsc_ast.StellarRays in

test/examples.t

@@ -55,7 +55,7 @@ NPDA (non-deterministic pushdown automaton) example:
 Prolog-style examples:
   $ sgen run ../examples/prolog.sg
   (s (s (s (s 0))))
-  [(-grandparent tom Z0) Z0]
+  [(-grandparent tom Z) Z]
   { [ok (-to 1)] [(-from 5)] [(-from 4)] [(-from 5)] }
 
 Stack example:
@@ -72,7 +72,7 @@ Syntax reference:
   { [c] [b] [a] }
   (%string hello world)
   (function a b)
-  { [(-f X0) (-f Y0) (r X0 Y0) || (!= X Y)] [(+f b)] [(+f a)] }
+  { [(-f X) (-f Y) (r X Y) || (!= X Y)] [(+f b)] [(+f a)] }
   { [(r b a) || (!= b a)] [(r a b) || (!= a b)] }
   (+n2 (s (s 0)))
   { [(+field test2) (%cons (+f b) (%cons ok %nil))] [(+field test1) (%cons (+f a) (%cons ok %nil))] }