Gauss-Jordan Elimination for Matrices Represented as Functions
Gauss-Jordan Elimination for Matrices Represented as Functions
复制标题
表示为函数的矩阵的高斯约当消元法
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
T. Nipkow
中科院分区：
文献类型：
--
作者：
T. Nipkow
这个理论提供了一个紧凑的公式高斯-约旦消除矩阵表示为函数。它的显著特点是简洁。它不适合大型计算。1 Gauss-Jordan消元算法理论Gauss-Jordan-Elim-Fun导入主要开始矩阵是函数：type-synonym ′a matrix = nat nat ′a为了限制为有限矩阵，一个矩阵通常与一个或两个自然数组合，表示矩阵的最大行和最大列。高斯-约当消去法用自然数n参数化。它表示矩阵A有n行和n列。实际上，A是具有n+1列的增广矩阵。列n是“右侧”，即常数向量B。结果是单位矩阵被第n列中的解增广;参见下面的正确性定理。fun gauss-jordan：：（′a：：field）matrix矩阵选项其中gauss-jordan A 0 = Some（A）|gauss-jordan A（Suc m）=（case dropWhile（λi . A i m = 0）[0.. <Suc m] of []无|p #λ（设Ap ′ =（λj . A p j / A p m）; A ′ =（λi .如果i=p，则Ap ′ else（λj . A i j − A i m <$Ap ′ j））在gauss-jordan（Fun.swap p m A ′）m））中一些辅助函数：定义解：：（′a：：field）矩阵nat（nat ′a）bool其中
This theory provides a compact formulation of Gauss-Jordan elimination for matrices represented as functions. Its distinctive feature is succinctness. It is not meant for large computations. 1 Gauss-Jordan elimination algorithm theory Gauss-Jordan-Elim-Fun imports Main begin Matrices are functions: type-synonym ′a matrix = nat ⇒ nat ⇒ ′a In order to restrict to finite matrices, a matrix is usually combined with one or two natural numbers indicating the maximal row and column of the matrix. Gauss-Jordan elimination is parameterized with a natural number n. It indicates that the matrix A has n rows and columns. In fact, A is the augmented matrix with n+1 columns. Column n is the “right-hand side”, i.e. the constant vector b. The result is the unit matrix augmented with the solution in column n; see the correctness theorem below. fun gauss-jordan :: ( ′a::field)matrix ⇒ nat ⇒ ( ′a)matrix option where gauss-jordan A 0 = Some(A) | gauss-jordan A (Suc m) = (case dropWhile (λi . A i m = 0 ) [0 ..<Suc m] of [] ⇒ None | p # ⇒ (let Ap ′ = (λj . A p j / A p m); A ′ = (λi . if i=p then Ap ′ else (λj . A i j − A i m ∗ Ap ′ j )) in gauss-jordan (Fun.swap p m A ′) m)) Some auxiliary functions: definition solution :: ( ′a::field)matrix ⇒ nat ⇒ (nat ⇒ ′a) ⇒ bool where