Bằng chứng Tam giác Cân
Một trong những kết quả nổi bật nhất từ nghiên cứu suy luận máy tính sơ khai: một chương trình chứng minh định lý hình học đã tạo ra một bằng chứng của định lý tam giác cân mà các nhà thiết kế của nó không thể dự đoán được, & mà hầu hết các nhà toán học không biết.
Bằng chứng cổ điển yêu cầu xây dựng một đường phụ trợ: vẽ đường phân giác góc từ đỉnh, sử dụng sự đồng dạng SAS trên hai tam giác con. Bằng chứng có hiệu lực nhưng yêu cầu một cấu trúc bên ngoài mà vấn đề ban đầu không đề cập.
Bằng chứng của chương trình không sử dụng bất kỳ cấu trúc phụ trợ nào. Nó so sánh tam giác ABC với tam giác CBA — cùng một tam giác, được đọc ngược. Sự tương ứng A↔A, B↔C, C↔B biến tam giác ban đầu thành chính nó với các đỉnh cơ sở được hoán đổi. Cả hai cạnh đều bằng nhau theo giả thuyết. Theo sự đồng dạng SSS, tam giác ABC đồng dạng với tam giác CBA, có nghĩa là góc B bằng góc C.
Bằng chứng này xuất hiện như một chú thích trong một số phiên bản của Euclid, nhưng nó không được biết rộng rãi. Các lập trình viên đã xây dựng hệ thống này không biết nó. Chương trình tìm thấy nó bằng cách tuân theo một chiến lược được lập trình: thử chứng minh trực tiếp trước; nếu bị kẹt, hãy thử vẽ các đường phụ trợ.
Chương trình Có Thể hiện Sáng tạo không?
Hamming đặt câu hỏi trực tiếp: điều này có cấu thành sáng tạo của máy tính không? Câu trả lời của ông: một phần, & sự hạn chế rất quan trọng.
Các lập trình viên đã viết hướng dẫn để thử chứng minh định lý trực tiếp, & khi bị kẹt hãy thử xây dựng phụ trợ. Chương trình tuân theo những hướng dẫn đó. Bằng chứng mới nổi lên từ việc áp dụng những hướng dẫn đó vào một vấn đề nơi chứng minh trực tiếp xảy ra hoạt động một cách thanh lịch.
Quan sát của Hamming: chính xác đó là cách sáng tạo hoạt động ở con người. Đào tạo hình học của bạn đã tải một chương trình vào bạn. Các hướng dẫn nói: thử chứng minh trực tiếp; nếu bị kẹt, vẽ các đường phụ trợ. Bạn học những hướng dẫn đó kém sạch sẽ hơn một máy tính làm — bạn quên, áp dụng sai, & cần lặp lại vô tận. Nhưng cấu trúc là giống nhau.
Nghịch lý Hamming đặt tên: khi một chương trình tồn tại để làm một cái gì đó, những người quan sát tự động phân loại lại hành vi là thường lệ. Sự tồn tại của chương trình phá hủy ấn tượng về trí thông minh. Một máy tính không bao giờ có thể chứng minh, trước một khán giả hoài nghi, rằng nó nhiều hơn một máy tính — bởi vì bất kỳ chứng minh nào đều bị phân loại lại thành 'chỉ là lập trình'.
Max Mathews & Âm nhạc Máy tính
Hamming chuyển từ hình học sang âm nhạc, & sự chuyển tiếp này là cố ý: ông muốn chỉ ra rằng suy luận máy tính mở rộng ngoài các lĩnh vực rõ ràng là phân tích.
Max Mathews & John Pierce tại Bell Labs đã tính toán âm nhạc bằng cách tổng hợp hình sóng kỹ thuật số. Hệ thống yêu cầu chọn tốc độ lấy mẫu: theo định lý Nyquist, để tái tạo âm thanh lên đến tần số f, bạn cần tốc độ lấy mẫu ít nhất 2f. Thính giác của con người kéo dài đến khoảng 18.000 Hz; chất lượng giọng nói điện thoại cần 8.000 Hz, yêu cầu tốc độ lấy mẫu ít nhất 16.000 Hz.
Với tốc độ lấy mẫu cố định, hệ thống có thể tính toán bất kỳ chuỗi biên độ nào đại diện cho bất kỳ hình sóng có thể nào, chuyển các giá trị qua bộ chuyển đổi tương tự-kỹ thuật số & bộ lọc làm mịn, & phát lại kết quả. Tones thuần chất là các sóng sin đơn giản. Các nhạc cụ kết hợp nhiều tần số với các bao giác tham và suy giảm đặc trưng. Thành phố trở thành một vấn đề xác định các chuỗi nốt nhạc & các mô hình nhạc cụ.
Họ sau đó hỏi: tại sao cung cấp các nốt nhạc theo cách thủ công? Các quy tắc của thành phố tồn tại. Họ sử dụng những quy tắc đó cộng với tạo số ngẫu nhiên để tạo ra âm nhạc được tạo thành bởi máy tính.
Kết quả: âm nhạc được tạo thành bởi máy tính, được phát lại bởi máy tính đã xuất hiện trong quảng cáo trên radio & TV trong giữa những năm 1970. Bản ghi 'chất lượng cao nhất' năm 1994 là kỹ thuật số. Quan sát của Hamming: bây giờ đó là vấn đề loại âm thanh nào đáng được tạo ra, không phải những âm thanh nào về mặt kỹ thuật là có thể. Biên giới kỹ thuật đã đóng; biên giới thẩm mỹ vẫn mở.
Biên giới Kỹ thuật Đã Đóng
Hamming đưa ra một yêu cầu sắc nét: với âm thanh kỹ thuật số, không thể có những cải tiến kỹ thuật đáng kể trong tương lai cho tái tạo âm thanh. Phương tiện đã đạt được tính hoàn chỉnh về mặt lý thuyết. Những cải tiến còn lại là về thẩm mỹ, không phải kỹ thuật.
Ông quan sát rằng các hệ thống âm nhạc máy tính cũng thay đổi vai trò của nhà soạn nhạc: phát lại thời gian thực thay thế những năm dài chờ đợi để biểu diễn trực tiếp. Một nhà soạn nhạc bây giờ có thể phát triển phong cách nhanh hơn vì chu kỳ phản hồi có độ dài nhỏ hơn nhiều bậc độ lớn.
Công việc Thường lệ & Vấn đề Khả năng
Hamming không e ngại câu hỏi thay thế lao động. Máy tính thay thế công nhân khỏi công việc thường lệ. Ông nêu điều này một cách rõ ràng: 'các robot sẽ thay thế nhiều con người làm công việc thường lệ. Theo một cách rất thực tế, máy tính có thể tốt nhất làm công việc thường lệ, do đó giải phóng con người cho công việc nhân đạo hơn.'
Sự hạn chế không thoải mái: 'thật không may, nhiều con người hiện tại không được trang bị để cạnh tranh với máy tính — họ không thể làm gì nhiều hơn công việc thường lệ.'
Ông bày tỏ nghi ngờ rằng hầu hết mọi người có thể được đào tạo lại từ công việc thường lệ sang công việc không thường lệ. Đây không phải là một vị trí phổ biến. Ông thừa nhận niềm tin phổ biến (hy vọng, ông nói) rằng đào tạo đúng sẽ để cho công nhân bị thay thế cạnh tranh. Ông công khai nghi ngờ điều đó, sau đó tiếp tục.
Thuộc tính Phân biệt
Những gì phân biệt công việc không thường lệ khỏi công việc thường lệ, trong khuôn khổ của Hamming: khả năng phân tích một tình huống cẩn thận & xác định chi tiết những gì nên được thực hiện tiếp theo. Đó chính xác là những gì một chương trình làm — & những gì máy tính ngày càng có thể làm. Câu hỏi là liệu tập hợp các tình huống yêu cầu xác định con người có đang shrink hay phát triển không.
Vấn đề Khả năng
Sự nghiệp của Hamming tại Bell Labs đã cho phép quan sát trực tiếp: trong nhiều thập kỷ, công việc được thay thế khỏi sự chú ý con người bởi máy tính liên tục skew hướng tới thường lệ, & công việc mới xuất hiện skew hướng tới không thường lệ. Giá trị con người còn lại nằm trong phán đoán, tổng hợp, & lựa chọn những vấn đề nào cần theo đuổi — không phải trong thực hiện.
Ông đưa ra nhưng không giải quyết: mô hình này có phải là vĩnh viễn không, hay tự động hóa cuối cùng cũng tiêu thụ không thường lệ?
Hợp tác Con người-Máy tính
Khung ưa thích của Hamming cho suy luận máy tính không phải là cạnh tranh mà là hợp tác. Ông quan tâm đến những gì con người & máy tính có thể làm cùng nhau mà không ai có thể làm một mình.
Ví dụ ông thấy tại Bell Labs: hệ thống đơn giản hóa đại số hướng dẫn các nhà toán học đại số qua các phép thao tác ký hiệu dài trong khi để lại các lệnh gọi phán đoán cho con người; hệ thống âm nhạc máy tính mở rộng sức mạnh sáng tạo của nhà soạn nhạc trong khi để lại lựa chọn thẩm mỹ cho nhà soạn nhạc; hệ thống hỗ trợ chẩn đoán y tế kết hợp nhận dạng mẫu máy tính với phán đoán bối cảnh con người.
Dự đoán của ông: công việc có giá trị nhất trong những thập kỷ sắp tới nằm ở giao diện — không phải con người được thay thế bởi máy tính, & không phải máy tính bị hạn chế bởi con người, mà sự kết hợp vượt quá cả hai.
Chương trình tổng hợp hóa học là một ví dụ rõ ràng: nó liệt kê các tuyến đường tổng hợp có thể, tính toán chi phí & năng suất, & trình bày các tùy chọn. Nhà hóa học chọn. Không ai một mình sẽ làm cũng như vậy: chương trình không thể nhận ra tổng hợp nào là thanh lịch hoặc sản phẩm phụ nào quan trọng để sử dụng hạ lưu; nhà hóa học không thể liệt kê 10.000 tuyến đường bằng tay.