ARM 명령어를 난생 처음 작성하다가 잘 안되어 기본적인 내용을 정리해본다. 이 내용은 Structure of the ARM A64 instruction set 에서 가져왔다.

레지스터

A64 아키텍쳐는 30개의 정수 레지스터가 있으며 각각은 x0부터 x31까지의 이름을 갖는다.

여기에 스택포인터 레지스터와 제로 레지스터가 있다. 제로 레지스터는 모든 비트가 0으로 고정된 레지스터이다. 그런데 이들 두개 모두 31번 레지스터 번호로 인코딩된다. 그리고 인스트럭션에 따라 스택포인터로 쓸지 제로레지스터로 사용할지가 결정된다.

30번 레지스터인 x30은 리턴주소를 저장하는데 사용된다.

여기서 이야기하는 레지스터들은 모두 길이가 64비트이다. 이들의 하위 32비트에 접근하는 용도로 w0에서 w31을 사용할 수 있다. 하위 비트에 쓰기 명령을 수행하면 상위 비트는 남아있게 될까? 그렇지는 않다. 하위 32비트에 쓰기 명령을 내리면 상위 32비트가 클리어된다.

부동소수점/벡터 레지스터

A64에는 위의 정수 레지스터와는 별개로 부동소수점이나 128비트 벡터 연산을 위한 32개의 레지스터가 존재한다. 이들은 벡터 연산을 지원하기 때문에 한꺼번에 64비트나 128비트씩 동작하도록 할 수 있다. 즉, 한번에 8비트 혹은 16비트, 32비트, 64비트씩 나누어 쓸 수 있다. 이렇게 하면 한번에 여러개의 동일한 연산을 수행시킬 수 있어서 코드 실행속도를 높일 수 있다. 원래는 루프를 돌면서 해야 할 일을 한꺼번에 수행하는 것이다.

명령어

명령어들은 ARM ARM for ARMv8-A 문서에서 설명되어 있다. 명령어 갯수는 앨리어스를 제외하고 442개 정도 된다고 한다.

A64 명령어들은 모두 32비트 길이이다.

(명령어들의 레벨 분류 - main encoding, instruction group, decode group, instruction - 에 대해서는 이해하지 못해 정리할 수 없었다)

같은 이름을 쓰고 피연산자를 달리 갖는 명령어가 있다. 예를 들어 아래 FMUL명령어는 두 개의 부동소수점을 곱한다. C 언어에서 a = b * c 와 같은 것이다. A64에서는 피연산자에 따라 아래에서 보여지는 것들 중 하나가 될 것이다.

fmul s0, s1, s2            ;single precision floats
fmul d0, d1, d2            ;double precision floats
fmul v0.2s, v1.2s, v2.2s   ;vectors with two singles
fmul v0.4s, v1.4s, v2.4s   ;vectors with four singles
fmul v0.2d, v1.2d, v2.2d   ;vectors with two doubles
fmul s0, s1, v2.s[0]       ;multiplies by a vector element
fmul d0, d1, v2.d[0]
fmul v0.2s, v1.2s, v2.s[0] ;combinations of the above
fmul v0.4s, v1.4s, v2.s[0]
fmul v0.2d, v1.2d, v2.d[0]

이렇게 하나의 FMUL에서 많은 변형이 생기게 된다. 모든 대표 명령어에서 이렇게 변형이 많이 생기는 것은 아니다. 그래서 이런 변형까지 다 계산하면 모든 명령어의 수는 1000에서 2000개 정도가 된다고 한다. 명령어세트 설계자는 이들 변형과 피연산자까지 모두 포함하여 32비트 길이의 공간에 인코딩해야 하며 혹시라도 나중에 추가될 수도 있는 부분을 위한 여분까지 남겨두어야 할 것이다.

나머지 부분은 이해를 못해서 제외한다.

Emacs와 IPython을 함께 쓰기위한 설정을 만지던 중, 특정 virtualenv와 연동하는 부분에서 좀 막히게 되었다. 완벽한 솔루션은 아니지만 기록해둔다.

초반 삽질: elpy

