Lập trình khai báo: sự thật, quy tắc và mục tiêu
Đã giới thiệu| English | Ý nghĩa |
|---|---|
| fact/fækt/ | Sự thật |
| declarative programming/dɪˈklærətɪv ˈprəʊɡræmɪŋ/ | Lập trình khai báo |
| rule/ruːl/ | Quy tắc |
| goal/ɡəʊl/ | Mục tiêu |
| backtrack/ˈbæktræk/ | Hồi quy |
| unification/ˌjuːnɪfɪˈkeɪʃn/ | Thống nhất hóa |
Hỏi ai có thể mượn máy ảnh
- Một câu lạc bộ truyền thông lưu giữ thông tin về thành viên và khóa đào tạo đã hoàn thành. Họ muốn hỏi ai có thể mượn máy ảnh mà không cần viết một vòng lặp mới cho mỗi câu hỏi.
- Lập trình khai báo mô tả sự thật, luật lệ và một mục tiêu. Bộ xử lý logic tìm kiếm các giá trị làm cho mục tiêu đúng. Lập trình viên vẫn phải viết các luật chính xác; bộ xử lý không đọc suy nghĩ hay bảng thông báo của câu lạc bộ.
Sự thật nêu rõ những gì đã biết
- Một sự thật là một khẳng định trong cơ sở tri thức. Trong
member(aya)., vị từmemberliên kết một người với việc trở thành thành viên câu lạc bộ.trained(aya, camera).liên kết một người với một thiết bị. - Bài học này sử dụng ký hiệu kiểu Prolog: tên viết thường là hằng hoặc vị từ; tên viết hoa là biến. Dấu chấm cuối câu kết thúc mỗi sự thật hoặc luật.
member(aya).
member(ben).
member(chen).
trained(aya, camera).
trained(chen, camera).
trained(ben, audio).
Cho biết các sự thật member(ben). và trained(ben, audio)., phát biểu nào dưới đây là một sự thật được cung cấp?
Difficulty 1/5 · 100 coins + a small bonus on first completion today
member(ben). được đưa ra trực tiếp. Cơ sở tri thức không bao gồm việc huấn luyện camera cho Ben.
Một luật kết hợp các điều kiện
- Một luật quy định khi nào một kết luận được coi là đúng. Đọc
:-như “nếu” và dấu phẩy là VÀ: một người có thể mượn máy ảnh nếu họ là thành viên và đã được đào tạo về máy ảnh. Personchỉ cùng một biến ở cả ba vị trí. Bộ xử lý phải tìm một giá trị duy nhất thỏa mãn cả hai điều kiện, chứ không phải một thành viên và một người đã được đào tạo khác nhau.
can_borrow(Person, camera) :- member(Person), trained(Person, camera).
Trong quy tắc can_borrow(Person, camera) :- member(Person), trained(Person, camera)., dấu phẩy giữa hai điều kiện có nghĩa là ____.
Difficulty 1/5 · 100 coins + a small bonus on first completion today
Cả thành viên và huấn luyện camera đều phải đúng cho cùng một Người.
Mục tiêu đặt ra một câu hỏi
- Mục tiêu
?- can_borrow(aya, camera).yêu cầu kết quả có/không. Bộ xử lý khớp với luật và kiểm tramember(aya)vàtrained(aya, camera): cả hai sự thật đều tồn tại, nên mục tiêu thành công. - Mục tiêu
?- can_borrow(Person, camera).yêu cầu các phép gán của biến. Với cơ sở tri thức này, các câu trả lời làPerson = ayavàPerson = chen. Đây là các mục tiêu cần suy luận; các khối hiển thị chỉ là ký hiệu, không phải môi trường chạy thử thực tế.
Các thành viên câu lạc bộ là aya, ben và chen. Aya và Chen được huấn luyện về camera; Ben chỉ được huấn luyện âm thanh. Quy tắc can_borrow(Person, camera) yêu cầu cả thành viên và huấn luyện camera. Ai thỏa mãn can_borrow(Person, camera)?
Difficulty 2/5 · 140 coins + a small bonus on first completion today
Aya và Chen có cả hai sự thật cần thiết. Ben chỉ có huấn luyện âm thanh.
Biến Person trong member(Person) có thể mang một giá trị khác với Person trong trained(Person, camera) trong cùng một lần chứng minh.
Difficulty 1/5 · 100 coins + a small bonus on first completion today
Tất cả các xuất hiện của cùng một biến phải giữ nguyên liên kết giống nhau trong lần chứng minh đó.
Ví dụ minh họa: truy vết một ứng viên thất bại
- Bắt đầu từ
Person = ben.member(ben)thành công.trained(ben, camera)thất bại: sự thật về khóa học khả dụng dành cho âm thanh, không khớp với máy ảnh. - Bộ xử lý lùi lại để thử một ứng viên khác,
Person = chen. Cả hai điều kiện đều thành công. Nếu yêu cầu thêm câu trả lời, nó sẽ tiếp tục tìm kiếm; nếu không còn ứng viên nào, sẽ không còn câu trả lời nữa.
Theo dõi quá trình tìm kiếm còn lại sau khi Aya đã được trả về.
Difficulty 3/5 · 200 coins + a small bonus on first completion today
Ben là thành viên nhưng thiếu một sự kiện khớp về việc đào tạo camera; sau đó động cơ sẽ thử Chen.
Khớp chia sẻ giá trị trên một luật
- Thống nhất hóa khớp các thuật ngữ trong khi liên kết các biến một cách nhất quán. Khớp
trained(Person, camera)vớitrained(chen, camera)sẽ gánPersonchochen; nhưng khớp nó vớitrained(ben, audio)sẽ thất bại vì thiết bị khác nhau. - Một mục tiêu thất bại có nghĩa là không thể chứng minh từ những sự thật và luật này. Nó không chứng minh rằng Ben chưa bao giờ dùng máy ảnh trong đời thực; cơ sở tri thức có thể đơn giản là chưa đầy đủ.
Việc khớp trained(Person, camera) với trained(chen, camera) gán Person cho ____.
Difficulty 1/5 · 100 coins + a small bonus on first completion today
Thiết bị khớp và đối số đầu tiên cung cấp liên kết chen.
Ví dụ minh họa: viết một luật mới
- Yêu cầu: một cố vấn chỉ có thể giúp đỡ ai đó khi cố vấn đó có đào tạo về máy ảnh và người học là thành viên. Thêm luật bên dưới, sau đó hỏi
?- can_help(aya, ben).. trained(aya, camera)vàmember(ben)đều tồn tại, nên mục tiêu thành công. Luật này cho phép Aya tự giúp mình. Nếu việc tự giúp phải bị loại trừ, yêu cầu cần thêm một điều kiện nữa; đừng tự ý thêm vào mà không báo trước.
can_help(Mentor, Learner) :- trained(Mentor, camera), member(Learner).
Cho biết trained(aya, camera). và member(ben)., cùng quy tắc can_help(Mentor, Learner) :- trained(Mentor, camera), member(Learner)., liệu can_help(aya, ben) có thành công không?
Difficulty 1/5 · 100 coins + a small bonus on first completion today
Aya có đào tạo camera và Ben là thành viên; Ben không cần phải có đào tạo camera để trở thành người học.
Điểm số dễ mất
- Một sự thật nêu lên điều gì đó đã biết; một luật rút ra kết luận khi các điều kiện của nó được đáp ứng; một mục tiêu hỏi xem một kết luận có thể được chứng minh hay không, hoặc những giá trị nào làm cho nó đúng.
- Giữ cho các biến lặp lại nhất quán.
member(X), trained(Y, camera)sẽ cho phép một thành viên chưa được đào tạo đủ điều kiện vì có người khác đã có đào tạo. Thay đổi tên biến có thể thay đổi ý nghĩa của luật.
Từ yêu cầu đến chứng minh
- Viết các sự thật, dịch mỗi yêu cầu thành một luật, và đặt một mục tiêu. Truy vết mỗi phép gán biến qua từng điều kiện và thử các phương án khác khi một ứng viên thất bại.
- Chỉ có Aya và Chen mới có thể mượn máy ảnh. Khóa học âm thanh của Ben không phải là đào tạo về máy ảnh. Kết quả tuân theo cơ sở tri thức đã cung cấp, không phải dựa trên phỏng đoán về con người thực.
Các thành viên câu lạc bộ bao gồm Aya, Ben và Chen. Aya và Chen đã được đào tạo về camera; Ben chỉ được đào tạo âm thanh. Quy tắc can_borrow(Person, camera) yêu cầu cả thành viên và đào tạo camera. Có bao nhiêu người thỏa mãn can_borrow(Person, camera)?
Difficulty 2/5 · 140 coins + a small bonus on first completion today
Aya và Chen là hai giải pháp.
Một mục tiêu thất bại chứng minh rằng sự kiện tương ứng chưa từng xảy ra bên ngoài cơ sở tri thức này.
Difficulty 1/5 · 100 coins + a small bonus on first completion today
Lỗi có nghĩa là mục tiêu không thể chứng minh được từ các dữ liệu và quy tắc hiện có.