서지주요정보
Verified real computation = 검증된 실수 연산
서명 / 저자 Verified real computation = 검증된 실수 연산 / Se Won Park.
저자명 Park, Se Won ; 박세원
발행사항 [대전 : 한국과학기술원, 2017].
Online Access 원문보기 원문인쇄

소장정보

등록번호

8031434

소장위치/청구기호

학술문화관(문화관) 보존서고

MCS 17045

SMS전송

도서상태

이용가능

대출가능

반납예정일

초록정보

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.

근삿값의 무한수열으로서의 실수를 사용하는 연산의 경우 대수적 계산 모형에서의 연산 또는 자연수 유리수 등과 같은 이산적인 대상에 대한 연산과 다른 특성을 갖는다. 실수의 크기 비교는 계산 불가능한 문제임이 알려져 있으며 실수 연산의 계산 복잡도 또한 출력 오차에 영향을 받기에 대수적 계산 모형에서의 또는 이산적 대상에 대한 계산 이론을 직접 대입하기 어려운 점이 있다. 프로그램 검증은 종료 조건을 포함한 프로그램의 입출력 관계에 대한 명제를 증명하는 것이며 간단한 명령형 프로그램의 경우 몇 가지의 추론 규칙을 통하여 진행할 수 있다. 이 논문에서는 기존에 존재하던 프로그램 검증의 추론 규칙을 실수 연산으로 확장한다. 또한 몇 가지 실수 연산 프로그램을 예시로 확장된 추론 규칙을 사용하여 검증한다. 중복된 고윳값을 가질 수 있는 행렬의 경우 튜링 머신에서 계산 불가능하며 추가로 서로 다른 고윳값의 개수가 주어질 경우 계산 가능하다는 사실이 알려져 있다. 이 논문에서는 서로 다른 고윳값의 개수가 주어진 실수 대칭 행렬 또는 복소수 에르미트행렬의 대각화 문제에 대해서 다룬다. 특성 다항식의 해를 찾는 여러 알고리즘들을 분석하며 고윳값을 근사하는 방식에 대해 새로운 접근 방법을 제안한다. 또한 위의 알고리즘들을 실제 구현하며 실행 및 분석한다.

서지기타정보

서지기타정보
청구기호 {MCS 17045
형태사항 iii, 41 p. : 삽도 ; 30 cm
언어 영어
일반주기 저자명의 한글표기 : 박세원
지도교수의 영문표기 : Martin Ziegler
지도교수의 한글표기 : 마틴 지글러
학위논문 학위논문(석사) - 한국과학기술원 : 전산학부,
서지주기 References: p. 40-41
주제 Computable Analysis
Exact Real Computation
Formal Verification
Matrix Diagonalization
계산 해석학
실수 연산
프로그램 검증
행렬 대각화
QR CODE qr code