Janusเป็น ภาษาโปรแกรม ที่ย้อนเวลาได้เขียนขึ้นที่Caltechในปี 1982 ^{[ 1 ]}ความหมายเชิงปฏิบัติการของภาษาได้รับการกำหนดอย่างเป็นทางการ พร้อมด้วยตัวผกผันโปรแกรมและตัวแปลความหมายด้วยตนเอง ที่ผกผันได้ ในปี 2007 โดย Tetsuo Yokoyama และ Robert Glück ^{[ 2 ] [ 3 ]}ตัวผกผันและตัวแปลความหมายของ Janus มีให้ใช้งานได้ฟรีโดยกลุ่มวิจัย TOPPSที่DIKU ^{[ 4 ]}ตัวแปลความหมายของ Janus อีกตัวหนึ่งถูกนำไปใช้ในPrologในปี 2009 ^{[ 5 ]}คอมไพเลอร์ที่ปรับให้เหมาะสมได้รับการพัฒนาในกลุ่มวิจัย RC3 ^{[ 6 ] [ 7 ]}ด้านล่างนี้สรุปภาษาที่นำเสนอในเอกสารปี 2007 ^{[ 2 ]}

Janus เป็นภาษาการเขียนโปรแกรมเชิงคำสั่งที่มีโครงสร้างซึ่งทำงานบนหน่วยความจำส่วนกลางโดยไม่ต้องจัดสรรฮีป และไม่รองรับโครงสร้างข้อมูลแบบไดนามิก ในฐานะภาษาการเขียนโปรแกรมแบบย้อนกลับได้ Janus ดำเนินการคำนวณแบบกำหนดได้ทั้งในทิศทางไปข้างหน้าและย้อนกลับ ส่วนขยายของ Janus มีพารามิเตอร์ของขั้นตอนและ การประกาศ ตัวแปรท้องถิ่น (local-delocal) ^{[ 3 ]}นอกจากนี้ Janus เวอร์ชันอื่นๆ ยังรองรับโครงสร้างข้อมูลแบบไดนามิก เช่น รายการ^{[ 8 ] [ 9 ]}

เรากำหนดไวยากรณ์ของ Janus โดยใช้รูปแบบ Backus– Naur

โปรแกรม Janus คือลำดับของการประกาศตัวแปรหนึ่งตัวขึ้นไป ตามด้วยลำดับของการประกาศโปรแกรมย่อยหนึ่งตัวขึ้นไป:

< โปรแกรม> :: = <v-decl> <v-decls> <p-decl> <p-decls> <v-decls> :: = <v-decl> <v-decls> | " " <p-decls> :: = <p-decl> <p-decls> | " "​​ ​​​​​​​​​​​ 

หมายเหตุ Janus ตามที่ระบุไว้ในเอกสารปี 2007 ^{[ 2 ]}อนุญาตให้มีตัวแปรศูนย์ตัวหรือมากกว่า แต่โปรแกรมที่เริ่มต้นด้วยร้านค้าว่างเปล่าจะสร้างร้านค้าว่างเปล่า โปรแกรมที่ไม่ทำอะไรเลยสามารถผกผันได้อย่างง่ายดาย และไม่น่าสนใจในทางปฏิบัติ

การประกาศตัวแปรจะกำหนดค่าให้กับตัวแปรหรืออาร์เรย์หนึ่งมิติ:

< v-decl > ::= < v > | < v > "[" < c > "]" 

โปรดทราบว่า การประกาศตัวแปรไม่มีข้อมูลประเภท เนื่องจากค่าทั้งหมด (และค่าคงที่ทั้งหมด) ใน Janus เป็นจำนวนเต็ม 32 บิตที่ไม่เป็นลบ ดังนั้นค่าทั้งหมดจึงอยู่ระหว่าง 0 และ 2³² ⁻ 1 = 4294967295 อย่างไรก็ตาม โปรดทราบว่าตัวแปลภาษา Janus ที่โฮสต์โดยTOPPSใช้ จำนวนเต็ม 32 บิต แบบสองส่วนเติม เต็มปกติ ดังนั้นค่าทั้งหมดในนั้นจึงอยู่ระหว่าง −2³¹ ⁼ −2147483648 และ^2³¹ − 1 = 2147483647 ตัวแปรทั้งหมดจะถูกกำหนดค่าเริ่มต้นเป็น 0

ไม่มีข้อจำกัดทางทฤษฎีเกี่ยวกับขนาดของอาร์เรย์ แต่ตัวแปลดังกล่าวต้องการขนาดอย่างน้อย 1 ^{[ 4 ]}

