Name: HypergraphGo
SKU: -

소개

HypergraphGo는 Go 언어로 작성된 놀 getType 이론(HoTT) 커널과 일반화된 하이퍼그래프操作 라이브러리입니다. 프로그래밍 언어 연구자, 도구 개발자, 그리고 유형 이론의 내부 구조를 이해하려는 학습자를 위해 설계되었습니다. 이 프로젝트는 대규모 표준 라이브러리와 증명 모드를 포함하여, 유형 검사기의 기반부터 증명까지의 전체적인 흐름을 제공합니다.

상세정보

HoTT 커널

HoTT 커널은 NbE(Normalization by Evaluation) 기반 정규화, 양방향 유형 검사, 항등 유형, 경로 유형, 글루 유형(Glue Types), 합성(Composition), 전송(Transport), 그리고 고계 유형(Higher Inductive Types)을 포함하는 입증된 유형 이론 구현입니다.

계산적 단일성(Univalence): ua 함수는 등가성을 경로로 변환하며, 글루 유형을 통해 실제로 계산됩니다.
고계 유형(HITs): 원형 S¹의 루프(loop), 명제적 단순화(propositional truncation), 현탁(suspensions) 등 경로 생성자가 계산됩니다.
유도 타입 및 제거자: 사용자 정의 유도 타입과 자동 생성되는 제거자를 지원합니다. List A, Vec A n 등의 매개변수화된 타입과 상호 재귀를 처리합니다.
양방향 유형 검사: Synth로 추론하고, Check로 검증하며, 소스 위치를 포함한 구조화된 오류를 제공합니다.

하이퍼그래프 라이브러리

하이퍼그래프는 일반 그래프를 일반화하여 간선이 두 개가 아닌 임의의 수의 정점에 연결될 수 있게 합니다. 이 라이브러리는 Go에서 범용 하이퍼그래프 연산을 제공합니다.

기본 연산: 정점과 간선을 추가하고, 이중(dual), 2-섹션(two-section), 선 그래프(line graph) 등의 변환을 수행합니다.
알고리즘: BFS/DFS 순회, 연결 성분, 탐욕적 히팅 세트(greedy hitting set), 최소 전달자(minimal transversals), 정점 색칠(vertex coloring) 등을 포함합니다.

다운로드 및 설치

HypergraphGo는 다양한 패키지 관리자를 통해 설치할 수 있습니다. Windows에서는 Chocolatey 또는 Scoop을 사용할 수 있습니다.

Go 모듈 사용: go get github.com/watchthelight/HypergraphGo
Homebrew (macOS/Linux): brew install watchthelight/tap/hg
Scoop (Windows): scoop bucket add watchthelight https://github.com/watchthelight/scoop-bucket 후 scoop install hg
APT (Debian/Ubuntu): 설정 스크립트 실행 후 sudo apt install hypergraphgo
Docker: docker pull ghcr.io/watchthelight/hypergraphgo:1.9.1
Chocolatey (Windows): Chocolatey 패키지 페이지를 통해 설치 가능합니다.
바이너리 다운로드: GitHub 릴리스 페이지에서 직접 다운로드할 수도 있습니다.

기본 사용법 및 명령어

두 가지 주요 실행 파일(hg와 hottgo)을 제공합니다.

hg: 하이퍼그래프 연산

hg new -o graph.json: 빈 하이퍼그래프를 생성합니다.
hg add-edge -f graph.json -id E1 -m A,B,C: 간선을 추가합니다.
hg dual -f graph.json -o dual.json: 이중 변환을 수행합니다.
hg bfs -f graph.json -start A: BFS 탐색을 시작합니다.
hg repl: 대화형 모드를 시작합니다.

hottgo: 유형 검사 및 증명

hottgo --check FILE: 파일의 유형을 검사합니다.
hottgo --eval EXPR: 식을 평가합니다.
hottgo --synth EXPR: 타입을 합성합니다.
hottgo --load FILE: 태스크립트 스크립트를 검증합니다.
REPL 모드에서 :eval, :synth, :prove TYPE, :quit 등의 명령을 사용할 수 있습니다.

이런 경우에 유용합니다

프로그래밍 언어 연구자: 증명 조교(proof assistant)의 복잡한 설명기(elaborator) 없이 입방 유형 이론(cubical type theory)을 연구하고 싶을 때 유용합니다.
도구 개발자: 실제로 임베딩하고 제어할 수 있는 유형 이론 백엔드가 필요할 때 유용합니다.
HoTT 학습자: NbE, 양방향 검사, 경로 유형 등 내부 작동 방식을 직접 확인하고 학습하고 싶을 때 유용합니다.
Go 개발자: 종속 타입(dependent types)에 대한 호기심을 충족하고 자체 도구를 구축하기 위한 커널 레이어를 찾을 때 유용합니다.

지원 환경·시스템 요구사항

언어: Go 1.23 이상이 필요합니다.
운영 체제: Linux, Windows, macOS를 지원합니다.
아키텍처: 커널은 약 6,700줄, 지원 코드는 약 7,000줄로 구성되어 있습니다.

제한 사항·확인 사항

이 소프트웨어는 프로그래밍 언어 연구자 및 개발자를 위한 개발·코딩 도구입니다.
설치 및 사용을 위해 Go 언어 환경 설정이 필요할 수 있습니다.
증명 스크립트의 문법은 S-표현식과 명시적인 드 브루인 인덱스를 사용합니다.

FAQ

Q: HypergraphGo는 무료인가요?
A: 네, 이 프로젝트는 MIT 라이선스에 따라 오픈 소스로 제공됩니다.

Q: Windows에서 사용할 수 있나요?
A: 네, Windows를 지원하며 Chocolatey, Scoop을 통해 설치하거나 GitHub에서 바이너리를 다운로드할 수 있습니다.

Q: 인터넷 연결이 필요한가요?
A: 패키지 관리자를 통한 설치 시 인터넷 연결이 필요하지만, 설치 후에는 오프라인에서 실행 가능합니다.

시스템 요구사항

Go 1.23 이상

HypergraphGo

소개