Computing with infinite data such as real numbers cannot be performed exactly on a Turing machine. Instead, real numbers are treated as an infinite sequence of approximations. Computing a real function means that a Turing machine converts approximations to the argument into approximations of the value, according to Computable Analysis. [Brattka&Hertling’98] have suggested an equivalent but more practical model of computation over the reals: the feasible real-RAM. Based on this fundamental idea, the iRRAM library for C++ has been developed as an imperative programming language which supports abstract datatypes with exact and multivalued semantics.
In this dissertation, we extend Floyd-Hoare logic to formally verify correctness of such algorithms. A set of inference rules is suggested as a systematic framework for program verification.
We also consider the diagonalization of complex self--adjoint matrices with a particular emphasis on the degenerate cases, which in general are ill-posed and in fact provably uncomputable. Employing a Recursive Analysis, we have designed, implemented and evaluated several reliable algorithms on iRRAM which can compute some orthonormal basis of eigenvectors, in the sense of output approximation, up to any desired precision - provided that, in addition to approximations to the d(d+1)/2 matrix' entries, its number of distinct eigenvalues k is known/provided.
근삿값의 무한수열으로서의 실수를 사용하는 연산의 경우 대수적 계산 모형에서의 연산 또는 자연수 유리수 등과 같은 이산적인 대상에 대한 연산과 다른 특성을 갖는다. 실수의 크기 비교는 계산 불가능한 문제임이 알려져 있으며 실수 연산의 계산 복잡도 또한 출력 오차에 영향을 받기에 대수적 계산 모형에서의 또는 이산적 대상에 대한 계산 이론을 직접 대입하기 어려운 점이 있다. 프로그램 검증은 종료 조건을 포함한 프로그램의 입출력 관계에 대한 명제를 증명하는 것이며 간단한 명령형 프로그램의 경우 몇 가지의 추론 규칙을 통하여 진행할 수 있다. 이 논문에서는 기존에 존재하던 프로그램 검증의 추론 규칙을 실수 연산으로 확장한다. 또한 몇 가지 실수 연산 프로그램을 예시로 확장된 추론 규칙을 사용하여 검증한다.
중복된 고윳값을 가질 수 있는 행렬의 경우 튜링 머신에서 계산 불가능하며 추가로 서로 다른 고윳값의 개수가 주어질 경우 계산 가능하다는 사실이 알려져 있다. 이 논문에서는 서로 다른 고윳값의 개수가 주어진 실수 대칭 행렬 또는 복소수 에르미트행렬의 대각화 문제에 대해서 다룬다. 특성 다항식의 해를 찾는 여러 알고리즘들을 분석하며 고윳값을 근사하는 방식에 대해 새로운 접근 방법을 제안한다. 또한 위의 알고리즘들을 실제 구현하며 실행 및 분석한다.
