이상규
가입: 2026년 3월 4일 올린 글: 7 위치: 대한민국 서울
|
올려짐: 2026년4월15일 1:21 주제: [숙제 4] Record의 Equality |
|
|
안녕하세요,
Record는 structural equality로 확인한다고 하셨는데, 이와 관련해 질문 드립니다.
1. k-.pdf 상에서 어떤 메모리로 equality를 확인하는지가 불분명합니다.
를 이용한다고 생각하면 될까요?
2. 무한히 재귀적인 record에서 equality는 어떻게 정의되나요?
예컨대 아래 코드의 실행 결과는 "1\n1\n1\n"이 되어야 하나요?
| 코드: | let r1 := {next := {}} in
let r2 := {next := {}} in
let r3 := {next := {}} in
r1.next := r2;
r2.next := r3;
r3.next := r2;
write(if r1 = r1 then 1 else 0);
write(if r1.next = r1 then 1 else 0);
write(if r1 = r2 then 1 else 0)
|
r1 = r1은 어느 면으로 보나 참이어야 하고,
r1.next = r1은 조금 어색하지만 무한히 긴 리스트이므로 참이라고 생각됩니다.
마지막은 양쪽이 다 가능해 보입니다.
| 인용: |
레코드가 같은지 비교할 때에는 구조가 재귀적으로 같은지(structural equality) 확인합니다. 즉 r1, r2이 같은 field를 갖고 있고, 각 field의 값이 서로 같을 때 r1과 r2는 같다고 합니다.
|
이 정의를 충실히 따른다면 r1과 r2는 같은 field인 next를 갖고 있고, 그 값인 r1과 r3가 같은지 보아야 합니다. r1과 r3는 같은 field인 next를 갖고 있고, 그 값인 r1과 r2가 같은지 보아야 합니다. 이것이 무한히 반복되므로 r1 = r2는 참입니다.
그러나 아래의 두 조작을 가했을 때 나타나는 결과는 다릅니다. r1.next.next = {} 이후에 r1은 {next := {}}이 되지만, r2.next.next = {} 이후에 r2는 {next := {next := {}}이 됩니다. 조작을 가한 결과가 다르므로 두 record의 "구조가 다르다"고 볼 수도 있습니다.
equality의 의미를 보다 엄밀하게 정의해주실 수 있을까요?
감사합니다.
이상규 올림 |
|