shopkeeper/korean_wiki_content_only_120125 huggingface dataset:
임의 정밀도로 저장된 숫자에 대한 산술 연산을 효율적으로 수행하기 위해 수많은 알고리즘이 개발되었다. 특히 자릿수가 사용된다고 가정할 때, 큰 에 대한 점근 복잡도를 최소화하기 위한 알고리즘이 설계되었다.
가장 간단한 알고리즘은 덧셈과 뺄셈이며, 여기서는 단순히 자릿수를 순서대로 더하거나 빼고 필요에 따라 올림수를 처리하여 알고리즘( 점근 표기법 참조)을 산출한다.
비교 또한 매우 간단하다. 차이가 발견될 때까지 상위 자릿수(또는 기계어 단어)를 비교한다. 나머지 자릿수/단어를 비교할 필요는 없다. 최악의 경우는 이지만, 유사한 크기의 피연산자로 훨씬 더 빨리 완료될 수 있다.
곱셈의 경우, 손으로 숫자를 곱하는 데 사용되는 가장 간단한 알고리즘(초등학교에서 가르치는 대로)은 연산이 필요하지만, 곱셈 알고리즘은 고속 푸리에 변환에 기반한 쇤하게-슈트라센 알고리즘과 같이 복잡도를 달성하는 알고리즘이 고안되었으며, 약간 더 나쁜 복잡도를 가지지만 더 작은 에 대해 때로는 뛰어난 실제 성능을 보이는 알고리즘도 있다. 카라추바 알고리즘 곱셈이 그러한 알고리즘이다.
나눗셈의 경우, 호제법을 참조하라.
복잡도 추정치와 함께 알고리즘 목록은 수학 연산의 계산 복잡도를 참조하라.
X86 어셈블리 예시는 외부 링크를 참조하라.
사전 설정 정밀도.
REXX 및 ooRexx와 같은 일부 언어에서는 계산을 수행하기 전에 모든 계산의 정밀도를 설정해야 한다. 파이썬 및 루비와 같은 다른 언어는 오버플로를 방지하기 위해 자동으로 정밀도를 확장한다.
계승 계산은 매우 큰 숫자를 쉽게 생성할 수 있다. 이는 많은 공식(테일러 급수 등)에서 사용되는 데 문제가 되지 않는다. 왜냐하면 다른 항과 함께 나타나기 때문에, 평가 순서에 주의를 기울이면 중간 계산 값이 문제가 되지 않기 때문이다. 계승 값의 근사치가 필요한 경우 스털링 근사는 부동 소수점 연산을 사용하여 좋은 결과를 제공한다. 고정 크기 정수 변수의 가장 큰 표현 가능한 값은 아래 표에 나타난 것처럼 상대적으로 작은 인수에서도 초과될 수 있다. 부동 소수점 숫자도 곧 범위를 벗어나므로, 계산을 숫자의 로그로 다시 캐스팅하는 것이 도움이 될 수 있다.
그러나 큰 계승에 대한 정확한 값이 필요한 경우, 다음의 의사코드와 같이 특수 소프트웨어가 필요하다. 이 코드는 연속적인 계승 값인 1, 1×2, 1×2×3, 1×2×3×4 등을 계산하는 고전적인 알고리즘을 구현한다.
상수:
Limit = 1000 % 충분한 자릿수.
Base = 10 % 시뮬레이션된 연산의 기수.
FactorialLimit = 365 % 해결할 목표 숫자, 365!
tdigit: Array[0:9] of character = ["0","1","2","3","4","5","6","7","8","9"]
digit: Array[1:Limit] of 0..9 % 큰 숫자.
carry, d: Integer % 곱셈 중 보조 변수.
last: Integer % 큰 숫자의 자릿수 인덱스.
text: Array[1:Limit] of character % 출력을 위한 임시 공간.
digit[*] := 0 % 배열 전체를 지운다.
last := 1 % 큰 숫자는 한 자릿수부터 시작하며,
digit[1] := 1 % 유일한 자릿수는 1이다.
for n := 1 to FactorialLimit: % 1!, 2!, 3!, 4! 등을 순차적으로 생성한다.
carry := 0 % n을 곱하기 시작한다.
for i := 1 to last: % 모든 자릿수를 따라간다.
d := digit[i] * n + carry % 한 자릿수를 곱한다.
digit[i] := d mod Base % 결과의 하위 자릿수를 유지한다.
carry := d div Base % 다음 자릿수로 올림수를 전달한다.
while carry &gt; 0: % 남은 올림수를 큰 숫자에 저장한다.
if last &gt;= Limit: error("overflow")
last := last + 1 % 한 자릿수 추가.
digit[last] := carry mod Base
carry := carry div Base % 올림수에서 마지막 자릿수를 제거한다.
text[*] := " " % 이제 출력을 준비한다.
for i := 1 to last: % 이진수에서 텍스트로 변환한다.
text[Limit - i + 1] := tdigit[digit[i]] % 순서를 뒤집는다.
print text[Limit - last + 1:Limit], " = ", n, "!"
이 예제를 통해 여러 세부 사항을 논의할 수 있다. 가장 중요한 것은 큰 수 표현 방식의 선택이다. 이 경우, 자릿수에 정수 값만 필요하므로 고정 너비 정수 배열이 적절하다. 배열의 연속적인 요소가 기수의 더 높은 거듭제곱을 나타내도록 하는 것이 편리하다.
두 번째로 중요한 결정은 산술의 기수(여기서는 10)를 선택하는 것이다. 고려해야 할 사항이 많다. 스크래치패드 변수 는 한 자릿수 곱셈의 결과와 이전 자릿수 곱셈의 올림수를 합한 값을 담을 수 있어야 한다. 10진법에서는 16비트 정수가 32767까지 허용하므로 확실히 적절하다. 그러나 이 예제는 의 값이 한 자릿수로 제한되지 않는다는 점에서 속임수를 썼다. 이는 정도에서는 이 방법이 실패할 것이라는 결과를 초래한다. 더 일반적인 구현에서는 도 여러 자릿수 표현을 사용한다. 지름길의 두 번째 결과는 여러 자릿수 곱셈이 완료된 후, 올림수의 마지막 값이 단일 자릿수가 아니라 여러 상위 자릿수로 전달되어야 할 수 있다는 것이다.
사람의 고려를 위해 결과를 10진수로 인쇄하는 문제도 있다. 기수가 이미 10이므로 배열 `digit`의 연속적인 자릿수를 인쇄하여 결과를 간단하게 표시할 수 있지만, 가장 높은 자릿수가 마지막에 나타난다(예: 123이 "321"로 나타남). 배열 전체를 역순으로 인쇄할 수 있지만, 이는 선행 0("00000...000123")이 있는 숫자를 표시하여 불쾌감을 줄 수 있으므로 이 구현은 공백으로 채워진 텍스트 변수에 표현을 만들고 이를 인쇄한다. 처음 몇 가지 결과(5자리마다 공백을 추가하고 주석을 달았다)는 다음과 같다.
이 구현은 컴퓨터에 내장된 연산을 더 효율적으로 사용할 수 있다. 간단한 확장은 기수를 100으로 사용하는 것(출력 번역 과정에서 해당 변경 사항 적용)이거나, 충분히 넓은 컴퓨터 변수(예: 32비트 정수)가 있다면 10,000과 같은 더 큰 기수를 사용할 수 있다. 컴퓨터의 내장 정수 연산에 가까운 2의 거듭제곱 기수에서 작업하는 것이 유리하지만, 출력을 위한 십진법으로의 변환은 더 어려워진다. 일반적인 최신 컴퓨터에서는 덧셈과 곱셈이 피연산자의 값과 무관하게(피연산자가 단일 기계어 단어에 들어맞는 한) 일정한 시간이 걸리므로, 자릿수 배열의 각 요소에 가능한 한 많은 큰 숫자를 패킹하는 데 큰 이점이 있다. 컴퓨터는 또한 예제와 같이 나머지 연산과 나눗셈 연산을 두 번 수행할 필요 없이 곱셈 결과를 자릿수와 올림수로 분리하는 기능을 제공할 수 있으며, 거의 모든 산술 장치는 다중 정밀도 덧셈 및 뺄셈에 활용될 수 있는 올림수 플래그를 제공한다. 이러한 세부 사항은 기계어 코드 프로그래머의 주된 관심사이며, 적절한 어셈블리 언어 큰 숫자 루틴은 이러한 기능에 직접 접근할 수 없고 고수준 문장을 최적화 컴파일러를 사용하여 대상 기계의 모델에 매핑하는 고수준 언어 컴파일 결과보다 빠르게 실행될 수 있다.
한 자릿수 곱셈의 경우 작업 변수는 (기수−1) + 올림수 값을 담을 수 있어야 하며, 여기서 올림수의 최대값은 (기수−1)이다. 마찬가지로, 자릿수 배열을 인덱싱하는 데 사용되는 변수 자체도 너비가 제한된다. 인덱스를 확장하는 간단한 방법은 큰 숫자의 자릿수를 편리한 크기의 블록으로 처리하여 주소 지정이 (블록 i, 자릿수 j)와 같이 이루어지도록 하는 것이다. 여기서 i와 j는 작은 정수이거나, 인덱싱 변수에 큰 숫자 기술을 적용할 수도 있다. 궁극적으로, 기계 저장 용량과 실행 시간은 문제 크기에 제약을 가한다.
IBM의 최초 비즈니스 컴퓨터인 1950년대 중반의 진공관 기계인 IBM 702는 1자리에서 511자리까지 모든 길이의 자릿수 문자열에 대해 정수 연산을 완전히 하드웨어로 구현했다. 임의 정밀도 연산의 가장 초기에 널리 사용된 소프트웨어 구현은 아마도 맥리스프에 있었을 것이다. 이후 1980년경, VAX/VMS 및 VM/CMS 운영체제는 한 경우에는 문자열 함수 모음으로, 다른 경우에는 EXEC 2 및 REXX 언어로 큰 수 기능을 제공했다.
초기 널리 퍼진 구현은 1959년부터 1970년까지의 IBM 1620을 통해 가능했다. 1620은 이산 트랜지스터를 사용한 십진 숫자 기계였지만, 두 자리부터 사용 가능한 메모리만큼의 길이까지의 자릿수 문자열에 대해 정수 연산을 수행하는 하드웨어(순람표 사용)를 가지고 있었다. 부동 소수점 연산의 경우, 가수부는 100자리 이하로 제한되었고, 지수부는 두 자리로만 제한되었다. 공급된 가장 큰 메모리는 60,000자리를 제공했지만, 1620용 포트란 컴파일러는 기본값이 만족스럽지 않은 경우 제어 카드에서 지정할 수 있었지만 10자리와 같은 고정된 크기를 사용했다.
소프트웨어 라이브러리.
대부분의 컴퓨터 소프트웨어에서 임의 정밀도 연산은 요청된 정밀도로 숫자를 저장하고 계산을 수행하는 자료형 및 서브루틴을 제공하는 외부 라이브러리를 호출하여 구현된다.
다양한 라이브러리는 임의 정밀도 숫자를 나타내는 방식이 다르며, 일부 라이브러리는 정수 숫자만 사용하고, 다른 라이브러리는 다양한 기수(10진수 또는 2진수 거듭제곱)로 부동소수점 숫자를 저장한다. 일부 라이브러리는 숫자를 단일 값으로 표현하는 대신 분자/분모 쌍(유리수)으로 저장하며, 일부는 계산 가능한 수를 완전히 표현할 수 있지만, 이는 저장 한도까지이다. 근본적으로 튜링 기계는 모든 실수를 표현할 수 없다. formula_2의 크기가 formula_3의 크기를 초과하기 때문이다.
컴퓨팅에서 미니플로트(minifloat)는 매우 적은 비트로 표현되는 부동소수점 값이다. 이렇게 정밀도가 줄어들면 범용 수치 계산에는 적합하지 않지만, 다음과 같은 특수 목적에 유용하다.
또한, 부동소수점 및 IEEE 754 숫자의 속성과 구조를 시연하기 위해 컴퓨터 과학 과정에서 교육 도구로 자주 사용된다.
맥락에 따라 미니플로트는 32비트 미만, 16비트 이하 또는 16비트 미만의 모든 크기를 의미할 수 있다. 마이크로플로트라는 용어는 8비트 이하의 모든 크기를 의미할 수 있다.
이 페이지는 미니플로트를 설명하기 위해 () 표기법을 사용한다.
미니플로트는 IEEE 754 표준의 원칙을 따라 설계할 수 있다. 거의 모든 미니플로트는 비정규수와 정규수에 가장 작은 지수를 사용한다. 많은 미니플로트는 무한과 NaN에 가장 큰 지수를 사용하며, 이는 (특수 지수) 로 표시된다. 일부 미니플로트는 이 지수 값을 정상적으로 사용하며, 이 경우 이다.
지수 편향 이다. 이 값은 모든 표현 가능한 숫자가 표현 가능한 역수를 갖도록 보장한다.
이 표기법은 () 형식으로 와 같이 변환할 수 있다.
라데온 R300 및 R420 GPU는 "fp24" 부동소수점 형식 (1.7.16)을 사용했다. Direct3D 9.0의 "전체 정밀도"는 독점적인 24비트 부동소수점 형식이다. 마이크로소프트의 D3D9(셰이더 모델 2.0) 그래픽 API는 초기에 FP24(ATI의 R300 칩과 유사)와 FP32(엔비디아의 NV30 칩과 유사)를 "전체 정밀도"로 지원했으며, FP16은 그래픽 하드웨어에서 수행되는 정점 및 픽셀 셰이더 계산을 위한 "부분 정밀도"로 지원했다.
미니플로트는 또한 부동소수점을 소프트웨어에서 에뮬레이션해야 하는 마이크로컨트롤러와 같은 임베디드 장치에서도 일반적으로 사용된다. 계산 속도를 높이기 위해 가수는 일반적으로 비트의 정확히 절반을 차지하므로 레지스터 경계가 시프트 없이 부분을 자동으로 주소 지정한다(예: 4비트 장치에서 (1.3.4)).
bfloat16 (1.8.7) 형식은 단정밀도 숫자의 처음 16비트이며, 다른 형식에 대한 하드웨어 지원이 추가되기 전에 이미지 처리 및 기계 학습에서 자주 사용되었다.
IEEE 754-2008 개정판에는 "반정밀도"라고 불리는 16비트 (1.5.10) 부동소수점(32비트 단정밀도 및 64비트 배정밀도와 반대)이 포함되어 있다.
2016년에 크로노스는 불칸에서 사용할 10비트 (0.5.5) 및 11비트 (0.5.6) 부호 없는 형식을 정의했다. 이 형식은 부호 및 후미 숫자를 잘라내어 양수 반정밀도에서 변환할 수 있다.
2022년에 엔비디아와 다른 회사들은 "fp8" 형식 (1.5.2)에 대한 지원을 발표했다. 이 형식은 후미 숫자를 잘라내어 반정밀도에서 변환할 수 있다.
2023년부터 IEEE SA 워킹 그룹 P3109는 기계 학습에 최적화된 8비트 미니플로트 표준을 작업하고 있다. 현재 초안은 단일 형식이 아닌 "binary8pP"라는 7가지 다른 형식의 패밀리를 정의하며, 여기서 "P"는 1부터 7까지의 숫자이고 비트 패턴은 (1.8-P.P-1)이다. 이 형식은 또한 을 가지며 가장 큰 값을 무한대로 사용하고 음수 0의 패턴을 NaN으로 사용한다.
또한 2023년부터 4비트 (1.2.1) 부동소수점 숫자(네 가지 특수 IEEE 값 없음)는 대형 언어 모델의 가속화에 사용되기 시작했다.
8비트 (1.4.3).
여기서는 1비트 부호, 4비트 지수, 3비트 가수 (1.4.3)를 가진 1바이트(8비트) 미니플로트를 시연한다. 지수 편향은 다른 IEEE 754 부동소수점과 일치하도록 값을 1 중심으로 설정하기 위해 7로 정의된다. 따라서 (대부분의 값에 대해) 지수 의 실제 승수는 이다. 모든 IEEE 754 원칙이 유효해야 한다. 이 형식은 명령어에 매우 흔하게 사용된다.
0은 지수가 0이고 가수가 0인 것으로 표현된다. 지수가 0이라는 것은 0이 선행 "0." 접두사를 가진 비정규수이며, 가수가 0이면 소수점 이하의 모든 비트가 0이므로 이 값은 formula_1으로 해석된다. 부동소수점 숫자는 부호 있는 0을 사용하므로 formula_2도 사용할 수 있으며 양수 formula_3과 같다.
0 0000 000 = 0
1 0000 000 = −0
가장 낮은 지수의 경우 가수는 "0."으로 확장되고 지수 값은 가장 작은 정규화된 숫자처럼 1 더 높은 것으로 처리된다.
0 0000 001 = 0.0012 × 21 - 7 = 0.125 × 2−6 = 0.001953125 (가장 작은 비정규수)
0 0000 111 = 0.1112 × 21 - 7 = 0.875 × 2−6 = 0.013671875 (가장 큰 비정규수)
다른 모든 지수의 경우 가수는 "1."로 확장된다.
0 0001 000 = 1.0002 × 21 - 7 = 1 × 2−6 = 0.015625 (가장 작은 정규화된 숫자)
0 0001 001 = 1.0012 × 21 - 7 = 1.125 × 2−6 = 0.017578125
0 0111 000 = 1.0002 × 27 - 7 = 1 × 20 = 1
0 0111 001 = 1.0012 × 27 - 7 = 1.125 × 20 = 1.125 (1보다 큰 가장 작은 값)
0 1110 000 = 1.0002 × 214 - 7 = 1.000 × 27 = 128
0 1110 001 = 1.0012 × 214 - 7 = 1.125 × 27 = 144
0 1110 110 = 1.1102 × 214 - 7 = 1.750 × 27 = 224
0 1110 111 = 1.1112 × 214 - 7 = 1.875 × 27 = 240 (가장 큰 정규화된 숫자)
무한 값은 가수가 0으로 설정된 가장 높은 지수를 갖는다. 부호 비트는 양수 또는 음수가 될 수 있다.
0 1111 000 = +무한
1 1111 000 = −무한
NaN 값은 가장 높은 지수를 가지며, 가수는 0이 아니다.
s 1111 mmm = NaN (mmm ≠ 000인 경우)
이것은 이 예시 8비트 부동소수점의 가능한 모든 값에 대한 차트이다.
NaN이 아닌 값은 242개밖에 없다( +0과 −0을 다른 것으로 간주할 경우). 14개의 비트 패턴이 NaN을 나타내기 때문이다.
8비트 (1.4.3) (B = −2).
이러한 작은 크기에서는 다른 편향 값이 흥미로울 수 있다. 예를 들어, 편향이 −2이면 숫자 0-16이 정수 0-16과 동일한 비트 표현을 갖게 되지만, 정수가 아닌 값은 표현할 수 없다는 손실이 발생한다.
0 0000 000 = 0.0002 × 21 - (-2) = 0.0 × 23 = 0 (비정규수)
0 0000 001 = 0.0012 × 21 - (-2) = 0.125 × 23 = 1 (비정규수)
0 0000 111 = 0.1112 × 21 - (-2) = 0.875 × 23 = 7 (비정규수)
0 0001 000 = 1.0002 × 21 - (-2) = 1.000 × 23 = 8 (정규수)
0 0001 111 = 1.1112 × 21 - (-2) = 1.875 × 23 = 15 (정규수)
0 0010 000 = 1.0002 × 22 - (-2) = 1.000 × 24 = 16 (정규수)
8비트 (1.3.4).
모든 비트 할당이 가능하다. 더 적은 정밀도로 더 많은 동적 범위를 필요로 하는 경우 지수에 더 많은 비트를 할당하거나, 더 적은 동적 범위로 더 많은 정밀도를 필요로 하는 경우 가수에 더 많은 비트를 할당할 수 있다. 극단적으로는 모든 비트를 지수에 할당하거나(1.7.0), 한 비트를 제외한 모든 비트를 가수에 할당하여(1.1.6) 지수에 한 비트만 남길 수 있다. 지수에는 최소한 한 비트가 주어져야 한다. 그렇지 않으면 더 이상 부동소수점으로 의미가 없으며, 단지 부호 있는 숫자가 된다.
다음은 (1.3.4)에 대한 모든 가능한 값의 차트이다. 는 전체 범위에 걸쳐 정밀도가 최소한 0.5를 유지하도록 보장한다.
위와 같은 표는 스크립트를 사용하여 모든 SEMB(부호, 지수, 가수/유효 숫자, 편향) 값 조합에 대해 생성할 수 있다. 파이썬 또는 GDScript.
6비트 (1.3.2).
64개의 값만으로는 모든 값을 다이어그램으로 나타낼 수 있어 유용하다.
이 그래픽은 IEEE 754의 규칙을 정확히 따르는 두 개의 6비트 (1.3.2) 미니플로트의 수학을 보여준다. 녹색 X는 NaN 결과, 청록색 X는 +무한 결과, 자홍색 X는 −무한 결과이다. 유한 결과의 범위는 같은 값을 연결하는 곡선으로 채워져 있으며, 양수는 파란색, 음수는 빨간색이다.
4비트 (1.2.1).
정규화된 숫자, 비정규수, 부호 있는 0, 부호 있는 무한대, 여러 NaN 값을 포함하여 모든 IEEE 원칙을 따르는 가장 작은 부동소수점 크기는 1비트 부호, 2비트 지수, 1비트 가수를 가진 4비트 부동소수점이다.
3비트 (1.1.1).
정규화된 숫자가 필요하지 않은 경우, 지수를 1로 줄여 크기를 3비트로 줄일 수 있다.
2비트 (0.2.1) 및 (0.1.1).
부호 비트를 제외할 수 있는 상황에서는 위 예시 각각을 1비트 더 줄여 위 표의 첫 번째 행만 유지할 수 있다. 1비트 지수와 1비트 가수를 가진 2비트 부동소수점은 0, 1, Inf, NaN 값만 가질 것이다.
1비트 (0.1.0).
가수를 제거하면 0과 Inf 두 가지 값만 허용된다. 지수를 제거하는 것은 작동하지 않는다. 위 공식은 0과 sqrt(2)/2를 생성한다. 지수는 최소 1비트여야 한다. 그렇지 않으면 더 이상 부동소수점으로 의미가 없어진다(단지 부호 있는 숫자가 될 뿐).
bfloat16(brain floating point) 부동소수점 형식은 주기억장치에서 16비트를 차지하는 컴퓨터 숫자 형식이다. 이는 부동 소수점(floating radix point)을 사용하여 넓은 동적 범위의 숫자 값을 나타낸다. 이 형식은 기계 학습 및 니어 센서 컴퓨팅의 가속화를 목표로 하는 32비트 IEEE 754 단정밀도 부동소수점 형식(binary32)의 단축(16비트) 버전이다. 8개의 지수 비트를 유지함으로써 32비트 부동소수점 숫자의 대략적인 동적 범위를 보존하지만, binary32 형식의 24비트 유효숫자 대신 8비트 정밀도만을 지원한다. 단정밀도 32비트 부동소수점 숫자보다 bfloat16 숫자는 정수 계산에는 부적합하지만, 이는 의도된 용도가 아니다. bfloat16은 기계 학습 알고리즘의 저장 요구 사항을 줄이고 계산 속도를 높이는 데 사용된다.
bfloat16 형식은 구글의 인공지능 연구 그룹인 구글 브레인에서 개발되었다. 이는 인텔 제온 프로세서(AVX-512 BF16 확장), 인텔 데이터 센터 GPU, 인텔 너바나 NNP-L1000, 인텔 FPGA, AMD 젠, AMD 인스팅트, 엔비디아 GPU, 구글 클라우드 TPU, AWS 인퍼렌티아, AWS 트레이니움, ARMv8.6-A, 애플의 M2 및 이후 A15 칩 등 다양한 CPU, GPU, AI 프로세서에서 활용된다. CUDA, 인텔 oneAPI Math Kernel Library, AMD ROCm, AMD 최적화 CPU 라이브러리, PyTorch, 텐서플로 등 여러 라이브러리가 bfloat16을 지원한다. 이러한 플랫폼에서 bfloat16은 혼합 정밀도 연산에서도 사용될 수 있으며, 이때 bfloat16 숫자는 더 넓은 자료형으로 연산되고 확장될 수 있다.
bfloat16 부동소수점 형식.
bfloat16은 다음 형식을 가진다.
bfloat16 형식은 단축된 IEEE 754 단정밀도 32비트 부동소수점 형식이므로 IEEE 754 단정밀도 32비트 부동소수점 형식으로의 형 변환 및 그 반대 변환이 빠르다. bfloat16 형식으로 변환할 때 지수 비트는 보존되는 반면, 유효숫자 필드는 절단(따라서 0으로 반올림에 해당) 또는 기타 반올림 메커니즘에 의해 축소될 수 있으며, NaN 특수 사례는 무시된다. 지수 비트를 보존함으로써 32비트 부동소수점의 범위인 약 10−38에서 약 3 × 1038이 유지된다.
비트는 다음과 같이 배열된다.
bfloat16 이진 부동소수점 지수는 오프셋 이진 표현을 사용하여 인코딩되며, 0 오프셋은 127이다. 이는 IEEE 754 표준에서 지수 편향으로도 알려져 있다.
따라서, 오프셋 이진 표현으로 정의된 실제 지수를 얻기 위해서는 지수 필드 값에서 127의 오프셋을 빼야 한다.
지수 필드의 최소 및 최대 값(00H 및 FFH)은 IEEE 754 표준 형식과 마찬가지로 특별하게 해석된다.
최소 양수 정규 값은 2−126 ≈ 1.18 × 10−38이고 최소 양수 (비정규) 값은 2−126−7 = 2−133 ≈ 9.2 × 10−41이다.
반올림 및 변환.
가장 일반적인 사용 사례는 IEEE 754 binary32와 bfloat16 사이의 변환이다. 다음 섹션에서는 변환 과정과 변환 시의 반올림 방식을 설명한다. bfloat16으로 또는 bfloat16에서 다른 형식으로의 변환 시나리오도 있을 수 있음을 참고한다. 예를 들어, int16과 bfloat16.
특수 값 인코딩.
양의 무한대와 음의 무한대.
IEEE 754에서와 마찬가지로, 양의 무한대와 음의 무한대는 해당 부호 비트와 8개의 지수 비트가 모두 설정(FFhex)되고 모든 유효숫자 비트가 0으로 표현된다. 명시적으로,
val s_exponent_signcnd
+inf = 0_11111111_0000000
-inf = 1_11111111_0000000
숫자가 아님.
IEEE 754에서와 마찬가지로, NaN 값은 부호 비트, 8개의 지수 비트가 모두 설정(FFhex)되고 모든 유효숫자 비트가 0이 아닌 경우로 표현된다. 명시적으로,
+NaN = 0_11111111_klmnopq
-NaN = 1_11111111_klmnopq
여기서 k, l, m, n, o, p, q 중 적어도 하나는 1이다. IEEE 754와 마찬가지로, NaN 값은 quiet 또는 signaling일 수 있지만, 2018년 9월 현재 signaling bfloat16 NaN의 알려진 사용 사례는 없다.
범위 및 정밀도.
Bfloat16은 32비트 IEEE 754 단정밀도 부동소수점 형식(binary32)의 숫자 범위를 유지하면서 정밀도를 24비트에서 8비트로 줄이도록 설계되었다. 이는 정밀도가 2에서 3십진수 자릿수 사이이며, bfloat16은 최대 약 3.4 × 1038의 유한 값을 표현할 수 있음을 의미한다.
이 예시들은 부동소수점 값의 비트 표현을 십육진법과 이진법으로 보여준다. 여기에는 부호, (편향된) 지수, 유효숫자가 포함된다.
3f80 = 0 01111111 0000000 = 1
c000 = 1 10000000 0000000 = −2
7f7f = 0 11111110 1111111 = (28 − 1) × 2−7 × 2127 ≈ 3.38953139 × 1038 (bfloat16 정밀도에서 최대 유한 양수 값)
0080 = 0 00000001 0000000 = 2−126 ≈ 1.175494351 × 10−38 (bfloat16 정밀도 및 단정밀도 부동소수점에서 최소 정규 양수 값)
일반 bfloat16 숫자의 최대 양의 유한 값은 3.38953139 × 1038이며, 단정밀도에서 표현 가능한 최대 양의 유한 값인 (224 − 1) × 2−23 × 2127 = 3.402823466 × 1038보다 약간 낮다.
영과 무한대.
0000 = 0 00000000 0000000 = 0
8000 = 1 00000000 0000000 = −0
7f80 = 0 11111111 0000000 = 무한대
ff80 = 1 11111111 0000000 = −무한대
4049 = 0 10000000 1001001 = 3.140625 ≈ π ( 파이 )
3eab = 0 01111101 0101011 = 0.333984375 ≈ 1/3
NaNs.
ffc1 = x 11111111 1000001 =&gt; qNaN
ff81 = x 11111111 0000001 =&gt; sNaN
구마노군()은 일본 교토부(단고국)에 있던 군이다.
1879년 행정 구역으로 발족 당시의 군역은 교탄고시의 일부에 해당한다.
직관주의 유형 이론(Intuitionistic type theory, 直觀主義類型理論), 직관주의 유형론, 구성주의 유형 이론 또는 마르틴뢰프 유형 이론(Martin-Löf type theory, MLTT)은 유형 이론이자 대안적인 수학의 기초이다. 직관주의 유형 이론은 스웨덴의 수학자이자 철학자인 페르 마르틴뢰프(Per Martin-Löf)가 만들었으며, 1972년에 처음 출판되었다. 이 유형 이론에는 여러 버전이 있는데, 마르틴뢰프는 이론의 내포적(intensional) 및 외연적(extensional) 변형과 초기의 비가술적(非可述的, impredicative) 버전을 모두 제안했지만, 지라르의 역설(Girard's paradox)로 인해 모순이 있는 것으로 나타나 가술적(predicative) 버전으로 대체되었다. 그러나 모든 버전은 의존형을 사용하는 구성주의 논리의 핵심 설계를 유지한다.
마르틴뢰프는 수학적 구성주의의 원리에 따라 유형 이론을 설계했다. 구성주의는 모든 존재 증명이 "증거"를 포함해야 한다고 요구한다. 따라서 "1000보다 큰 소수가 존재한다"는 증명은 소수이면서 1000보다 큰 특정 숫자를 식별해야 한다. 직관주의 유형 이론은 BHK 해석을 내면화함으로써 이러한 설계 목표를 달성했다. 유용한 결과는 증명이 검사, 비교 및 조작될 수 있는 수학적 객체가 된다는 것이다.
직관주의 유형 이론의 유형 생성자는 논리적 연결사와 일대일 대응을 따르도록 구축되었다. 예를 들어, 함의(formula_1)라는 논리적 연결사는 함수의 유형(formula_2)에 해당한다. 이 대응을 커리-하워드 동형이라고 한다. 이전 유형 이론도 이 동형을 따랐지만, 마르틴뢰프의 이론은 의존형을 도입하여 술어 논리로 확장한 최초의 이론이었다.
유형 이론은 존재하는 근본적인 객체를 기술하는 수학적 존재론 또는 기초론의 일종이다. 표준 기초론인 집합론과 수리 논리학의 결합에서, 근본적인 객체는 원소를 포함하는 컨테이너인 집합이다. 유형 이론에서 근본적인 객체는 항(term)이며, 각 항은 오직 하나의 유형(type)에 속한다.
직관주의 유형 이론은 세 가지 유한 유형(finite type)을 가지며, 이들은 다섯 가지 다른 유형 생성자를 사용하여 구성된다. 집합론과는 달리, 유형 이론은 프레게의 논리처럼 논리 위에 구축되지 않는다. 따라서 유형 이론의 각 기능은 수학과 논리 모두의 기능으로 두 가지 역할을 한다.
0 유형, 1 유형 및 2 유형.
세 가지 유한 유형이 있다. 0 유형은 항을 포함하지 않는다. 1 유형은 하나의 기초 항(canonical term)을 포함한다. 2 유형은 두 개의 기초 항을 포함한다.
0 유형은 항을 포함하지 않으므로 공 유형이라고도 불린다. 존재할 수 없는 모든 것을 나타내는 데 사용된다. 또한 formula_3으로도 쓰이며 증명 불가능한 모든 것(즉, 그것의 증명이 존재할 수 없음)을 나타낸다. 결과적으로 부정은 그것에 대한 함수로 정의된다. formula_4.
마찬가지로, 1 유형은 하나의 기초 항을 포함하며 존재를 나타낸다. 또한 단위 유형이라고도 불린다.
마지막으로, 2 유형은 두 개의 기초 항을 포함한다. 이것은 두 값 사이의 명확한 선택을 나타낸다. 불 값에 사용되지만 명제에는 사용되지 않는다.
명제는 대신 특정 유형으로 표현된다. 예를 들어, 참 명제는 1 유형으로 표현될 수 있고, 거짓 명제는 0 유형으로 표현될 수 있다. 그러나 이것들이 유일한 명제라고 단언할 수는 없으며, 즉 직관주의 유형 이론에서 명제에 대해 배중률은 성립하지 않는다.
Σ 유형 생성자.
Σ-유형은 순서쌍을 포함한다. 일반적인 순서쌍(또는 2-튜플) 유형과 마찬가지로, Σ-유형은 두 다른 유형 formula_5와 formula_6의 카르테시안 곱, formula_7를 설명할 수 있다. 논리적으로, 그러한 순서쌍은 formula_5의 증명과 formula_6의 증명을 포함하므로, 그러한 유형은 formula_10로 쓰이는 것을 볼 수 있다.
Σ-유형은 의존적 유형화 때문에 일반적인 순서쌍 유형보다 더 강력하다. 순서쌍에서 두 번째 항의 유형은 첫 번째 항의 값에 따라 달라질 수 있다. 예를 들어, 쌍의 첫 번째 항이 자연수이고 두 번째 항의 유형이 첫 번째 항의 길이와 같은 실수의 수열일 수 있다. 그러한 유형은 다음과 같이 쓰일 것이다.
집합론 용어를 사용하면, 이것은 집합의 인덱스화된 분리합집합과 유사하다. 일반적인 카르테시안 곱의 경우, 두 번째 항의 유형은 첫 번째 항의 값에 따라 달라지지 않는다. 따라서 카르테시안 곱 formula_12을 설명하는 유형은 다음과 같이 쓰인다.
여기서 첫 번째 항의 값인 formula_14은 두 번째 항의 유형인 formula_15에 의존하지 않는다는 점에 유의해야 한다.
Σ-유형은 수학에서 사용되는 더 긴 의존적 튜플과 대부분의 프로그래밍 언어에서 사용되는 레코드 또는 구조체를 구성하는 데 사용될 수 있다. 의존적 3-튜플의 예로는 두 정수와 첫 번째 정수가 두 번째 정수보다 작다는 증명이 있으며, 이는 다음 유형으로 설명된다.
의존적 유형화는 Σ-유형이 존재 양화사의 역할을 수행하도록 허용한다. "유형 formula_17의 formula_14이 존재하고, formula_19이 증명된다"는 문장은 첫 번째 항목이 유형 formula_17의 값 formula_14이고 두 번째 항목이 formula_19의 증명인 순서쌍의 유형이 된다. 두 번째 항목(formula_19의 증명)의 유형이 순서쌍의 첫 번째 부분(formula_14)의 값에 의존한다는 점에 주목하라. 그 유형은 다음과 같을 것이다.
Π 유형 생성자.
Π-유형은 함수를 포함한다. 일반적인 함수 유형과 마찬가지로, 입력 유형과 출력 유형으로 구성된다. 그러나 반환 유형이 입력 값에 따라 달라질 수 있다는 점에서 일반적인 함수 유형보다 더 강력하다. 유형 이론의 함수는 집합론과 다르다. 집합론에서는 순서쌍 집합에서 인수의 값을 찾는다. 유형 이론에서는 인수가 항에 대입된 다음, 항에 대한 계산("환원")이 적용된다.
예를 들어, 자연수 formula_14이 주어지면 formula_14개의 실수를 포함하는 벡터를 반환하는 함수의 유형은 다음과 같이 쓰인다.
출력 유형이 입력 값에 의존하지 않을 때, 함수 유형은 종종 단순히 formula_29로 쓰인다. 따라서 formula_30은 자연수에서 실수로 가는 함수의 유형이다. 이러한 Π-유형은 논리적 함의에 해당한다. 논리적 명제 formula_1는 formula_5의 증명을 받아 formula_6의 증명을 반환하는 함수를 포함하는 유형 formula_2에 해당한다. 이 유형은 다음과 같이 더 일관성 있게 쓸 수 있다.
Π-유형은 또한 보편 양화를 위한 논리에도 사용된다. "모든 유형 formula_17의 formula_14에 대해 formula_19이 증명된다"는 문장은 유형 formula_17의 formula_14에서 formula_19의 증명으로 가는 함수가 된다. 따라서 formula_14에 대한 값이 주어지면 함수는 해당 값에 대해 formula_43가 성립한다는 증명을 생성한다. 이 유형은 다음과 같을 것이다.
= 유형 생성자.
=-유형은 두 개의 항으로부터 생성된다. formula_45와 formula_46와 같은 두 항이 주어지면, 새로운 유형 formula_47를 생성할 수 있다. 그 새로운 유형의 항들은 그 쌍이 동일한 기초 항으로 축소된다는 증명을 나타낸다. 따라서 formula_45와 formula_49 모두 기초 항 formula_50로 계산되므로, 유형 formula_47의 항이 존재할 것이다. 직관주의 유형 이론에서는 =-유형을 도입하는 단일한 방법이 있으며, 그것은 반사성에 의한 것이다.
항이 동일한 기초 항으로 축소되지 않는 formula_53와 같은 =-유형을 생성하는 것이 가능하지만, 그 새로운 유형의 항을 생성할 수는 없다. 사실, 만약 formula_53의 항을 생성할 수 있었다면, formula_3의 항을 생성할 수 있었을 것이다. 그것을 함수에 넣으면 formula_56 유형의 함수가 생성될 것이다. formula_57는 직관주의 유형 이론이 부정을 정의하는 방식이므로, formula_58 또는 최종적으로 formula_59를 가질 것이다.
증명의 등식은 증명 이론에서 활발히 연구되는 분야이며 호모토피 유형 이론 및 다른 유형 이론의 발전을 이끌었다.
귀납 유형.
귀납 유형은 복잡한 자기 참조 유형을 생성할 수 있도록 한다. 예를 들어, 자연수의 연결 리스트는 빈 리스트이거나 자연수와 또 다른 연결 리스트의 쌍이다. 귀납 유형은 나무, 그래프 등과 같은 무한 수학적 구조를 정의하는 데 사용될 수 있다. 사실, 자연수 유형은 귀납 유형으로 정의될 수 있는데, 이는 formula_60이거나 다른 자연수의 다음수이다.
귀납 유형은 formula_61와 같은 새로운 상수와 다음수 함수 formula_62를 정의한다. formula_63는 정의를 가지고 있지 않고 대체(substitution)를 사용하여 평가될 수 없으므로, formula_64와 formula_65와 같은 항은 자연수의 기초 항이 된다.
귀납 유형에 대한 증명은 귀납법을 통해 가능하다. 각 새로운 귀납 유형은 고유한 귀납 규칙과 함께 제공된다. 모든 자연수에 대해 술어 formula_43를 증명하려면 다음 규칙을 사용한다.
직관주의 유형 이론의 귀납 유형은 잘 정돈된 트리의 유형인 W-유형으로 정의된다. 유형 이론의 후속 연구는 보다 모호한 종류의 자기 참조성을 가진 유형에 대한 코귀납 유형, 귀납-재귀 및 귀납-귀납을 생성했다. 고차 귀납 유형은 항 간의 등식을 정의할 수 있도록 한다.
전체 유형.
전체 유형은 다른 유형 생성자로 생성된 모든 유형에 대한 증명을 작성할 수 있도록 한다. 전체 유형 formula_68의 모든 항은 formula_69 및 귀납 유형 생성자의 모든 조합으로 생성된 유형에 매핑될 수 있다. 그러나 역설을 피하기 위해, 어떤 formula_70에 대해서도 formula_71에 formula_71으로 매핑되는 항은 없다.
모든 "작은 유형"과 formula_68에 대한 증명을 작성하려면 formula_74을 사용해야 한다. 이 유형은 formula_68에 대한 항을 포함하지만, 자체 formula_74에 대한 항은 포함하지 않는다. 마찬가지로, formula_77도 그렇다. 예측적 계층의 전체가 존재하므로, 고정된 상수 formula_78 전체에 대한 증명을 정량화하려면 formula_79을 사용할 수 있다.
전체 유형은 유형 이론의 까다로운 기능이다. 마르틴뢰프의 원래 유형 이론은 지라르의 역설을 설명하기 위해 변경되어야 했다. 후속 연구는 "초 전체", "말로 전체" 및 비예측적 전체와 같은 주제를 다루었다.
직관주의 유형 이론의 형식적 정의는 판단을 사용하여 작성된다. 예를 들어, "만약 formula_5가 유형이고 formula_6가 유형이면 formula_82는 유형이다"라는 문장에는 "는 유형이다", "그리고", "만약...이면..."이라는 판단이 있다. 표현 formula_82는 판단이 아니다; 그것은 정의되는 유형이다.
유형 이론의 이 두 번째 수준은 특히 등식(equality)과 관련하여 혼란스러울 수 있다. 항 등식에 대한 판단이 있을 수 있는데, 예를 들어 formula_84가 있다. 이것은 두 항이 동일한 기초 항으로 축소된다는 진술이다. 유형 등식에 대한 판단도 있으며, 예를 들어 formula_85라고 말하면, formula_5의 모든 요소가 유형 formula_6의 요소이며 그 반대도 마찬가지라는 의미이다. 유형 수준에서는 유형 formula_84가 있으며, formula_50와 formula_45가 동일한 값으로 축소된다는 증명이 있다면 이 유형에는 항이 포함된다. (이 유형의 항은 항 등식 판단을 사용하여 생성된다.) 마지막으로, 자연언어(영어) 수준의 등식이 있는데, 이는 우리가 "four"라는 단어와 "formula_50"라는 기호를 사용하여 기초 항 formula_92를 참조하기 때문이다. 이러한 동의어는 마르틴뢰프에 의해 "정의적으로 동일하다"고 불린다.
아래 판단에 대한 설명은 노르드스트롬, 페테르손, 스미스의 논의를 기반으로 한다.
형식 이론은 유형과 객체를 다룬다.
유형은 다음과 같이 선언된다.
객체가 존재하며 유형에 속하는 경우는 다음과 같다.
객체는 같을 수 있다.
그리고 유형은 같을 수 있다.
다른 유형의 객체에 의존하는 유형은 다음과 같이 선언된다.
그리고 대입으로 제거된다.
다른 유형의 객체에 의존하는 객체는 두 가지 방법으로 수행될 수 있다.
객체가 "추상화"된 경우, 다음과 같이 쓰인다.
객체에 의존하는 객체는 재귀 유형의 일부로 상수로 선언될 수도 있다. 재귀 유형의 예는 다음과 같다.
여기서 formula_63는 상수 객체 의존 객체이다. 추상화와 관련이 없다. formula_63와 같은 상수는 등식을 정의하여 제거할 수 있다. 여기서 덧셈과의 관계는 등식과 formula_63의 재귀적 측면을 처리하기 위한 패턴 매칭을 사용하여 정의된다.
formula_63는 불투명한 상수로 조작된다. 즉, 대체할 내부 구조가 없다.
따라서 객체와 유형, 그리고 이러한 관계는 이론에서 공식을 표현하는 데 사용된다. 다음 스타일의 판단은 기존 객체, 유형 및 관계에서 새로운 객체, 유형 및 관계를 생성하는 데 사용된다.
관례상, 다른 모든 유형을 나타내는 유형이 있다. 이를 formula_114(또는 formula_115)라고 한다. formula_114는 유형이므로, 그 구성원들은 객체이다. 각 객체를 해당 유형에 매핑하는 의존 유형 formula_117이 있다. 대부분의 텍스트에서는 formula_117이 작성되지 않는다. 진술의 문맥상 독자는 formula_5가 유형을 나타내는지, 아니면 유형에 해당하는 formula_114의 객체를 나타내는지를 거의 항상 알 수 있다.
이것이 이론의 완전한 기초이다. 다른 모든 것은 파생된다.
논리를 구현하기 위해 각 명제는 고유한 유형을 갖는다. 해당 유형의 객체는 명제를 증명하는 다양한 가능한 방법을 나타낸다. 명제에 대한 증명이 없으면 해당 유형에는 객체가 없다. 명제에 작용하는 "그리고" 및 "또는"과 같은 연산자는 새로운 유형과 새로운 객체를 도입한다. 따라서 formula_121는 유형 formula_5와 유형 formula_6에 의존하는 유형이다. 해당 의존 유형의 객체는 formula_5와 formula_6의 모든 객체 쌍에 대해 존재하도록 정의된다. formula_5 또는 formula_6 중 하나가 증명이 없고 빈 유형이면 formula_128를 나타내는 새 유형도 비어 있다.
이것은 다른 유형(부울, 자연수 등) 및 해당 연산자에 대해서도 수행될 수 있다.
유형 이론의 범주적 모형.
범주론의 언어를 사용하여 R. A. G. 실리는 유형 이론의 기본 모형으로 국소 카르테시안 닫힌 범주 (LCCC)의 개념을 도입했다. 이것은 호프만과 딥비르에 의해 카트멜의 이전 작업을 기반으로 패밀리가 있는 범주 또는 속성이 있는 범주로 정교화되었다.
패밀리가 있는 범주는 문맥의 범주 C(여기서 객체는 문맥이고, 문맥 사상은 대입이다)와, 반변함자 T : Cop → Fam(Set)으로 구성된다.
Fam(Set)은 집합의 패밀리 범주이며, 객체는 "인덱스 집합" A와 함수 B: X → A의 쌍 이고, 사상은 함수 f : A → A' 와 g : X → X' 의 쌍으로, B' ° g = f ° B를 만족한다. 즉, f는 Ba를 Bg(a)로 매핑한다.
함자 T는 문맥 G에 대해 유형 집합 를 할당하고, 각 에 대해 항 집합 를 할당한다. 함자에 대한 공리는 이들이 대입과 조화롭게 작동하도록 요구한다. 대입은 일반적으로 Af 또는 af 형태로 쓰며, 여기서 A는 의 유형이고 a는 의 항이며, f는 D에서 G로의 대입이다. 여기서 이고 이다.
범주 C는 종단 객체(빈 문맥)와, 오른쪽에 있는 원소가 왼쪽 원소의 문맥에 있는 유형인 포괄(comprehension) 또는 문맥 확장이라는 형태의 곱에 대한 최종 객체를 포함해야 한다. G가 문맥이고 이면, 매핑 p : D → G, q : Tm(D,Ap)를 갖는 문맥 D 중에서 최종적인 객체 가 있어야 한다.
마르틴뢰프의 것과 같은 논리적 프레임워크는 문맥 의존적인 유형 및 항 집합에 대한 닫힘 조건의 형태를 취한다. 즉, Set이라는 유형이 있어야 하고, 각 Set에 대해 유형이 있어야 하며, 유형은 의존 합 및 곱의 형태와 다양한 형태의 귀납적 정의에 대해 닫혀 있어야 한다.
예측적 집합론과 같은 이론은 집합의 유형과 그 원소에 대한 닫힘 조건을 표현한다. 즉, 의존 합 및 곱을 반영하는 연산과 다양한 형태의 귀납적 정의에 대해 닫혀 있어야 한다.
외연적 대 내포적.
근본적인 구분은 외연적 유형 이론 대 내포적 유형 이론이다. 외연적 유형 이론에서는 정의적(즉, 계산적) 동등성과 증명을 필요로 하는 명제적 동등성이 구별되지 않는다. 결과적으로 유형 이론 내의 프로그램이 종료되지 않을 수 있으므로 외연적 유형 이론에서는 유형 검사가 결정 불가능해진다. 예를 들어, 이러한 이론은 Y 콤비네이터에 유형을 부여하는 것을 허용한다. 이에 대한 자세한 예시는 Nordstöm과 Petersson의 "Programming in Martin-Löf's Type Theory"에서 찾을 수 있다. 그러나 이것이 외연적 유형 이론이 실용적인 도구의 기반이 되는 것을 막지는 못한다. 예를 들어, 누프르 시스템은 계산 유형 이론에 기반을 두고 있다. 그리고 Coq는 귀납적 구성의 계산에 기반을 두고 있다.
반면, 내포적 유형 이론에서는 유형 검사가 결정 가능하지만, 표준 수학적 개념의 표현은 다소 번거롭다. 내포적 추론은 집합동치 또는 유사한 구성을 사용해야 하기 때문이다. 정수, 유리수, 실수와 같이 이 없이는 다루기 어렵거나 표현할 수 없는 공통 수학적 객체가 많이 있다. 정수와 유리수는 집합동치 없이도 표현할 수 있지만, 이러한 표현은 다루기 어렵다. 코시 실수는 이 없이는 표현할 수 없다.
호모토피 유형 이론은 이 문제를 해결하기 위해 노력한다. 이는 고차 귀납 유형을 정의할 수 있게 하는데, 이는 1차 생성자(값 또는 점)뿐만 아니라 고차 생성자, 즉 요소 간의 등식(경로), 등식 간의 등식(호모토피), 그리고 무한히 계속되는 등식을 정의한다.
유형 이론의 구현.
다양한 형태의 유형 이론이 여러 증명 보조기의 기반이 되는 형식 시스템으로 구현되었다. 많은 시스템이 페르 마르틴뢰프의 아이디어를 기반으로 하지만, 많은 시스템은 추가 기능, 더 많은 공리 또는 다른 철학적 배경을 가지고 있다. 예를 들어, 누프르 시스템은 계산 유형 이론(computational type theory)에 기반을 두고 있으며 Coq는 (공)귀납적 구성의 계산에 기반을 두고 있다. 의존형은 또한 ATS, 카옌, 에피그램, 아그다, 및 아이드리스와 같은 프로그래밍 언어의 설계에도 특징적으로 나타난다.
마르틴뢰프 유형 이론.
페르 마르틴뢰프는 여러 유형 이론을 구축하여 다양한 시기에 발표했는데, 일부는 그의 설명이 담긴 사전 인쇄물이 전문가들(특히 장 이브 지라르와 조반니 삼빈)에게 공개된 시점보다 훨씬 늦게 발표되었다. 아래 목록은 인쇄된 형태로 설명된 모든 이론을 나열하고 서로를 구별하는 주요 특징을 간략하게 설명하려고 한다. 이 모든 이론은 종속 곱, 종속 합, 분리 합집합, 유한 유형 및 자연수를 가지고 있었다. 모든 이론은 종속 곱 또는 종속 합에 대한 η-환원을 포함하지 않는 동일한 환원 규칙을 가졌으며, 종속 곱에 대한 η-환원이 추가된 MLTT79는 예외였다.
MLTT71은 페르 마르틴뢰프가 만든 최초의 유형 이론이다. 1971년 사전 인쇄물로 등장했다. 하나의 전체를 가지고 있었지만, 이 전체는 그 자체로 이름을 가지고 있었다. 즉, 오늘날 "유형 안의 유형(Type in Type)"이라고 불리는 유형 이론이었다. 장 이브 지라르는 이 시스템이 불일치함을 보여주었고, 사전 인쇄물은 출판되지 않았다.
MLTT72는 1972년 현재 출판된 사전 인쇄물에서 발표되었다. 이 이론은 하나의 전체 V를 가지고 있었고 동일성 유형 (=-유형)은 없었다. 이 전체는 예측적이었는데, 이는 V에 있지 않은 객체(예를 들어 V 자체)에 대한 V의 객체들의 패밀리의 종속 곱이 V에 있다고 가정되지 않았다는 의미이다. 이 전체는 버트런드 러셀의 수학 원리와 유사했는데, 즉 "T∈V"와 "t∈T" (마르틴뢰프는 현대의 ":" 대신 "∈" 기호를 사용했다)를 추가적인 생성자 "El" 없이 직접 작성했을 것이다.
MLTT73은 페르 마르틴뢰프가 처음으로 출판한 유형 이론의 정의였다(1973년 논리 콜로퀴엄에서 발표되었고 1975년에 출판되었다). 그는 "명제"라고 설명하는 동일성 유형이 있지만, 명제와 다른 유형 간의 실제 구별이 도입되지 않았기 때문에 그 의미는 불분명하다. 나중에 J-소거자라는 이름을 얻게 되는 것이 있지만 아직 이름이 없다(pp. 94–95 참조). 이 이론에는 V0, ..., Vn, ...와 같은 무한한 전체 시퀀스가 있다. 이 전체는 예측적이고, 러셀 스타일이며, 누적되지 않는다. 사실, p. 115의 따름정리 3.10은 A∈Vm이고 B∈Vn이 A와 B가 변환 가능하면 m=n이라고 말한다.
MLTT79는 1979년에 발표되었고 1982년에 출판되었다. 이 논문에서 마르틴뢰프는 종속 유형 이론의 네 가지 기본 판단 유형을 도입했는데, 이는 그 이후 이러한 시스템의 메타 이론 연구에서 기본이 되었다. 그는 또한 컨텍스트를 별도의 개념으로 도입했다(p. 161 참조). J-소거자(MLTT73에도 나타났지만 그때는 이 이름이 없었다)를 가진 동일성 유형이 있었지만, 이론을 "외연적"으로 만드는 규칙도 있었다(p. 169). W-유형도 있었다. 누적되는 예측적 전체의 무한 시퀀스가 있었다.
비블리오폴리스(Bibliopolis): 1984년 비블리오폴리스 책에는 유형 이론에 대한 논의가 있지만, 다소 개방적이며 특정 선택 집합을 나타내는 것 같지 않으므로 그와 관련된 특정 유형 이론은 없다.
컴퓨터 과학에서 컨테이너(container)는 다른 객체들의 클래스 또는 자료 구조의 인스턴스이다. 즉, 특정 접근 규칙을 따르는 조직화된 방식으로 객체를 저장한다.
컨테이너의 크기는 컨테이너가 포함하는 객체(요소)의 수에 따라 달라진다. 다양한 컨테이너 유형의 하위(상속된) 구현은 크기, 복잡성 및 언어 유형에 따라 달라질 수 있지만, 많은 경우 주어진 시나리오에 맞는 올바른 구현을 선택할 수 있는 유연성을 제공한다.
컨테이너 자료 구조는 많은 종류의 프로그래밍 언어에서 흔히 사용된다.
기능 및 속성.
컨테이너는 다음 세 가지 속성으로 특징지을 수 있다.
컨테이너 클래스는 다음을 수행하기 위한 CRUD와 유사한 메서드를 구현할 것으로 예상된다.
컨테이너는 때때로 반복자와 함께 구현된다.
컨테이너는 단일 값 컨테이너 또는 연관 컨테이너로 분류될 수 있다.
단일 값 컨테이너는 각 객체를 독립적으로 저장한다. 객체는 직접, 언어 루프 구조(예: For 루프) 또는 반복자로 접근할 수 있다.
연관 컨테이너는 키-값 쌍으로 구성된 연관 배열, 맵 또는 딕셔너리를 사용하며, 각 키는 컨테이너에 최대 한 번 나타난다. 키는 컨테이너에 저장되어 있는 경우 값인 객체를 찾는 데 사용된다. 연관 컨테이너는 프로그래밍 언어에서 클래스 템플릿으로 사용된다.
컨테이너 추상 자료형은 다음을 포함한다.
이러한 추상 유형을 구현하는 데 사용되는 일반적인 자료 구조는 다음을 포함한다.
그래픽 컨테이너.
위젯 툴킷은 또한 창, 패널과 같은 다른 위젯을 그룹화하는 특수 위젯인 컨테이너를 사용한다. 그래픽 속성 외에도 컨테이너 클래스와 동일한 유형의 동작을 가지는데, 이는 자식 위젯 목록을 유지하고 자식 중에서 위젯을 추가, 제거 또는 검색할 수 있도록 하기 때문이다.