[이도형]

안녕하세요!

오늘 수업 내용 관련해서 이해가 잘 안되는 점이 있어 질문드립니다

σ,M⊢C⇒M′

위의 식이 특정 환경, 메모리 상태에서 Statement를 수행 시 M'를 만들어낸다라는 의미로 이해했는데요. 그렇다면 Statement 수행 후 환경(시그마)은 바뀌지 않는것인가요??
x:= E와 같은 statement를 수행하면 Env에 x와 x에 해당하는 메모리 주소 값이 생길 수도 있는 것 아닌가요?

오늘 교수님이 SEQ 설명하실 때 S1 ; S2에서 S1을 실행 후 메모리 공간은 변하여서 S2에서 이 변경된 메모리 공간이 적용되는데 환경은 S1, S2 둘 다 동일하다고 설명하신 부분이 잘 이해가 되지 않아 질문드렸습니다.

제가 잘못 이해했거나 놓친 부분이 있는 것 같습니다.

감사합니다!!

[김두영]

환경은 메모리 주소를 가리키는 개념이고 메모리 주소에 적혀있는 값은 환경이 변하지 않아도 바뀔 수 있는 것 같습니다. 새로운 환경이 만들어진다는건 어떤 변수(심볼)가 가리키는 메모리 주소가 변하는 경우일 거구요.

예를 들어서
let x := 1 in
x := x + 1
x := x + 2
를 실행하면 let x := 1 을 실행할때 기존에 있던 환경(σ)에 (x, l) 이라는 걸 추가한 환경(σ')이 리턴되고 (x는 심볼(변수이름), l은 메모리 주소, l이 가리키는 메모리 값이 1), 밑의 SEQ(x := x + 1 ; x:= x + 2)를 실행할때는 둘 다 σ'이라는 환경을 사용하고 x가 가리키는 값(메모리주소)은 l로 변함없지만 l이라는 메모리주소에 담긴 값이 1->2->4로 변하는거라고 이해했습니다.
(만약 이 이후에 let x := 2 in 이라는 문장이 있다면 이게 실행될때는 환경 σ'과는 달리 x가 l'을 가리키는 환경 σ''이 생기고, 이때 l'이라는 메모리 주소는 2라는 값을 가리키고 있겠죠.)

[로파스]

안녕하세요.

김두영 수강생님이 기본적으로 잘 설명해주셨는데요, 약간의 보충설명을 드리겠습니다.

결론부터 말하자면 프로그램(C) 실행결과로 환경이 바뀔 수 있는 것이 맞고,

S1;S2에서 S1과 S2의 환경이 동일하다는 것도 맞습니다.

김두영 수강생님이 제시해주신 예제를 조금 변형해 아래와 같은 식을 생각해보겠습니다.

(let x = 1 in x := x+1); x := x+2

를 실행할때, let x = 1 in x := x + 1 을 실행할때의 환경이 σ라고 하면
(이 프로그램 식의 앞부분은 생략했지만, 이런 경우라면 앞부분에 이미 x라는 변수가 정의가 되어있어야겠지요.)

let x = 1 을 실행할때 환경이 한번 변할것이고, x := x+1을 실행할때 그 변한 환경을 반영해서 프로그램 식이 실행됩니다.

그러나 lex x =1 은 x := x+1까지만 유효한 변수선언이기 때문에 x:=x+2를 실행할때는 왼쪽 식을 처음 실행할때의 환경인 σ를 기반으로 계산이 될 것입니다.

그렇기때문에 결론적으로 S1과 S2가 같은 환경 내에서 실행이 된것입니다.

쉽게 말하자면 프로그램 실행중에 환경은 계속 변할 수 있고, 변해가는 환경을 반영해서 프로그램 식을 계산해주어야 한다고 이해하시면 됩니다.

σ,M⊢C⇒M′ 라는 표기때문에 헷갈리신 것 같은데,프로그램 실행결과로 환경을 리턴할 필요는 없기때문에 표기하지 않은 것일뿐 환경이 변하지 않는다는 뜻은 아닙니다. 실제로는 환경은 계속 변해가면서 실행되게 됩니다.

더 궁금하신 점 있다면 질문해주세요.

-조교 드림.

[이도형]

이해가 되었습니다! 두 분 다 감사합니다!!