Memprogram bahasa dengan fungsi kanonik

Apakah ada bahasa pemrograman (fungsional?) Di mana semua fungsi memiliki bentuk kanonik? Yaitu, setiap dua fungsi yang mengembalikan nilai yang sama untuk semua rangkaian input direpresentasikan dengan cara yang sama, misalnya jika f (x) mengembalikan x + 1, dan g (x) mengembalikan x + 2, maka f (f (x) )) dan g (x) akan menghasilkan executable yang tidak bisa dibedakan ketika program dikompilasi.

Mungkin yang lebih penting, di mana / bagaimana saya dapat menemukan lebih banyak informasi tentang representasi kanonik program (Googling "program representasi kanonik" kurang bermanfaat)? Sepertinya pertanyaan alami untuk ditanyakan, dan saya khawatir saya tidak tahu istilah yang tepat untuk apa yang saya cari. Saya ingin tahu apakah mungkin untuk bahasa seperti itu menjadi Turing lengkap, dan jika tidak, seberapa ekspresif bahasa pemrograman yang Anda miliki, sambil tetap mempertahankan properti seperti itu.

Latar belakang saya agak terbatas, jadi saya lebih suka sumber dengan prasyarat lebih sedikit, tetapi referensi ke sumber yang lebih maju mungkin keren juga, karena dengan begitu saya akan tahu apa yang ingin saya kerjakan.

Sejauh mana hal ini dimungkinkan sebenarnya merupakan pertanyaan terbuka utama dalam teori kalkulus lambda. Berikut ringkasan singkat dari apa yang diketahui:

• Kalkulus lambda yang diketik sederhana dengan unit, produk, dan ruang fungsi memang memiliki properti bentuk kanonik sederhana. Dua istilah sama jika dan hanya jika mereka memiliki bentuk beta-normal, eta-panjang yang sama. Menghitung bentuk-bentuk normal ini juga cukup mudah.

• Penambahan tipe penjumlahan sangat memperumit masalah. Masalah kesetaraan masih dapat diputuskan (kata kunci untuk mencari adalah "kesetaraan coproduct"), tetapi algoritma yang dikenal bekerja untuk alasan yang sangat rumit dan setahu saya tidak ada teorema bentuk normal yang sepenuhnya memuaskan. Inilah empat pendekatan yang saya tahu:

  • Neil Ghani, Beta-Eta Equality for Coproducts , TLCA 1995.
  • Vincent Balat, Roberto di Cosimo, Marcelo Fiore, Normalisasi ekstensional dan evaluasi parsial tipe-diarahkan untuk kalkulus lambda diketik dengan jumlah , POPL 2004.
  • Sam Lindley, Menulis Ulang Ekstensional dengan Sums, TLCA 2007.
  • Arbob Ahmad, Daniel R. Licata, dan Robert Harper, Prosedur Pengambilan Bukti-Teori untuk Finitary Lambda-Calculus . WMM 2007.

• Penambahan tipe yang tidak terikat, seperti bilangan asli, membuat masalah tidak dapat diputuskan. Pada dasarnya, Anda sekarang dapat menyandikan masalah kesepuluh Hilbert.

• Penambahan rekursi membuat masalah tidak dapat diputuskan, karena memiliki bentuk normal membuat kesetaraan dapat diputuskan, dan itu akan memungkinkan Anda memecahkan masalah penghentian.