File size: 5,650 Bytes
9425aed | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 | {-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeOperators, ScopedTypeVariables #-}
{-# LANGUAGE StrictData, BangPatterns, PatternSynonyms, ViewPatterns #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-- =====================================================================
-- LIQUIDLEAN // THEOREM 3 CRACK: KERNEL & TYPES
-- Target: Genus-0 Forcing via δ-Invariants + Mora Standard Bases
-- Author: Ahmad Ali Parr <ahmedparr93@gmail.com>
-- =====================================================================
module LiquidLean.Jacobian.Theorem3Kernel
( Z
, Polynomial(..)
, RationalFunction(..)
, LocalMonomial(..)
, Thermal(..)
, Energy(..)
, Obstruction(..)
, Result
, phiDecay
, emitEnergy
, zeroPoly
, onePoly
, addPoly
, subPoly
, mulPoly
, scalePoly
, partialDerivative
, evaluate
, totalDegree
, leadingTermLocal
, isZeroPoly
, terms
, fromTerms
, variable
, monomial
) where
import Prelude hiding (Rational)
import GHC.TypeLits (Nat, KnownNat, natVal)
import Data.Ratio (Ratio, denominator, numerator)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Control.Monad.State.Strict
-- | Exact rationals (redefine to avoid shadowing Prelude.Rational in type sigs)
type Rational = Ratio Integer
type Z = Integer
-- | Polynomial in ℚ[u, x] (sparse representation)
newtype Polynomial = Poly { unPoly :: Map (Int, Int) Rational }
deriving (Eq, Show, Ord)
-- | Rational function f/g
data RationalFunction = RF { rfNum :: !Polynomial, rfDen :: !Polynomial }
deriving (Eq, Show)
-- | Monomial in ds-order (degree ascending, lex descending)
data LocalMonomial = LM { lmU :: !Int, lmX :: !Int }
deriving (Eq, Show)
instance Ord LocalMonomial where
compare (LM u1 x1) (LM u2 x2) =
case compare (u1 + x1) (u2 + x2) of
EQ -> compare u2 u1 <> compare x2 x1
o -> o
-- | Thermal monad: energy-accounting computation
newtype Thermal a = Thermal { runThermal :: State Energy a }
deriving (Functor, Applicative, Monad, MonadState Energy)
data Energy = Energy { spent :: !Integer, budget :: !Integer }
deriving (Show)
-- | Obstruction types (total error handling)
data Obstruction
= NotIsolatedSingularity String
| HigherGenusObstruction Int
| NonRationalCurve String
| AdjointSystemDegenerate String
| VerificationFailure String
| PointNotOnCurve (Rational, Rational)
| SingularBasePoint (Rational, Rational)
| ConicFactorizationFailed
| DivisionByZero String
deriving (Show, Eq)
type Result a = Either Obstruction a
-- | Energy constant (φ⁻¹ discretized)
phiDecay :: Integer
phiDecay = 1
emitEnergy :: Integer -> Thermal ()
emitEnergy n = Thermal $ modify $ \e -> e { spent = spent e + n }
-- =====================================================================
-- Polynomial Operations (Total Functions)
-- =====================================================================
zeroPoly, onePoly :: Polynomial
zeroPoly = Poly Map.empty
onePoly = Poly (Map.singleton (0,0) 1)
addPoly, subPoly, mulPoly :: Polynomial -> Polynomial -> Polynomial
addPoly (Poly f) (Poly g) = Poly (Map.unionWith (+) f g)
subPoly (Poly f) (Poly g) = Poly (Map.unionWith (-) f g)
mulPoly (Poly f) (Poly g) = Poly $ Map.fromListWith (+)
[ ((u1+u2, x1+x2), c1*c2) | ((u1,x1),c1) <- Map.toList f
, ((u2,x2),c2) <- Map.toList g
, c1*c2 /= 0 ]
scalePoly :: Rational -> Polynomial -> Polynomial
scalePoly c (Poly f) = Poly (Map.map (c*) f)
-- =====================================================================
-- Differential & Evaluation
-- =====================================================================
partialDerivative :: Polynomial -> Int -> Polynomial
partialDerivative (Poly f) v = Poly $ Map.fromList
[ ((if v == 0 then u-1 else u, if v == 0 then x else x-1), c * fromIntegral (if v == 0 then u else x))
| ((u,x), c) <- Map.toList f
, (v == 0 && u > 0) || (v /= 0 && x > 0)
]
evaluate :: Polynomial -> [Rational] -> Rational
evaluate (Poly f) vals =
sum [ c * (u^u') * (x^x')
| ((u',x'),c) <- Map.toList f
, let u = if null vals then 0 else vals !! 0
, let x = if length vals < 2 then 0 else vals !! 1
]
-- =====================================================================
-- Basic Queries
-- =====================================================================
totalDegree :: Polynomial -> Int
totalDegree (Poly f) = if Map.null f then -1 else maximum [u+x | (u,x) <- Map.keys f]
leadingTermLocal :: Polynomial -> (Rational, LocalMonomial)
leadingTermLocal (Poly f) =
if Map.null f
then (0, LM 0 0)
else let (lm, c) = Map.foldlWithKey (\acc (u,x) c ->
let lm' = LM u x
in if lm' < fst acc then (lm', c) else acc)
(LM maxBound maxBound, 0) f
in (c, lm)
isZeroPoly :: Polynomial -> Bool
isZeroPoly (Poly f) = Map.null f
terms :: Polynomial -> [(Int, Int, Rational)]
terms (Poly f) = [ (u,x,c) | ((u,x),c) <- Map.toList f, c /= 0 ]
fromTerms :: [(Int, Int, Rational)] -> Polynomial
fromTerms = Poly . Map.fromListWith (+) . map (\(u,x,c) -> ((u,x),c)) . filter (\(_,_,c)->c/=0)
-- =====================================================================
-- Variables & Monomials
-- =====================================================================
variable :: Int -> Polynomial
variable 0 = monomial 1 0 -- u
variable 1 = monomial 0 1 -- x
variable i = error ("variable: unsupported index " ++ show i)
monomial :: Int -> Int -> Polynomial
monomial u x = Poly (Map.singleton (u,x) 1)
|