KB 2 — Value property dan total value

Kembali ke bagian induk

Cerita pengantar — penjelasan tambahan, data simulasi. Ani diberi nomor 1. Pengurus mengganti nama objek pada sebuah aturan dengan nama lain yang juga menunjuk nomor 1. Nilai aturan dapat tetap sama bila arti hubungan dan bagian lain tetap. Tetapi mengganti satu dari dua pemunculan sambil mengubah arti pemunculan yang tersisa dapat merusak hasil.

Dari cerita ke notasi dan konsep BMP. Sifat nilai menghubungkan nilai ekspresi yang diganti, nilai pengganti, kesepakatan interpretasi pada simbol lain, dan keamanan cakupan. Untuk substitusi term bebas yang aman, nilai $F [t / x]$ pada I sama dengan nilai F pada $I [x \leftarrow \llbracket t \rrbracket_{I}]$ . Tanda $\llbracket t \rrbracket_{I}$ berarti objek hasil menghitung t pada I. Formula ini adalah penulisan penjelas sifat nilai, dengan penggantian semua pemunculan bebas x dan tanpa capturing.

Contoh manual tanpa kuantifier: $F = q (x, x)$ , q berarti kesamaan, dan nilai term t=1. Mengganti total x dengan t menghasilkan $q (t, t)$ yang benar. Ini cocok dengan F di bawah x=1, yaitu $1 = 1$ . Tetapi mengganti sebagian menjadi $q (x, t)$ dengan x=2 memberi $2 = 1$ , salah. Nilai pengganti sama belum cukup; pemunculan yang tersisa juga harus memenuhi syarat agreement yang relevan.

Untuk melakukan substitusi aman: tandai sasaran dan pemunculannya; identifikasi variabel bebas dalam pengganti; periksa kuantifier yang akan dilewati; lakukan renaming bila diperlukan; lalu jalankan total/parsial sesuai instruksi. Untuk substitusi formula, periksa pula bahwa simbol predikat dan fungsi tetap dipakai dengan jenis hasil yang benar.