Show HN: Lean4 Datalog DSL Based on Google Zanzibar for AI Projects

개요

Lean 4를 기반으로 Google Zanzibar의 개념을 차용한 ZIL(Zanzibar-inspired Language)은 AI 프로젝트를 포함한 다양한 프로젝트에서 객체, 관계, 규칙을 정의하고 추론하는 데 사용되는 소규모 관계형 언어입니다.

주요 내용

* ZIL의 관계 모델: ZIL은 subject ── relation ──▶ object 형태의 3부분으로 구성된 관계(relation)를 사용하며, 이는 Google Zanzibar의 튜플(tuple) 기반 모델에서 영향을 받았습니다. 예를 들어 doc:readme#owner@user:10과 같은 형태를 Lean 네이티브 문법으로 zil_fact node(doc.readme) ⟶[owner] node(user.u10)와 같이 표현합니다.
* Datalog 스타일 규칙: ZIL은 Datalog 시스템에서 일반적으로 사용되는 Horn 규칙을 사용하여 기존 관계에서 새로운 관계를 추론합니다. 예를 들어, 그룹이 문서를 볼 수 있고 사용자가 해당 그룹에 속해 있다면, 사용자는 문서를 볼 수 있다는 규칙을 정의할 수 있습니다.
* 프로젝트 관계 맵: ZIL은 프로젝트의 선언(declarations), 요구사항(requirements), 문서(documents), 테스트(tests), 의존성(dependencies) 등의 복잡한 관계를 표현하고 추론하는 데 사용됩니다. 이를 통해 "어떤 선언이 이 요구사항을 구현하는가?"와 같은 질문에 답할 수 있습니다.
* Lean과 ZIL의 통합: Lean은 코드의 정확성을 검증하고, ZIL은 이러한 검증된 선언들이 프로젝트 내에서 어떤 역할을 하는지, 다른 요소들과 어떻게 연결되는지를 저장하고 추론합니다. 이는 개발자, 검토 도구, CI, 문서 도구, AI 어시스턴트 등이 동일한 프로젝트 정보를 활용할 수 있도록 합니다.
* 핵심 구조: ZIL은 노드(객체를 식별), 관계(두 항을 연결), 규칙(관계에서 관계를 도출), 쿼리(일치하는 항과 변수 바인딩 반환)의 네 가지 주요 구조를 사용합니다.
* 관계 스키마 및 타입 검사: 관계 스키마는 예상되는 소스 및 타겟 타입을 정의하여 범주 오류를 방지하며, 타입이 지정된 규칙을 통해 변수의 타입을 명시할 수 있습니다.
* 지속성 및 데이터 교환: ZIL은 Lean 환경 확장 기능을 사용하여 사실, 규칙, 스키마, 계약 등을 저장하며, ZILX/1 스냅샷 및 ZILD/1 델타를 통해 도구 간에 프로젝트 맵을 교환할 수 있습니다. 또한, Soufflé Datalog 또는 Prolog 형식으로 내보낼 수 있습니다.
* 신뢰 수준 및 설명: ZIL은 직접 등록된 사실(asserted), 그래프에서 파생된 관계(graphDerived), Lean 명제 및 증명으로 뒷받침되는 규칙(certified)의 세 가지 신뢰 수준을 기록하며, 추론된 관계에 대한 단계별 설명을 제공합니다.
* CLI 및 도구 지원: 네이티브 zil 실행 파일은 .zc 모델과 ZILR/1 리비전 로그를 읽고, 컴파일, 확장, 쿼리, 스냅샷 생성 등 다양한 작업을 지원합니다.

시사점

ZIL은 Lean의 형식 검증 능력과 Zanzibar의 강력한 관계 모델링을 결합하여, AI 프로젝트를 포함한 복잡한 소프트웨어 프로젝트에서 코드의 의미, 관계, 의존성을 명확하게 정의하고 관리하며, 이를 통해 개발 효율성, 코드 품질, 자동화된 도구와의 통합을 크게 향상시킬 수 있습니다.