Summary
Extend Tiny-Maude to support subsort declarations, and modify the term typing, operator application, and rewrite matching mechanisms accordingly. This adds order-sorted logic support, enabling features like operator overloading, safe coercion, and partiality handling.
Motivation
OBJ3 and Maude support order-sorted equational logic. This allows certain terms of one sort to be automatically treated as another — for instance, treating all Nat as Int if subsort Nat < Int is declared. Subsorts are essential for:
- Overloading operators (e.g.,
_+_ for both Nat and Int)
- Supporting error handling via sort refinement
- Simplifying user code by avoiding manual casts
- Building semantics with multiple representations
Functional Requirements
1. Syntax Support
Add parser support for subsort and subsorts declarations:
sorts Nat Int .
subsort Nat < Int .
Allow multi-level declarations:
sorts A B C D .
subsorts A < B < C .
subsorts A B < D .
2. Sort Hierarchy
• Maintain a directed acyclic graph (DAG) of declared sorts.
• Each sort must belong to exactly one kind (connected component).
• Enforce no cycles in the subsort relation at module load time.
3. Term Typing
• Terms must carry a declared sort.
• A term of sort S is also valid where a sort T is expected if S < T.
• Least common sort (aka “least sort”) computation is required for matching overloads or resolving ambiguities.
4. Operator Declarations & Overloading
Allow the same operator name with multiple type signatures:
op + : Nat Nat -> Nat .
op + : Int Int -> Int .
A term like 2 + 3 where 2 and 3 are of sort Nat should resolve to the first declaration. But 2 + (-5) (where -5 is Int) should use the second. Implicit upcasting from Nat to Int should be supported if needed.
5. Rewrite Matching
• During equation or rule matching, allow subsort-based matches.
• If a pattern expects a term of sort T, it can be matched by a term of sort S if S < T.
6. Optional: Retracts
Support optional retracts to handle cases where downcasting is required (e.g., using an Int where Nat is expected). This is not strictly required in the initial implementation, but it may be used to flag sort mismatches explicitly.
Example
Input Module
sorts Zero Nat Int .
subsort Zero < Nat < Int .
op 0 : -> Zero .
op s_ : Nat -> Nat .
op _+_ : Int Int -> Int .
vars X Y : Nat .
eq s(X) + Y = s(X + Y) .
Expected Behavior
• A term like s(0) + 0 should parse correctly and reduce using the rule above.
• The variable X : Nat can be instantiated with a Zero term due to Zero < Nat.
Implementation Plan
• Extend AST to capture subsort declarations.
• Build a SortGraph or SortHierarchy type to track the DAG of sorts.
• Modify term type-checking to allow upward coercion along the subsort graph.
• Implement least sort resolution for overloaded operator dispatch.
• Extend matcher/unifier to allow terms of a subsort to match against a supersort pattern.
• Add error handling for cyclic subsort declarations or unknown sorts.
• Add tests covering successful coercion, overload resolution, and failure cases.
Notes
• Subsorts should never require explicit coercion by the user.
• Cycles in the subsort graph must raise a hard error.
• The implementation should respect module boundaries — only sorts visible in scope can participate in coercions.
Summary
Extend Tiny-Maude to support subsort declarations, and modify the term typing, operator application, and rewrite matching mechanisms accordingly. This adds order-sorted logic support, enabling features like operator overloading, safe coercion, and partiality handling.
Motivation
OBJ3 and Maude support order-sorted equational logic. This allows certain terms of one sort to be automatically treated as another — for instance, treating all
NatasIntifsubsort Nat < Intis declared. Subsorts are essential for:_+_for bothNatandInt)Functional Requirements
1. Syntax Support
Add parser support for
subsortandsubsortsdeclarations:Allow multi-level declarations:
sorts A B C D .
subsorts A < B < C .
subsorts A B < D .
2. Sort Hierarchy
• Maintain a directed acyclic graph (DAG) of declared sorts.
• Each sort must belong to exactly one kind (connected component).
• Enforce no cycles in the subsort relation at module load time.
3. Term Typing
• Terms must carry a declared sort.
• A term of sort S is also valid where a sort T is expected if S < T.
• Least common sort (aka “least sort”) computation is required for matching overloads or resolving ambiguities.
4. Operator Declarations & Overloading
Allow the same operator name with multiple type signatures:
op + : Nat Nat -> Nat .
op + : Int Int -> Int .
A term like 2 + 3 where 2 and 3 are of sort Nat should resolve to the first declaration. But 2 + (-5) (where -5 is Int) should use the second. Implicit upcasting from Nat to Int should be supported if needed.
5. Rewrite Matching
• During equation or rule matching, allow subsort-based matches.
• If a pattern expects a term of sort T, it can be matched by a term of sort S if S < T.
6. Optional: Retracts
Support optional retracts to handle cases where downcasting is required (e.g., using an Int where Nat is expected). This is not strictly required in the initial implementation, but it may be used to flag sort mismatches explicitly.
Example
Input Module
Expected Behavior
• A term like s(0) + 0 should parse correctly and reduce using the rule above.
• The variable X : Nat can be instantiated with a Zero term due to Zero < Nat.
Implementation Plan
• Extend AST to capture subsort declarations.
• Build a SortGraph or SortHierarchy type to track the DAG of sorts.
• Modify term type-checking to allow upward coercion along the subsort graph.
• Implement least sort resolution for overloaded operator dispatch.
• Extend matcher/unifier to allow terms of a subsort to match against a supersort pattern.
• Add error handling for cyclic subsort declarations or unknown sorts.
• Add tests covering successful coercion, overload resolution, and failure cases.
Notes
• Subsorts should never require explicit coercion by the user.
• Cycles in the subsort graph must raise a hard error.
• The implementation should respect module boundaries — only sorts visible in scope can participate in coercions.