การประกาศขั้นตอนการทำงานประกอบด้วยคำหลักprocedureตามด้วยตัวระบุขั้นตอนการทำงานที่ไม่ซ้ำกัน และคำสั่ง:

<p-decl> :: = " ขั้นตอน " <id> <s>​​

จุดเริ่มต้นของโปรแกรม Janus คือขั้นตอนการทำงานที่มีชื่อว่าmainหากไม่มีขั้นตอนการทำงานดังกล่าว ขั้นตอนการทำงานสุดท้ายในข้อความของโปรแกรมจะเป็นจุดเริ่มต้นของโปรแกรม

คำสั่งอาจเป็นได้ทั้งการกำหนดค่า การสลับค่า เงื่อนไข if-then-else ลูป การเรียกใช้โปรแกรมย่อย การยกเลิกการเรียกใช้โปรแกรมย่อย การข้าม หรือลำดับของคำสั่ง:

< s >  := < x > < mod-op > "=" < e > | < x > "[" < e > "]" < mod-op > "=" < e > | < x > " < = > " < x > | "if" < e > "then" < s > "else" < s > "fi" < e > | "from" < e > "do" < s > "loop" < s > "until" < e > | "call" < id > | "uncall" < id > | "ข้าม" | < s > < s >

เพื่อให้การกำหนดค่าสามารถย้อนกลับได้ จำเป็นที่ตัวแปรทางด้านซ้ายมือจะต้องไม่ปรากฏในนิพจน์ทั้งสองด้านของการกำหนดค่า (หมายเหตุ การกำหนดค่าให้กับเซลล์ในอาร์เรย์จะมีนิพจน์อยู่ทั้งสองด้านของการกำหนดค่า)

การสลับ ( <x> "<=>" <x>) สามารถย้อนกลับได้อย่างง่ายดาย

เพื่อให้เงื่อนไขสามารถย้อนกลับได้ เราจึงมีทั้งการทดสอบ ( <e>หลังจาก"if") และการยืนยัน ( <e>หลังจาก"fi") ความหมายคือ การทดสอบต้องเป็นจริงก่อนการทำงานของส่วน then และการยืนยันต้องเป็นจริงหลังจากนั้น ในทางกลับกัน การทดสอบต้องไม่เป็นจริงก่อนการทำงานของส่วน else และการยืนยันต้องไม่เป็นจริงหลังจากนั้น ในโปรแกรมที่กลับด้าน การยืนยันจะกลายเป็นการทดสอบ และการทดสอบจะกลายเป็นการยืนยัน (เนื่องจากค่าทั้งหมดใน Janus เป็นจำนวนเต็ม จึงใช้ความหมายตามแบบฉบับของภาษา C ที่ 0 หมายถึงเท็จ)

เพื่อให้ลูปสามารถย้อนกลับได้ เราจึงต้องเพิ่มเงื่อนไขยืนยัน ( <e>after "from") และเงื่อนไขทดสอบ ( <e>after "until") เข้าไปด้วย หลักการคือ เงื่อนไขยืนยันจะต้องเป็นจริงเฉพาะตอนเข้าสู่ลูป และเงื่อนไขทดสอบจะต้องเป็นจริงเฉพาะตอนออกจากลูป ในโปรแกรมที่กลับด้าน เงื่อนไขยืนยันจะกลายเป็นเงื่อนไขทดสอบ และเงื่อนไขทดสอบจะกลายเป็นเงื่อนไขยืนยัน เงื่อนไข<e>after เพิ่มเติม "loop"จะช่วยให้สามารถทำงานต่อหลังจากที่เงื่อนไขทดสอบเป็นเท็จได้ การทำงานนั้นจะต้องทำให้เงื่อนไขยืนยันเป็นเท็จในภายหลัง

การเรียกใช้โปรซีเดอร์จะดำเนินการตามคำสั่งของโปรซีเดอร์ในทิศทางไปข้างหน้า การยกเลิก การ เรียกใช้โปรซีเดอร์จะดำเนินการตามคำสั่งของโปรซีเดอร์ในทิศทางย้อนกลับ โปรซีเดอร์ไม่มีพารามิเตอร์ ดังนั้นการส่งผ่านตัวแปรทั้งหมดจึงทำผ่านผลข้างเคียงในหน่วยความจำส่วนกลาง

นิพจน์ คือ ค่าคงที่ ( จำนวนเต็ม ) ตัวแปร ตัวแปรที่มีดัชนี หรือการประยุกต์ใช้การดำเนินการทวิภาค :

< อี> ::= < ค> | < x > | < x > "[" < e > "]" | < e > < bin-op > < e >

