Removed identity element argument from 'reduce' ops (#1164)

* Removed identity element argument from 'reduce' ops

* [pre-commit.ci] auto fixes from pre-commit.com hooks

for more information, see https://pre-commit.ci

* Addressed feedback

---------

Co-authored-by: pre-commit-ci[bot] <66853113+pre-commit-ci[bot]@users.noreply.github.com>

Author: MatthewDaggitt

ChangeLog.md

@@ -4,6 +4,18 @@
 
 ### Language
 
+* BREAKING: with the introduction of `infinity` to the language in `v0.25` all reduction operations have
+  sensible zero-dimensional values. Therefore the following operations no longer take the identity element
+  as an argument, i.e.:
+  ```
+  reduceAdd e xs -> reduceAdd xs   (if 0D returns 0)
+  reduceMul e xs -> reduceMul xs   (if 0D returns 1)
+  reduceMin e xs -> reduceMin xs   (if 0D returns infinity)
+  reduceMax e xs -> reduceMax xs   (if 0D returns -infinity)
+  reduceAnd e xs -> reduceAnd xs   (if 0D returns True)
+  reduceOr  e xs -> reduceOr  xs   (if 0D returns False)
+  ```
+
 * Added the operators:
   ```
   ^ : Tensor Real ds -> Real -> Tensor Real ds

docs/language/tensors.rst

@@ -130,16 +130,14 @@ The following operations over tensors are currently supported:
      - |backendall_full|
    * - | Reduce
        | and
-     - ``reduceAnd e t``
-     - | ``Bool →``
-       | ``Tensor Bool ds →``
+     - ``reduceAnd t``
+     - | ``Tensor Bool ds →``
        | ``Bool``
      - |backendall_full|
    * - | Reduce
        | or
-     - ``reduceOr e t``
-     - | ``Bool →``
-       | ``Tensor Bool ds →``
+     - ``reduceOr t``
+     - | ``Tensor Bool ds →``
        | ``Bool``
      - |backendall_full|
    * - | Pointwise
@@ -209,26 +207,26 @@ The following operations over tensors are currently supported:
        | |backendisabelle_easy|
    * - | Reduce
        | add
-     - ``reduceAdd e t``
-     - | ``A → Tensor A ds → A``
+     - ``reduceAdd t``
+     - | ``Tensor A ds → A``
        | (if ``A`` supports ``+``)
      - |backendall_full|
    * - | Reduce
        | multiply
-     - ``reduceMul e t``
-     - | ``A → Tensor A ds → A``
+     - ``reduceMul t``
+     - | ``Tensor A ds → A``
        | (if ``A`` supports ``*``)
      - |backendall_full|
    * - | Reduce
        | min
-     - ``reduceMin e t``
-     - | ``A → Tensor A ds → A``
+     - ``reduceMin t``
+     - | ``Tensor A ds → A``
        | (if ``A`` supports ``min``)
      - |backendall_full|
    * - | Reduce
        | max
-     - ``reduceMax e t``
-     - | ``A → Tensor A ds → A``
+     - ``reduceMax t``
+     - | ``Tensor A ds → A``
        | (if ``A`` supports ``max``)
      - |backendall_full|
 

vehicle-python/src/vehicle_lang/_ast/_nodes.py

@@ -208,7 +208,6 @@ class Var(Expression):
 
 @dataclass(frozen=True)
 class RatTensor(Expression):
-    """RatTensor (Tensor ExtendedFraction) from JSON"""
 
     contents: Tensor
 
@@ -222,109 +221,91 @@ class NegRatTensor(Expression):
 
 @dataclass(frozen=True)
 class AddRatTensor(Expression):
-    """Binary addition: AddRatTensor left right - provides App interface for translation"""
 
     x: Expression
     y: Expression
 
 
 @dataclass(frozen=True)
 class SubRatTensor(Expression):
-    """Binary subtraction: SubRatTensor left right - behaves like App for translation"""
 
     x: Expression
     y: Expression
 
 
 @dataclass(frozen=True)
 class MulRatTensor(Expression):
-    """Binary multiplication: MulRatTensor left right"""
 
     x: Expression
     y: Expression
 
 
 @dataclass(frozen=True)
 class DivRatTensor(Expression):
-    """Binary division: DivRatTensor left right"""
 
     x: Expression
     y: Expression
 
 
 @dataclass(frozen=True)
 class MinRatTensor(Expression):
-    """Binary minimum: MinRatTensor left right"""
 
     x: Expression
     y: Expression
 
 
 @dataclass(frozen=True)
 class MaxRatTensor(Expression):
-    """Binary maximum: MaxRatTensor left right"""
 
     x: Expression
     y: Expression
 
 
 @dataclass(frozen=True)
 class PowRatTensor(Expression):
-    """Binary power: PowRatTensor left right"""
 
     x: Expression
     y: Expression
 
 
 @dataclass(frozen=True)
 class LogRatTensor(Expression):
-    """Pointwise natural log: LogRatTensor x"""
 
     x: Expression
 
 
 @dataclass(frozen=True)
 class ExpRatTensor(Expression):
-    """Pointwise exponential: ExpRatTensor x"""
 
     x: Expression
 
 
 @dataclass(frozen=True)
 class ReduceAddRatTensor(Expression):
-    """Reduce addition: ReduceAddRatTensor expr dims"""
 
-    f: Expression
     x: Expression
 
 
 @dataclass(frozen=True)
 class ReduceMulRatTensor(Expression):
-    """Reduce multiplication: ReduceMulRatTensor expr dims"""
 
-    f: Expression
     x: Expression
 
 
 @dataclass(frozen=True)
 class ReduceMinRatTensor(Expression):
-    """Reduce minimum: ReduceMinRatTensor expr dims"""
 
-    f: Expression
     x: Expression
 
 
 @dataclass(frozen=True)
 class ReduceMaxRatTensor(Expression):
-    """Reduce maximum: ReduceMaxRatTensor expr dims"""
 
-    f: Expression
     x: Expression
 
 
 @dataclass(frozen=True)
 class SearchRatTensor(Expression):
-    """Search tensor: SearchRatTensor reductionOp lowerBound upperBound searchLambda"""
 
     name: str
     reduction_op: Expression
@@ -337,19 +318,17 @@ class SearchRatTensor(Expression):
 
 @dataclass(frozen=True)
 class Dimension(Expression):
-    """Dimension Int - for JSON parsing"""
 
     value: int
 
 
 @dataclass(frozen=True)
 class DimensionNil(Expression):
-    """DimensionNil - for JSON parsing"""
+    pass
 
 
 @dataclass(frozen=True)
 class DimensionLookup(Expression):
-    """Dimension lookup: DimensionLookup tensor index"""
 
     xs: Expression
     i: Expression
@@ -368,15 +347,13 @@ class DimensionIndex(Expression):
 
 @dataclass(frozen=True)
 class ConstTensor(Expression):
-    """ConstTensor shape value - for JSON parsing"""
 
     c: ExtendedFraction
     ds: Sequence[int]
 
 
 @dataclass(frozen=True)
 class StackTensor(Expression):
-    """StackTensor : StackTensor tensor_list"""
 
     xs: Sequence[Expression]
 

vehicle-python/src/vehicle_lang/loss/_abc/_builtins.py

@@ -54,16 +54,16 @@ def LogRatTensor(self, x: vcl.Tensor) -> vcl.Tensor: ...
     def ExpRatTensor(self, x: vcl.Tensor) -> vcl.Tensor: ...
 
     @abstractmethod
-    def ReduceAddRatTensor(self, e: vcl.Rat, xs: vcl.Tensor) -> vcl.Tensor: ...
+    def ReduceAddRatTensor(self, xs: vcl.Tensor) -> vcl.Tensor: ...
 
     @abstractmethod
-    def ReduceMulRatTensor(self, e: vcl.Rat, x: vcl.Tensor) -> vcl.Tensor: ...
+    def ReduceMulRatTensor(self, x: vcl.Tensor) -> vcl.Tensor: ...
 
     @abstractmethod
-    def ReduceMinRatTensor(self, e: vcl.Rat, x: vcl.Tensor) -> vcl.Tensor: ...
+    def ReduceMinRatTensor(self, x: vcl.Tensor) -> vcl.Tensor: ...
 
     @abstractmethod
-    def ReduceMaxRatTensor(self, e: vcl.Rat, x: vcl.Tensor) -> vcl.Tensor: ...
+    def ReduceMaxRatTensor(self, x: vcl.Tensor) -> vcl.Tensor: ...
 
     @abstractmethod
     def DimensionLookup(self, xs: vcl.Tensor, i: vcl.Index) -> vcl.Tensor: ...

vehicle-python/src/vehicle_lang/loss/_python/_translation.py

@@ -287,7 +287,6 @@ def translate_ReduceAddRatTensor(
         """Translate ReduceAddRatTensor to builtin call."""
         return py_app(
             py_builtin("ReduceAddRatTensor", provenance=vcl.MISSING),
-            self.translate_expression(expression.f),  # Note: using current field names
             self.translate_expression(expression.x),
             provenance=vcl.MISSING,
         )
@@ -298,7 +297,6 @@ def translate_ReduceMulRatTensor(
         """Translate ReduceMulRatTensor to builtin call."""
         return py_app(
             py_builtin("ReduceMulRatTensor", provenance=vcl.MISSING),
-            self.translate_expression(expression.f),
             self.translate_expression(expression.x),
             provenance=vcl.MISSING,
         )
@@ -309,7 +307,6 @@ def translate_ReduceMinRatTensor(
         """Translate ReduceMinRatTensor to builtin call."""
         return py_app(
             py_builtin("ReduceMinRatTensor", provenance=vcl.MISSING),
-            self.translate_expression(expression.f),
             self.translate_expression(expression.x),
             provenance=vcl.MISSING,
         )
@@ -320,20 +317,15 @@ def translate_ReduceMaxRatTensor(
         """Translate ReduceMaxRatTensor to builtin call."""
         return py_app(
             py_builtin("ReduceMaxRatTensor", provenance=vcl.MISSING),
-            self.translate_expression(expression.f),
             self.translate_expression(expression.x),
             provenance=vcl.MISSING,
         )
 
     def translate_SearchRatTensor(self, expression: vcl.SearchRatTensor) -> py.expr:
         """Translate SearchRatTensor to builtin call.
 
-        The reduction_op is a curried function (λe. λxs. reduce e xs) where:
-        - e is the identity element (a 0-dimensional tensor)
+        The reduction_op is a curried function (λxs. reduce xs) where:
         - xs is the sequence of samples to reduce
-
-        Since the Python Reduce* functions don't actually use the identity parameter,
-        we pass a dummy 0-dimensional tensor with value 0.
         """
         # Call sampler once to get samples
         sampler_call = py_app(
@@ -350,27 +342,9 @@ def translate_SearchRatTensor(self, expression: vcl.SearchRatTensor) -> py.expr:
             provenance=vcl.MISSING,
         )
 
-        # Create a dummy identity element (0-dimensional tensor with value 0)
-        # The Python Reduce* implementations don't actually use this parameter
-        identity = py_app(
-            py_builtin("ConstTensor", provenance=vcl.MISSING),
-            py.Constant(value=0, **asdict(vcl.MISSING)),
-            py_app(
-                py_builtin("DimensionNil", provenance=vcl.MISSING),
-                provenance=vcl.MISSING,
-            ),
-            provenance=vcl.MISSING,
-        )
-
-        # Apply as: reduction_op(identity)(samples)
-        partial_reduction = py_app(
-            self.translate_expression(expression.reduction_op),
-            identity,
-            provenance=vcl.MISSING,
-        )
-
+        # Apply as: reduction_op(samples)
         return py_app(
-            partial_reduction,
+            self.translate_expression(expression.reduction_op),
             sampler_call,
             provenance=vcl.MISSING,
         )

vehicle-python/src/vehicle_lang/loss/_pytorch/_builtins.py

@@ -118,31 +118,19 @@ def ExpRatTensor(self, x: torch.Tensor) -> torch.Tensor:
         return torch.exp(torch.as_tensor(x))
 
     @override
-    def ReduceAddRatTensor(
-        self, e: float, xs: torch.Tensor | Sequence[torch.Tensor]
-    ) -> torch.Tensor:
-        xs = torch.stack(list(xs))
-        return torch.add(torch.sum(xs), e)
+    def ReduceAddRatTensor(self, xs: torch.Tensor) -> torch.Tensor:
+        return torch.sum(xs)
 
     @override
-    def ReduceMulRatTensor(
-        self, e: float, x: torch.Tensor | Sequence[torch.Tensor]
-    ) -> torch.Tensor:
-        x = torch.stack(list(x))
-        return torch.mul(torch.prod(x), e)
+    def ReduceMulRatTensor(self, x: torch.Tensor) -> torch.Tensor:
+        return torch.prod(x)
 
     @override
-    def ReduceMinRatTensor(
-        self, e: float, x: torch.Tensor | Sequence[torch.Tensor]
-    ) -> torch.Tensor:
-        x = torch.stack([torch.Tensor(e)] + list(x))
+    def ReduceMinRatTensor(self, x: torch.Tensor) -> torch.Tensor:
         return torch.min(x)
 
     @override
-    def ReduceMaxRatTensor(
-        self, e: float, x: torch.Tensor | Sequence[torch.Tensor]
-    ) -> torch.Tensor:
-        x = torch.stack([torch.Tensor(e)] + list(x))
+    def ReduceMaxRatTensor(self, x: torch.Tensor) -> torch.Tensor:
         return torch.max(x)
 
     @override