Emacs Python IDE로 모드 중에 elpy가 눈에 띄었고, IPython관련 기능들도 있길래 이것으로 시작해 보았다. elpy는 pyvenv가 연동되며 자체에서 IPython 프로세스를 실행시키면 해당 pyvenv에 해당하는 IPython interpreter(Jupyter도 가능)가 뜨기 때문에 환경설정과 관련해서는 문제가 전혀 없었다.

하지만 곧 맞닥드린 문제가 있었는데, pyplot등으로 그린 표나 그림 등이 인라인으로 표시되지 않고 임시파일에 기록되어 미리보기(MacOS Preview App)등의 다른 윈도우에서 별도로 표시되는 것이었다.

인라인 표시 기능과 관련하여 한동안 찾아본 결과 org-babel이나 EIN(Emacs IPython Notebook)에서 가능하다는 정보를 알게 되었다.

Inline plot in emacs ipython REPL?

Emacs IPython Notebook

org-babel은 좀 아닌것 같아서 EIN을 들여다보기 시작했다. elpy처럼 자체에서 IPython REPL 프로세스를 띄울 수 있고, elpy에서 안되는 인라인 컨텐츠 표시도 잘 되었다.

하지만 EIN도 문제가 있었는데, 특정 virtualenv를 선택할 수가 없었다. 내 환경에는 virtualenv가 2개 - python3, python2 - 가 있는데 python3 환경에만 물렸다. 이렇게 되면 python3만 쓸 수 밖에 없다. 시스템에 python2랑 3가 둘 다 설치되어 있으면 브라우저 notebook 클라이언트에서는 둘 중 하나를 고를 수 있었는데, 특정 virtualenv와 물리게 되면 하나의 버전만 쓸 수 있다. 그럼 virtualenv에 python을 두개 설치하면? 확인해 본 결과 virtualenv는 하나의 python 버전만 사용하도록 설계되었단다.

Create a virtualenv with both python2 and python3

EIN and Jupyter with virtualenv

그래서 생각해낸 방법은 우선 터미널에서 virtualenv를 띄우고 거기서 Jupyter를 실행시킨 다음에, EIN에서 해당 Jupyter에 접속해서 notebook 환경을 사용하는 것이다. 이렇게 할 경우 터미널을 왔다갔다 해야 하긴 하지만 모든 문제가 해결된다. (해보진 않았지만) virtualenv/Jupyter 두 개 조합을 띄우고 둘 중 하나를 선택해서 들어갈 수도 있을 것 같다.

우선은 터미널을 띄우고 원하는 virtualenv를 활성화시킨다. 그리고 Jupyter를 띄우는데, 포트 번호랑 토큰(또는 암호)을 기록해둔다.

그리고 Emacs로 돌아와서 M-x ein:notebooklist-login 을 실행한다. 위에서 기록해둔 포트 번호와 토큰(또는 암호)를 입력한다. 그리고 M-x ein:notebooklist-open 을 입력하면 위에서 띄워놓은 notebook과 연결된다.

References

• Inline plot in emacs ipython REPL?
• Create a virtualenv with both python2 and python3
• Running a notebook server
• The Emacs IPython Notebook

이전에 다른곳에 썼던 내용을 이 블로그에 기록함.

안드로이드 빌드 스크립트를 만들다가 PATH 변수에 특정 문자열이 없을 경우 이를 추가해주는 기능이 필요했다. 관련 내용을 구글링해보니 대부분 문자열 치환에 대해서만 다루고 있었는데, stackoverflow 에서 마침내 원하는 답을 찾을 수 있었다.

http://stackoverflow.com/questions/229551/string-contains-in-bash

string = 'My long string';
if [[$string == *"My long"*]]
then
    echo "It's there!";
fi

이런식으로 대괄호 두개와([[, ]]) 와일드카드 캐릭터(*)를 써서 패턴 검사가 가능하다. 부정 연산자를 넣기 위해 좀 삽질을 했는데, 아래와 같이 ==을 !=으로 바꾸어주면 된다.

JAVA_HOME=/usr/lib/jvm/java-7-openjdk-amd64
if [[$PATH != *"$JAVA_HOME"*]]; then
    export PATH=$PATH:$JAVA_HOME/bin
fi

mode 버튼과 윗 방향 화살표 버튼을 동시에 누르세요.

참고: Forerunner 310XT Keys locked