ค่าคงที่ใน Janus (และตัวแปลภาษา Janus ที่โฮสต์โดยTOPPS ) ได้มีการกล่าวถึงไปแล้วข้างต้น

ตัวดำเนินการไบนารีคือตัวดำเนินการประเภทใดประเภทหนึ่งต่อไปนี้ ซึ่งมีความหมายคล้ายคลึงกับตัวดำเนินการไบนารีในภาษาซี:

<bin-op> :: = "+" | "-" | "^" | "*" | "/" | "%" | "&" | "|" | "&&" | "||" | ">" | "<" | "=" | "!=" | " < =" | " > =" 

ตัวดำเนินการปรับเปลี่ยนเป็นส่วนย่อยของตัวดำเนินการไบนารี โดยที่สำหรับทุก v จะเป็นฟังก์ชันหนึ่งต่อหนึ่งทั่วถึง และดังนั้นจึงสามารถผกผันได้ โดยที่เป็นตัวดำเนินการปรับเปลี่ยน: ${\displaystyle \lambda v'.\oplus \left(v',v\right)}$${\displaystyle \oplus }$

< mod-op > ::= "+" | "-" | "^" 

ฟังก์ชันผกผันคือ"-", "+", และ"^"ตามลำดับ

ข้อจำกัดที่ว่าตัวแปรที่กำหนดค่าให้จะต้องไม่ปรากฏในนิพจน์ใดๆ ทั้งสองด้านของการกำหนดค่า ทำให้เราสามารถพิสูจน์ได้ว่าระบบการอนุมานของ Janus เป็นแบบกำหนดได้ทั้งไปข้างหน้าและย้อนกลับ

ภาษา Janus ได้รับการคิดค้นขึ้นครั้งแรกที่ Caltech ในปี 1982 งานวิจัยต่อมาได้กำหนดความหมายของภาษาอย่างเป็นทางการในรูปแบบของความหมายตามธรรมชาติและความหมายเชิงสัญลักษณ์ [ ^{10 ] ความ}หมายของภาษาโปรแกรมที่ย้อนกลับได้อย่างสมบูรณ์ยังสามารถจัดการแบบย้อนกลับได้ในระดับเมตาด้วย

เราเขียนขั้นตอนวิธี Janus fibเพื่อหาจำนวนฟิโบนาชชีลำดับที่nสำหรับ n>2, i=n, ​​x1=1 และ x2=1:

ขั้นตอน fib จาก i = n ทำ x1 += x2 x1 <=> x2 i -= 1 จนกระทั่ง i = 2 

เมื่อสิ้นสุดการทำงานx1จะเป็นจำนวนฟิโบนาชชีลำดับที่ ( n − 1) และx2จะเป็นจำนวนฟิโบนาชชี^{ลำดับ ที่ n} iเป็น ตัวแปร ตัววนซ้ำที่ตั้งแต่nถึง 2 เนื่องจากiลดลงในทุกการวนซ้ำ สมมติฐาน ( i = n) จึงเป็นจริงเฉพาะก่อนการวนซ้ำครั้งแรกเท่านั้น การทดสอบ ( i = 2) เป็นจริงเฉพาะหลังจากการวนซ้ำครั้งสุดท้ายของลูป (โดยสมมติว่าn > 2)

โดยสมมติว่าขั้นตอนเบื้องต้นเป็นไปตามนี้ เราจะได้เลขฟิโบนาชี่ลำดับที่ 4 ดังนี้x2:

ใน x1 x2 ขั้นตอนหลัก n += 4 i += n x1 += 1 x2 += 1 เรียกโกหก 

โปรดทราบว่า ฟังก์ชันหลักของเราจะต้องทำงานเพิ่มเติมอีกเล็กน้อยหากเราต้องการให้รองรับ n≤2 โดยเฉพาะอย่างยิ่งจำนวนเต็มลบ

สิ่งที่ตรงข้ามกับfibคือ:

ขั้นตอน fib จาก i = 2 ทำ i += 1 x1 <=> x2 x1 -= x2 วนซ้ำ จนกระทั่ง i = n 

ดังที่คุณเห็น โปรแกรม Janus สามารถแปลงได้โดยการผกผันเฉพาะที่ โดยที่การทดสอบและการยืนยันในลูปจะถูกสลับกัน ลำดับของคำสั่งจะถูกกลับด้าน และคำสั่งทุกคำสั่งในลูปเองก็จะถูกกลับด้านเช่นกัน โปรแกรมผกผันนี้สามารถใช้เพื่อหาค่าnเมื่อx1 เป็น ^{จำนวน} ฟิโบนาชชีลำดับ ที่ (n-1) และx2เป็นจำนวนฟิโบนาชชีลำดับ ^{ที่ n}