추상 개서기

ARM(Abstract Rewriting Machine)은 최소 기간 다시 쓰기 시스템에 대한 용어 다시 쓰기를 구현하는 가상 시스템입니다.

최소 용어 개서 시스템은 각 규칙이 다음 6가지 형식 중 하나를 사용하는 왼쪽 선형 용어 개서 시스템입니다.

속행

${\displaystyle fbc {x}, {\vec {y}, {\vec {z}})\rightarrow gbc\vec {x}, hbec\vec {y}}, {\vec {z}}}}}}}}$

돌아가다

${\displaystyle f(x)\오른쪽 화살표 x}$

경기

${\displaystyle fbec {x}}, gbec\vec {y}, {\vec {z}})\rightarrow hbc\vec {x}, {\vec {y}, {\vec {z}}}}}}}}$

더하다

${\displaystyle fvc {x}, {\vec {z}}, {\vec {x}}, {\vec {z}}-{\rm {for}~y\in {vec {z}}}\cup {vec {z}}}}$

삭제

${\displaystyle fbc {x}, {\vec {y}, {\vec {z}})\rightarrow gbc\vec {x}, {\vec {z}}}}$

식별하다

$(\displaystyle fvec {x})\오른쪽 화살표 gvec {x}})$

이들 6가지 폼 각각은 (ARM으로) 최신 마이크로프로세서의 1개 또는 몇 개의 프로세서 명령에 매핑되어 있습니다.따라서 최소 용어 개서는 감소 단계당 수십~수백 클럭 사이클(초당 수백만 개의 감소 단계)로 달성됩니다.

ARM은 일반 용어 개서를 구현하며, 모든 단일 정렬 무조건 좌선형 용어 개서 시스템을 동일한 정규 형식 관계를 발생시키는 최소 용어 개서 시스템으로 변환(컴파일)할 수 있습니다.

가장 안쪽 개서를 위한 이 컴파일 프로세스에 대한 개요와 ARM에 대한 자세한 개요는 "Within ARM's reach: 최소 개서 시스템을 통한 왼쪽 선형 개서 시스템 편집"에서 찾을 수 있습니다.느린(가장 안쪽이 아닌) 개서에 대한 설명은 "게으른 기계로 개서"에서 확인할 수 있습니다.

ARM의 문서화된 실장(언어 「Epic」을 개서)은, 이쪽에서 입수할 수 있습니다.사이트와 소프트웨어는 더 이상 능동적으로 유지 보수되지 않습니다.

레퍼런스

• Giesl, J. R.; Middeldorp, A. (July 2004). "Transformation techniques for context-sensitive rewrite systems" (PDF). Journal of Functional Programming. 14 (4): 379–427. CiteSeerX 10.1.1.127.2817. doi:10.1017/S0956796803004945.
• Lucas, Salvador (2002). "Lazy Rewriting and Context-Sensitive Rewriting" (PDF). Electronic Notes in Theoretical Computer Science. 64: 234–254. CiteSeerX 10.1.1.14.3470. doi:10.1016/S1571-0661(04)80353-0. Archived from the original (PDF) on 2006-05-16. Retrieved 2015-08-29.
• Nguyen, Quang-Huy (2001). "Compact Normalisation Trace via Lazy Rewriting" (PDF). Electronic Notes in Theoretical Computer Science. 57: 87–108. CiteSeerX 10.1.1.24.771. doi:10.1016/S1571-0661(04)00269-5.
• Schernhammer, F.; Gramlich, B. (April 2008). "Termination of Lazy Rewriting Revisited" (PDF). Electronic Notes in Theoretical Computer Science. 204: 35–51. CiteSeerX 10.1.1.142.1957. doi:10.1016/j.entcs.2008.03.052.
• Kirchner, C.; Kirchner, H. (2014). "Equational Logic and Rewriting". Handbook of the History of Logic. 9: 255–282. doi:10.1016/B978-0-444-51624-4.50006-X. ISBN 9780444516244.
• Antoy, S.; Johannsen, J.; Libby, S. (2015). "Needed Computations Shortcutting Needed Steps". Proceedings 8th International Workshop on Computing with Terms and Graphs. 183: 18–32. arXiv:1505.07162v1. doi:10.4204/EPTCS.183.2.