운동을 마치고 시계(Gramin 310XT)를 만지던 중, 버튼을 누를 때마다 화면에 'Key Locked'라고 뜨는 현상이 생겼다. 홀드기능이 동작한건데, 뭘 눌러도 풀리지가 않아 집에와서 검색해보고 해결할 수 있었다. 위의 링크에서는 저 방법으로 홀드기능이 풀리지가 않았다던데 내 경우는 잘 풀렸다.

쉘 프롬프트에 현재 디렉토리 위치를 넣을 경우, 디렉토리 깊이가 깊어질수록 터미널이 지저분해지게 된다. Ubuntu 등의 배포판에서는 PROMPT_DIRTRIM 변수에 숫자를 지정해주면 그 숫자만큼만 프롬프트상에 표시되는 현재 디렉토리 경로를 줄여준다. 그렇지만 MacOS 기본 Bash 쉘(3.2.57)에는 PROMPT_DIRTRIM 이 구현되어 있지 않다. Bash 자체 버전을 올려도 되지만, 순정 상태를 건드리고 싶지는 않다(...). 그런데 손으로 구현하는 방법이 있어 정리해둔다.

참고: https://stackoverflow.com/questions/26554713/how-to-truncate-working-directory-in-prompt-to-show-first-and-last-folder

PS1='$(pwd | sed -E -e "s|^$HOME|~|" -e '\''s|^([^/]*/[^/]*/).*(/[^/]*)|\1..\2|'\'') \$ '

위 스택오버플로 페이지의 솔루션은 좋긴 하지만 처음 두 개 디렉토리 .. 마지막 하나의 디렉토리 로 구성된다. 이것을 조금 바꾸어 처음 1개의 디렉토리 .. 마지막 두개의 디렉토리 으로 만들고 싶다. 아무래도 뒤에 있는 경로가 좀 더 중요하니까. 따라서 스택오버플로 솔루션에서 순서를 바꾸어야 한다.

    PROMPT_PRE='\[\033[38;5;11m\]\u\[\033[38;5;15m\]@\h:\[\033[38;5;6m\]'
    PROMPT_POST='\[\033[38;5;15m\] '
    PWDTRIM1='$(pwd | sed -E -e "s|^$HOME|~|" -e '\''s|^([^/]*/[^/]*/).*(/[^/]*)|\1..\2|'\'')'
    PWDTRIM2='$(pwd | sed -E -e "s|^$HOME|~|" -e '\''s|^([^/]*/).*([^/]*/[^/]*/)|\1..\2|'\'')'
    PS1="${PROMPT_PRE}${PWDTRIM2}${PROMPT_POST}"

PWDTRIM1 이 스택오버플로 버전이고 PWDTRIM2 가 수정된 버전이다.

스크립트의 전체 구조를 보면, ① 먼저 pwd 명령으로 현재 작업 디렉토리 경로를 받아온 다음, ② sed로 $HOME 디렉토리 패턴을 물결(~)로 바꾸고, ③ 이어서 sed로 처음 하나의 디렉토리와 마지막 두개의 디렉토리 경로를 제외한 부분을 쩜쩜(..) 으로 바꾸어준다.

③ 단계가 복잡하니 이것만 자세히 분석해본다.

    PWDTRIM2='$(pwd | sed -E -e "s|^$HOME|~|" -e '\''s|^([^/]*/).*([^/]*/[^/]*/)|\1..\2|'\'')'

빨갛게 표시한 부분 좌우에 '\' 등 외따옴표로 묶인 것들은 escape를 위해 넣은 것들이다. 위의 sed 명령어에 쓰인 패턴매칭 크게 네 부분으로 나눌 수 있다.

① ^([^/]*/)

슬래시(/) 문자를 제외한 모든 문자 0개 이상으로 이루어진 문자열로 시작하는 패턴을 Back Reference로 구성하여 \1 로 저장. 이 패턴은 처음에 슬래시 문자가 나왔다가 다시 등장하거나, 슬래시 문자가 없다가 등장할 경우 패턴매칭이 끝나기 때문에 첫 번째 디렉토리 경로로 볼 수 있다.

② .*

