코인전도

이 글에는 여러 가지 문제가 있다.이 문제를 개선하거나 대화 페이지에서 토의하십시오.(이러한 템플릿 메시지를 제거하는 방법 및 시기 알아보기) 이 글은 대부분의 독자들이 이해하기에는 너무 기술적인 것일 수도 있다. 기술 세부 정보를 제거하지 않고 비전문가가 이해할 수 있도록 개선하십시오.(2011년 10월) (이 템플릿 메시지를 제거하는 방법 및 시기 학습) 이 기사는 주요 출처에 대한 언급에 너무 많이 의존하고 있다. 이차 또는 3차 소스를 추가하여 개선하십시오.(2019년 11월) (이 템플릿 메시지를 제거하는 방법과 시기 알아보기) (이 템플릿 메시지를 제거하는 방법 및 시기 알아보기)

컴퓨터 과학에서 코인 전도는 동시에 상호작용하는 사물의 시스템의 속성을 정의하고 증명하는 기술이다.

동전도란 구조적 유도에 대한 수학적인 이중성이다.코인덕적으로 정의된 유형은 코다타라고 알려져 있으며 일반적으로 스트림과 같은 무한 데이터 구조다.

정의 또는 명세서로서, 코인 전도는 물체가 단순한 물체로 "관찰", "파괴"될 수 있는 방법을 설명한다.증명 기법으로서, 그러한 명세서의 가능한 모든 구현에 의해 방정식이 충족된다는 것을 보여주기 위해 사용될 수 있다.

코다타를 생성하고 조작하기 위해서, 사람들은 게으른 평가와 함께 일반적으로 핵심 기능을 사용한다.비공식적으로 각 유도 생성자에 대한 패턴 매칭에 의해 함수를 정의하기 보다는 함수 결과에 대해 각각 "파괴자" 또는 "파괴자"를 정의한다.

프로그래밍에서, 공동 로직 프로그래밍(간단함을 위한 co-LP)은 로직 프로그래밍과 코인 유도 논리 프로그래밍의 자연스러운 일반화로서, 무한 트리, 게으른 술어, 동시 통신 술어 등과 같은 로직 프로그래밍의 다른 확장을 일반화한다.'Co-LP'는 합리적 나무, 비위생적 특성 검증, 게으른 평가, 동시 로직 프로그래밍, 모델 확인, 이등비교 증명 등에 응용이 가능하다.^[1]co-LP의 실험 구현은 달라스의^[2] 텍사스 대학교와 로그톡(예: 참조)^[3] 및 SWI-Prolog에서 이용할 수 있다.

참고 항목

• F-석탄자
• 코어커시온
• 비시뮬레이션
• 아나모르피즘
• 총 기능 프로그래밍

참조

추가 읽기

교과서

• 다비데 생요르기(2012년).비시뮬레이션과 코인전도 소개.케임브리지 대학 출판부.
• 다비드 생요르기와 얀 러튼(2011년).Bisimulation 및 Coinroduation의 고급 주제.케임브리지 대학 출판부.

입문서

• 앤드루 D. 고든(1994년)."A Tutorial on Co-induction and Functional Programming". 1994: 78–95. CiteSeerX 10.1.1.37.3914. {{cite journal}}: Cite 저널 요구 (도움말) — 수학 중심적 설명
• 바트 제이콥스와 얀 러튼(1997년).(Co)에 대한 자습서알헤브라스 및 (Co)유도(대체 링크) — 유도 및 코인 전도를 동시에 설명
• 에두아르도 기메네즈와 피에르 카스테란(2007)이다."Coq의 [Co-]유도형식에 대한 자습서"
• 코인전도 - 간략한 소개

역사

• 다비데 생요르기."비시뮬레이션과 코인전도의 기원에 관한 연구" ACM Transactions on Programming Language and Systems, Vol. 31, Nb 4, Mai 2009.

잡다한

• 동시 로직 프로그래밍: 코인 전도를 통한 로직 프로그래밍 확장 — 공동 로직 프로그래밍 패러다임을 설명한다.