Category:CafeOBJ: Difference between revisions
Content added Content deleted
No edit summary |
No edit summary |
||
| Line 43: | Line 43: | ||
vars N N' : Nat |
vars N N' : Nat |
||
-- A very short sorting program using |
-- A very short sorting program using on transition equation in POA logic, which is a type of rewrite logic/ |
||
-- The program is in the form of a condition transition, which will swap N and N' if N is larger or equal to N'. |
|||
-- This is a equation in POA logic so there is no need for an intermediate variable to do the swap. |
|||
ctrans [swap] : (N . N') => (N' . N) if N' <= N . |
ctrans [swap] : (N . N') => (N' . N) if N' <= N . |
||
} |
} |
||
| Line 50: | Line 52: | ||
open SORTING-NAT |
open SORTING-NAT |
||
exec (3 . 2 . 1) . |
exec (3 . 2 . 1) . |
||
**> We can consider sorting as a path through the state space of the permutations of N numbers. |
|||
**> There are N! permutations only one of which is sorted. |
|||
**> Sorting natural numbers using search command |
**> Sorting natural numbers using search command |
||
**> we can use (show path N) with this command, where N is the |
**> we can use (show path N) with this command, where N is the number of possible states. |
||
red (3 . 2 . 1) =(1,1)=>* (1 . 2 . 3) . |
red (3 . 2 . 1) =(1,1)=>* (1 . 2 . 3) . |
||
red (3 . 2 . 1) =(1,2)=>* (1 . 2 . 3) . |
red (3 . 2 . 1) =(1,2)=>* (1 . 2 . 3) . |
||