첫 번째 매칭 이후에 나오는 모든 문자들의 패턴. 뒤에 나올 마지막 2개 디렉토리 패턴은 해당 패턴이 가져가므로, 처음 하나 ~ 나중 두개 디렉토리 경로에서 중간 부분이라고 볼 수 있다.

③ ([^/]*/[^/]*/)

[^/]*	'슬래시(/)문자를 제외한 모든문자 0개 이상으로 이루어진 문자열' 이후에
/	'슬래시(/)문자'가 나오고
[^/]*	그리고 이어서 '슬래시(/)문자를 제외한 모든 문자 0개 이상으로 이루어진 문자열'이 등장.
/	이어서 마지막으로 '슬래시(/)문자'가 나온다.

종합해 보면 마지막 2개의 디렉토리를 의미한다. 그리고 이 패턴은 Back Reference로서 /2 에 저장된다.

④ \1..\2

Back Reference 1번은 작업 디렉토리 경로에서 첫 번째 디렉토리이고, Back Reference 2번은 작업 디렉토리에서 마지막 두 개의 디렉토리이다. 이들 가운데 쩜쩜(..)을 넣도록 하여 문자열을 대치한다.

sed(1) 에서 사용되는 정규표현식에 대해서 알아보기 위해 Overview of Regular Expression Syntax 의 내용을 옮겨본다.

sed 를 잘 쓰기 위해서는 정규표현식(regexp)을 잘 알아야 한다. 정규표현식이란 주어진 문자열(subject string)에서 왼쪽에서 오른쪽으로 봐가면서 매칭되는 패턴을 의미한다. 정규표현식에서 대부분의 문자들(character)은 일반문자(ordinary)이다. 즉 이 문자들이 패턴 자체이고 주어진 문자열에서 해당 문자들이 나올 경우 매칭되게 된다. 예를 들어 아래와 같은 패턴은,

The quick brown fox

그 자체가 패턴이 된다. 하지만 정규표현식의 강력한 기능은 패턴을 작성함에 있어서 대치(alternatives)와 반복(repetitions)이 가능하다는 점이다. 정규표현식에서 대치와 반복은 특수문자를 써서 표현할 수 있다. 이렇게 특수문자로 쓰인 패턴은 그 자체가 패턴이 되는 것이 아니라 뭔가 특별한 용도를 위해 다르게 처리된다. 그럼 아래에 sed 에서 쓰이는 정규표현식 문법에 대해 정리해 보겠다.

정규표현식의 매칭방식은 좌에서 우로 나아가며 매칭하고, 같은 위치에서 두 개 이상의 매칭이 발견되었을 경우에는 긴 쪽을 택한다. 그래서 greedy(탐욕스러운) 하다라고도 한다.

아래는 정규표현식 예제들이다.

'abcdef'

쓰여진 그대로 'abcdef' 와 매칭됨.

'a*b'

0개 이상의 'a'와 그 다음에 'b'가 나오는 경우와 매칭된다. 예를 들면 'b'나 'aaaaab'.

'a\?b'

\? 는 0개 또는 1개 와 매칭되는 것이다. 따라서 'b' 또는 'ab' 와 매칭된다.

a\+b\+

\+ 는 1개 이상과 매칭되는 것이다. 따라서 1개 이상의 'a'와 이어서 1개 이상의 'b'가 오는 경우이다. 가장 짧게 매칭되는 경우가 'ab' 이고 'aaaab', 'abbbbb', 'aaaaaabbbbbb' 이렇게도 가능하다.

'.*/
'.\+'

둘 다 모든 캐릭터 문자열과 매칭되는 경우이다. 단, 위의 케이스는 널 스트링을 포함한 모든 문자열과 매칭되지만, 아래것은 최소한 하나의 문자는 들어있는 문자열과 매칭된다.

'^main.*(.*)'

'main'으로 시작하고, 소괄호로 둘러쌓인 문자열이 이어지는 경우이다. 'n'과 '('과 ')' 이 위치가 반드시 딱 붙어있어야 하는것은 아니다.

'^#'

'#'으로 시작하는 문자열과 매칭된다.

\\$

백슬래시(\) 하나로 끝나는 문자열과 매칭된다. 백슬래시를 두 개 썼지만 하나는 escaping 용도로 쓴 것이다.

'\$'

