Noq

เลขที่

สำคัญอย่างยิ่ง! ภาษานี้เป็นงานที่กำลังดำเนินการ! ทุกสิ่งสามารถเปลี่ยนแปลงได้ตลอดเวลาโดยไม่ต้องแจ้งให้ทราบล่วงหน้า! ใช้ภาษานี้ด้วยความเสี่ยงของคุณเอง!

ไม่ใช่โค้ก. หม้อแปลงนิพจน์อย่างง่ายที่ไม่ใช่ Coq

เริ่มต้นอย่างรวดเร็ว

$ cargo run ./examples/peano.noq 

แนวคิดหลัก

แนวคิดหลักคือความสามารถในการกำหนดกฎการเปลี่ยนแปลงของนิพจน์พีชคณิตเชิงสัญลักษณ์และนำไปใช้ตามลำดับ

การแสดงออก

ไวยากรณ์นิพจน์ปัจจุบันสามารถกำหนดได้ประมาณนี้:

 <expression> ::= <operator-0>
<operator-0> ::= <operator-1> ((`+` | `-`) <operator-0>)*
<operator-1> ::= <operator-2> ((`*` | `/`) <operator-1>)*
<operator-2> ::= <primary> (`^` <operator-2>)*
<primary> ::= (`(` <expression> `)`) | <application-chain> | <symbol> | <variable>
<application-chain> ::= (<symbol> | <variable>) (<fun-args>)+
<symbol> ::= [a-z0-9][_a-zA-Z0-9]*
<variable> ::= [_A-Z][_a-zA-Z0-9]*
<fun-args> ::= `(` (<expression>),* `)`

กฎและรูปร่าง

เอนทิตีหลักสองประการของภาษาคือกฎและรูปร่าง กฎจะกำหนดรูปแบบ (ส่วนหัว) และเป็นการทดแทนที่สอดคล้องกัน (เนื้อหา) คำจำกัดความของกฎมีไวยากรณ์ดังต่อไปนี้:

 <name:symbol> :: <head:expression> = <body:expression>

นี่คือตัวอย่างของกฎที่สลับองค์ประกอบของคู่:

 swap :: swap(pair(A, B)) = pair(B, A)

การสร้างรูปร่างเป็นกระบวนการของการใช้กฎตามลำดับกับนิพจน์เพื่อเปลี่ยนให้เป็นนิพจน์อื่น การสร้างรูปร่างมีไวยากรณ์ดังต่อไปนี้:

 <expression> {
  ... sequence of rule applications ...
}

ตัวอย่างเช่น นี่คือวิธีที่คุณจัดรูปร่างนิพจน์ swap(pair(f(a), g(b))) ด้วยกฎ swap ที่กำหนดไว้ด้านบน:

 swap(pair(f(a), g(b))) {
  swap | all
}

ผลลัพธ์ของการสร้างรูปร่างนี้คือ pair(g(b), f(a))

กฎที่ไม่ระบุชื่อ

คุณไม่จำเป็นต้องกำหนดกฎเพื่อใช้ในการจัดรูปแบบ:

 swap(pair(f(a), g(b))) {
  swap(pair(A, B)) = pair(B, A) | all
}