달러 기호 하나와 매칭된다. 여기에 쓰인 백슬래시도 escaping 용도로 쓰였다.

'[a-zA-Z0-9]'

환경변수 로케일이 C locale 인 경우, 모든 ASCII 문자 혹은 숫자와 매칭된다.

'[^ tab]\+

여기서 tab 은 탭 문자이다. 이 예제는 공백이나 탭 문자를 제외한 한 글자 이상의 캐릭터와 일치한다. 즉, 한 단어(word)를 의미한다.

'^\(.*\)\n\1$'

\(regexp\) 은 그룹을 이루고 back reference 로도 쓰인다. 이 예제는 두 개의 동일한 문자열 사이에 개행문자가 하나 들어간 꼴이다.

'.\{9\}A$'

9개의 문자에 이어서 A가 나오는 패턴이다.

'^.\{15\}A'

16개의 문자로 시작하고, 그 16개 중에 마지막 문자가 A인 경우이다.

가끔 실행중인 프로세스를 종료시키고 싶을 때 Ctrl + c 가 먹지 않는 경우가 있다. 이럴때 나는 Ctrl + z 로 실행중인 프로세스를 백그라운드로 돌려놓고, PID를 알아낸 다음에 SIGKILL 시그널(9번)을 보내는 식으로 처리하곤 했다.

그런데 이것을 좀 쉽게 하는 방법이 있었다.

• 모든 백그라운드 프로세스 끝내버리기: kill -9 $(jobs -p)
• 백그라운드 프로세스 하나만 끝내버리기:
  우선 jobs 명령어로 모든 백그라운드 프로세스의 목록을 가져온 다음에,
  kill %1 하면 첫 번째 프로세스를 끝낼 수 있고,
  kill %2 하면 두 번째 프로세스를 끝낼 수 있다.

참고: https://unix.stackexchange.com/questions/104821/how-to-terminate-a-background-process

macOS에 emacs ggtags 설치 및 설정하는 과정을 정리한다. 성공한 환경은 아래와 같다.

• macOS Version: macOS Sierra 10.12.6 (16G29)
• emacs Version: GNU Emacs 25.1.1 (x86_64-apple-darwin13.4.0, NS appkit-1265.21 Version 10.9.5 (Build 13F1911)) of 2016-09-21

1. 설치

1.1 Homebrew로 ruby, ctags 설치

brew install --upgrade ruby
brew install --HEAD ctags

1.2 Homebrew로 GNU Global 설치

brew install global --with-exuberant-ctags

1.3 pygments 플러그인 설치

sudo pip install pygments
sudo pip3 install pygments

pygments는 Syntax Highlighter이다. ctags가 레퍼런스 탐색 기능을 제공하지 않기 때문에 Global에서 pygments 플러그인을 사용하도록 설정해 주어야 한다.

2. 설정

2.1 pygments 설정

시스템 환경 변수(.bashrc 등)에 아래와 같이 설정해준다.

export GTAGSCONF=~/.globalrc
export GTAGSLABEL=pygments

즉, Emacs에는 아래와 같이 해주면 된다.

(setenv "GTAGSCONF" (concat (expand-file-name "~") "./globalrc"))
(setenv "GTAGSLABEL" "pygments")

만일 ~/.globalrc 파일이 없다면, /usr/local/share/gtags/gtags.conf 파일을 복사하여 ~/.globalrc 로 만든다. 그리고 :ctagscom= 을 검색하여 아래와 같이 바꿔준다(2개 정도 나옴).

exuberant-ctags|plugin-example|setting to use Exuberant Ctags plug-in parser:\
  :tc=common:\
  :ctagscom=/usr/local/opt/ctags/bin/ctags:\

...

pygments-parser|Pygments plug-in parser:\
  :ctagscom=/usr/local/opt/ctags/bin/ctags:\

2.2 Emacs 설정

(and
 (require 'ggtags nil t)
 (message "ggtags initializing...")
 (autoload 'ggtags-mode "ggtags"
   "Minor mode for browsing source code using GLOBAL" t))

(eval-after-load 'ggtags
  '(progn
     (add-hook 'c-mode-common-hook
               (lambda ()
                 (when (derived-mode-p 'c-mode 'c++-mode 'java-mode 'objc-mode)
                   (ggtags-mode 1))))
     (add-hook 'python-mode-hook (lambda () (ggtags-mode 1)))

     ;; Set GTAGS variables
     (setenv "GTAGSCONF" (concat (expand-file-name "~") "/.globalrc"))
     (setenv "GTAGSLABEL" "pygments")

     (define-key ggtags-mode-map (kbd "C-c C-f") 'ggtags-find-file)
     (define-key ggtags-mode-map (kbd "C-c g") 'ggtags-grep)
     ))

(provide 'koodev-ggtags)

3. 실행

프로젝트 폴더로 가서 소스파일을 하나 열고 M-x ggtags-find-tags-dwim 을 실행하면 루트 폴더의 위치를 묻는데, 프로젝트 루트를 지정해주면 잠시 후 G* 파일들이 생성된다.

단축키 등의 자세한 정보는 다음 링크를 참고한다: https://github.com/leoliu/ggtags

4. 기타

ImportError: No module named pygments 이런 에러가 뜨는 경우, 우선은 pygments 플러그인을 잘 설치했나 확인해보고, 실행 환경에서 python이 어느 경로로 잡혀있는지 확인해본다. 내 경우에는 시스템에 python이 두 개가 설치되어 있었는데, 터미널을 열 경우와 Emacs나 다른 유틸(GNU Global)을 실행하는 시점에서 python 경로가 달라 위와 같은 에러가 떴다. 추가로 설치된 python을 삭제하고 pygments 등을 재설치해 주었더니 문제가 해결되었다.

References

• https://github.com/leoliu/ggtags
• https://github.com/leoliu/ggtags/wiki/Install-Global-with-support-for-exuberant-ctags
• http://pygments.org

다시 한 번 집고 넘어가보자. Group G의 Subgroup H의 Left Coset을 아래와 같이 정의했다.

위 식을 가지고 Right Coset을 정의하면 아래와 같다.

Right Coset들도 역시 Congruence Relation을 이루는 Equivalence Class이다. Left Coset의 Equivalence Relation과 비교해보자.

Right Coset과 Left Coset은 일치하지 않을 수 있다. Cosets 관련 포스트에서 계속 예로 들어온 S₃ 과 Subgroup {1, xy} 에서의 Right Coset은 아래와 같다.

반면에 Left Coset은 아래와 같았다.

이렇게 Left와 Right Coset으로 나뉘어진 Partition은 다를 수 있으나.., 그런데 N이 Normal Subgroup일 경우엔 Left와 Right Coset이 서로 같게 된다.

여기서 Normal Subgroup이 뭐였는지에 대해 잠깐 복습해보자.

Definition. 다음 속성을 갖는 Group G의 Subgroup N을 Normal Subgroup이라고 부른다: 모든 a ∈ N와 모든 b ∈ G에 대하여 Conjugate bab^-1은 N의 엘리먼트이다. (여기서 Subgroup N이 꼭 Kernel일 필요는 없다)

다시 본론으로 돌아와서 Normal Subgroup으로 만들어진 Left와 Right Coset에 대해 살펴보자.

Proof. H가 Normal이라고 하자. 그러면 Normal의 정의에 의해 h ∈ H와 a ∈ G에 대하여

이게 된다. 제일 오른쪽 두 항이 서로 역이라서 소거되므로 둘은 같다.

H가 Normal Subgroup이기 때문에 (Normal의 정의에 의해) Conjugate 엘리먼트인 k = aha^-1 은 H의 엘리먼트이기도 하게된다. 따라서 엘리먼트 ah는 ah = ka 가 성립하고, 이 엘리먼트는 aH에도 속하고, Ha에도 속한다. 즉, aH ⊂ Ha 이며, aH ⊃ Ha 이므로 두 Coset들은 서로 같게 된다.

이번엔 반대로 H가 Normal이 아닌 경우를 생각해보자. 그러면 aha^-1 ∉ H인 엘리먼트 h ∈ H 와 a ∈ G 가 존재할 것이다. 그리고 ah는 Left Coset인 aH의 엘리먼트이지만 Right Coset인 Ha의 엘리먼트는 아니게 된다. 근데 만일에 ah가 Right Coset에도 포함된다고 생각해보자. ah = h'a for some h' ∈ H 이고, 그러면 aha^-1 = h' (aa^-1) ∈ H 이게 된다. 이러면 애초에 Normal이 아닌 조건, 즉 aha^-1 ∉ H 였으므로 모순이 된다. 따라서 Normal Subgroup이 아니면 Left Coset과 Right Coset이 같을 수가 없는 것이다.

한가지 더, aH와 Ha가 공통의 엘리먼트를 하나 갖고 있다고 하자. 그 엘리먼트는 분명히 a이다. 따라서 aH는 a말고 다른 Right Coset과 같은 것이 있을 수 없다. 이를 통해 Left Coset으로 나뉘어진 Partition과 Right Coset으로 나뉘어진 Partition이 같을 수가 없다는 것을 확인할 수 있다.

지난 내용에서 Group G의 Subgroup H의 Left Coset을 아래와 같이 정의했다.

여기서 어떤 Subgroup의 Left Coset의 개수를 Index of H in G라고 부르고 아래와 같이 표기한다.

예를 들어 Group G를 Symmetric Subgroup S₃이며 G = {1, x, x², y, xy, x²y} 라고 하고, x와 y가 아래와 같고,

Subgroup H = {1, xy} 일 때, [G : H] = 3 이다. 물론 G가 무한개의 엘리먼트를 가진다면 Index도 무한대가 된다.

Subgroup H에서 Coset aH으로의 관계는 Bijective 매핑: h ⇝ ah 이다. 따라서 아래 내용이 성립한다.

H의 Coset들의 합집합(Union)은 G가 되며, 각각의 Coset들은 서로 겹치지 않기 때문에 Counting Formula라고 불리는 아래와 같은 공식을 이끌어낼 수 있다.

즉, 위의 예에서 G의 Order는 H의 Order가 2이고, H의 Left Coset은 총 3개가 나오므로, 2 × 3 = 6 이 된다.

그리고 위의 공식에서 우변의 두 항 모두가 좌변을 나눌 수 있다는 사실은 굉장히 중요하다. 이 사실을 정리하면 아래와 같은 Lagrange's Theorem이 된다.

나눈 값은 [G : H]이다. 앞서 Cyclic Subgruop에서 어떤 엘리먼트 a ∈ G의 Order는 a에 의해 생성되는 Cyclic Subgroup의 Order라고 했다. 따라서 Lagrange's Theorem은 아래 내용을 내포한다.

그리고 이 사실을 바탕으로 아래의 내용을 도출한다.

a ≠ 1 이기 때문에 a의 Order는 1 보다 크다. 그리고 위의 정리에 의하여 a의 Order가 |G| = p 를 나눈다. p가 1 또는 자기 자신으로밖에 못 나누기 때문에 a의 Order는 p가 되고, a로 인해 생성되는 Cyclic Subgroup은 Order가 p이므로 이는 G와 같게 되는 것이다.

또한 Order가 소수 p인 Group G와 그 엘리먼트 a로 생성되는 Order가 역시 p인 Cyclic Subgroup은 서로 Isomorphic 한 관계가 된다.

Counting Formula는 Homomorphism 에서도 적용될 수 있다. φ:G ⟶ G' 을 Homomorphism 매핑이라고 하자. ker φ의 Left Coset은 φ의 Fibres 라고 했다(Congruence Relation & Coset). 이들 Fibres는 매핑된 Image와 Bijective한 관계를 갖는다. 따라서 아래 공식도 성립한다.

Group G의 Subgroup인 ker φ 의 Left Coset 개수는 φ 를 통해 사상된 Image의 엘리먼트 개수와 같다. 이를 Counting Formula에 대입하면 아래 내용을 얻을 수 있다.

위의 식은 아래와 같은 방식으로 유도된다.

| G | = | H | · [G : H] ... (1)
| G | = | ker φ | · [G : ker φ] ... (2)
| G | = | ker φ | · | im φ | ... (3)
그리고 두 식 (2)와 (3)을 합치면,
| G | = | ker φ | · | im φ |

즉, | ker φ |나 | im φ |나 모두 | G |를 나눈다. 그리고 im φ는 G'의 Subgroup이기 때문에 | im φ |는 G'도 나눌 수 있다.